Merge branch 'chiquito-2024' into leo/interpreter

src/compiler/semantic/rules.rs

@@ -336,11 +336,84 @@ fn types_rule_tl(
     }
 }
 
+/// Check if the condition in an if statement is a logic expression (allowing bool literals and
+/// signals).
+fn if_condition_rule(analyser: &mut Analyser, stmt: &Statement<BigInt, Identifier>) {
+    match stmt {
+        Statement::IfThen(dsym, cond, _) | Statement::IfThenElse(dsym, cond, _, _) => {
+            // Check if the condition is a logic expression
+            let cond = cond.as_ref();
+            match cond {
+                Expression::True(_) | Expression::False(_) => {}
+
+                // Check if the signal is a bool
+                Expression::Query(_, s) => {
+                    if let Some(symbol) =
+                        analyser.symbols.find_symbol(&analyser.cur_scope, s.name())
+                    {
+                        if symbol.symbol.get_type() != "bool" {
+                            analyser.error(
+                                format!(
+                                    "Signal {:#?} in if statement condition must be bool",
+                                    cond
+                                ),
+                                dsym,
+                            )
+                        }
+                    }
+                }
+                _ => {
+                    if !cond.is_logic() {
+                        analyser.error(
+                            format!(
+                                "Condition {:#?} in if statement must be a logic expression",
+                                cond
+                            ),
+                            dsym,
+                        )
+                    }
+                }
+            }
+        }
+        _ => {}
+    }
+}
+
+// Left side of "=" should be only wg vars, no signals.
+fn wg_assignment_rule(analyser: &mut Analyser, expr: &Statement<BigInt, Identifier>) {
+    let ids = match expr {
+        Statement::WGAssignment(_, id, _) => id,
+        _ => return,
+    };
+
+    ids.iter().for_each(|id| {
+        if let Some(symbol) = analyser.symbols.find_symbol(&analyser.cur_scope, id.name()) {
+            let is_wgvar = matches!(
+                symbol.symbol.category,
+                SymbolCategory::WGVar
+                    | SymbolCategory::InputWGVar
+                    | SymbolCategory::OutputWGVar
+                    | SymbolCategory::InoutWGVar
+            );
+            if !is_wgvar {
+                analyser.error(
+                    format!(
+                        "Cannot assign with = to {:#?} {}, you can only assign to WGVars. Use <-- or <== instead.",
+                        symbol.symbol.category,
+                        id.name()
+                    ),
+                    &expr.get_dsym(),
+                )
+            }
+        }
+    });
+}
+
 lazy_static! {
     /// Global semantic analyser rules.
     pub(super) static ref RULES: RuleSet = RuleSet {
         expression: vec![undeclared_rule, true_false_rule],
-        statement: vec![state_decl, assignment_rule, assert_rule],
+        statement: vec![state_decl, assignment_rule, assert_rule, if_condition_rule, wg_assignment_rule],
         new_symbol: vec![rotation_decl, redeclare_rule, types_rule],
         new_tl_symbol: vec![rotation_decl_tl, machine_decl_tl, types_rule_tl],
     };
@@ -1029,8 +1102,8 @@ mod test {
 
              c <== a + b;
 
-             if i + 1 {
-                if 1 * true ^ false - 123 && 0 + false * false {
+             if i + 1 == 0 {
+                if 1 * true ^ false - 123 && 0 + false * false == 0 {
                     a <== 1;
                 }
               -> final {
@@ -1062,4 +1135,142 @@ mod test {
             r#"[SemErr { msg: "Cannot use true in expression 2 + true", dsym: DebugSymRef { line: 15, cols: "42-46" } }, SemErr { msg: "Cannot use true in expression 1 * true", dsym: DebugSymRef { line: 32, cols: "24-28" } }, SemErr { msg: "Cannot use false in expression false - 123", dsym: DebugSymRef { line: 32, cols: "31-36" } }, SemErr { msg: "Cannot use false in expression false * false", dsym: DebugSymRef { line: 32, cols: "50-55" } }, SemErr { msg: "Cannot use false in expression false * false", dsym: DebugSymRef { line: 32, cols: "58-63" } }]"#
         );
     }
+
+    #[test]
+    fn test_if_expression_rule() {
+        let circuit = "
+        machine fibo(signal n) (signal b: field) {
+            // n and be are created automatically as shared
+            // signals
+            signal a: field, i;
+
+            // there is always a state called initial
+            // input signals get bound to the signal
+            // in the initial state (first instance)
+            state initial {
+             signal c;
+
+             i, a, b, c <== 1, 1, 1, 2;
+
+             if false {                 // allowed
+                a <== 1;
+             }
+
+             if 3 + i == a {            // allowed
+                a <== 1;
+             }
+
+             -> middle {
+              a', b', n' <== b, c, n;
+             }
+            }
+
+            state middle {
+             signal c;
+             signal t: bool;
+
+             c <== a + b;
+
+             t <== true;
+
+             if i + 1 {                 // wrong
+                if c {                  // wrong
+                    a <== 1;
+                }
+                if t {                  // allowed
+                    a <== 1;
+                }
+                if 4 {                  // wrong
+                    a <== 1;
+                }
+              -> final {
+               i', b', n' <== i + 1, c, n;
+              }
+             } else {
+              -> middle {
+               i', a', b', n' <== i + 1, b, c, n;
+              }
+             }
+            }
+
+            // There is always a state called final.
+            // Output signals get automatically bound to the signals
+            // with the same name in the final step (last instance).
+            // This state can be implicit if there are no constraints in it.
+           }
+        ";
+
+        let debug_sym_ref_factory = DebugSymRefFactory::new("", &circuit);
+        let decls = lang::TLDeclsParser::new()
+            .parse(&debug_sym_ref_factory, circuit)
+            .unwrap();
+
+        let result = analyse(&decls);
+
+        assert_eq!(
+            format!("{:?}", result.messages),
+            r#"[SemErr { msg: "Condition i + 1 in if statement must be a logic expression", dsym: DebugSymRef { start: "36:14", end: "53:15" } }, SemErr { msg: "Signal c in if statement condition must be bool", dsym: DebugSymRef { start: "37:17", end: "39:18" } }, SemErr { msg: "Condition 4 in if statement must be a logic expression", dsym: DebugSymRef { start: "43:17", end: "45:18" } }]"#
+        );
+    }
+
+    #[test]
+    fn test_wg_assignment_rule() {
+        let circuit = "
+        machine fibo(signal n) (signal b: field) {
+            // n and be are created automatically as shared
+            // signals
+            signal a: field, i;
+            var wgvar;
+
+            // there is always a state called initial
+            // input signals get bound to the signal
+            // in the initial state (first instance)
+            state initial {
+             signal c;
+
+             wgvar = 31;
+             i = 0;                      // wrong
+
+             i, a, b, c <== 1, 1, 1, 2;
+
+             -> middle {
+              a', b', n' <== b, c, n;
+             }
+            }
+
+            state middle {
+             signal c;
+
+             c <== a + b;
+
+             if i + 1 == n {
+              -> final {
+               i', b', n' <== i + 1, c, n;
+              }
+             } else {
+              -> middle {
+               i', a', b', n' <== i + 1, b, c, n;
+              }
+             }
+            }
+
+            // There is always a state called final.
+            // Output signals get automatically bound to the signals
+            // with the same name in the final step (last instance).
+            // This state can be implicit if there are no constraints in it.
+           }
+        ";
+
+        let debug_sym_ref_factory = DebugSymRefFactory::new("", circuit);
+        let decls = lang::TLDeclsParser::new()
+            .parse(&debug_sym_ref_factory, circuit)
+            .unwrap();
+
+        let result = analyse(&decls);
+
+        assert_eq!(
+            format!("{:?}", result.messages),
+            r#"[SemErr { msg: "Cannot assign with = to Signal i, you can only assign to WGVars. Use <-- or <== instead.", dsym: DebugSymRef { line: 15, cols: "14-20" } }]"#
+        );
+    }
 }