Merge pull request #1124 from lorchrob/history-quantified-var

Disallow quantified variables in history type constructor
kind2-mc · Jan 23, 2025 · 24f3d5d · 24f3d5d
2 parents ad44ec9 + 7389f6a
commit 24f3d5d
Show file tree

Hide file tree

Showing 6 changed files with 42 additions and 0 deletions.
diff --git a/src/lustre/lustreSyntaxChecks.ml b/src/lustre/lustreSyntaxChecks.ml
@@ -69,6 +69,7 @@ type error_kind = Unknown of string
   | IllegalClockExprInActivate of LustreAst.expr
   | OpaqueWithoutContract of LustreAst.ident
   | TransparentWithoutBody of LustreAst.ident
+  | IllegalHistoryVar of LustreAst.ident
 
 type error = [
   | `LustreSyntaxChecksError of Lib.position * error_kind
@@ -123,6 +124,7 @@ let error_message kind = match kind with
   | IllegalClockExprInActivate e -> "Illegal clock expression '" ^ LA.string_of_expr e ^ "' in activate"
   | OpaqueWithoutContract n -> "An opaque annotation found for a node/function without a contract: " ^ HString.string_of_hstring n
   | TransparentWithoutBody n -> "A transparent annotation found for an imported node/function: " ^ HString.string_of_hstring n
+  | IllegalHistoryVar id -> "History type constructor uses illegal quantified variable '" ^ HString.string_of_hstring id ^ "'"
 
 let syntax_error pos kind = Error (`LustreSyntaxChecksError (pos, kind))
 
@@ -587,6 +589,20 @@ let no_clock_inputs_or_outputs pos = function
   | LA.ClockTrue -> Ok ()
   | _ -> syntax_error pos UnsupportedClockedInputOrOutput
 
+(* Make sure the History type constructor doesn't take a quantified variable as input *)
+let check_quantified_vars ctx vars = 
+  Res.seq (List.map (fun (_, _, ty) -> 
+    match ty with
+    | LA.History (pos, id) -> (
+      match StringMap.find_opt id ctx.quant_vars with 
+      | Some (Some _) -> syntax_error pos (IllegalHistoryVar id)
+      | _ -> Res.ok ()
+    )
+    (* We don't currently need to recurse on other cases because a History type 
+       cannot be nested within another type (see lustreParser.mly) *)
+    | _ -> Ok ()
+  ) vars)
+
 let rec expr_only_supported_in_merge observer expr =
   let r = expr_only_supported_in_merge in
   let r_list obs e = Res.seqM (fun x _ -> x) () (List.map (r obs) e) in
@@ -904,6 +920,7 @@ and check_expr: context -> (context -> LA.expr -> ([> warning] list, ([> error]
     | Quantifier (_, _, vars, e) ->
         let over_vars ctx (_, i, ty) = ctx_add_quant_var ctx i (Some ty) in
         let ctx = List.fold_left over_vars ctx vars in
+        check_quantified_vars ctx vars >>
         check_expr ctx f e
     | BinaryOp (_, _, e1, e2)
     | CompOp (_, _, e1, e2)

diff --git a/src/lustre/lustreSyntaxChecks.mli b/src/lustre/lustreSyntaxChecks.mli
@@ -52,6 +52,7 @@ type error_kind = Unknown of string
   | IllegalClockExprInActivate of LustreAst.expr
   | OpaqueWithoutContract of LustreAst.ident
   | TransparentWithoutBody of LustreAst.ident
+  | IllegalHistoryVar of LustreAst.ident
 
 type error = [
   | `LustreSyntaxChecksError of Lib.position * error_kind

diff --git a/tests/ounit/lustre/lustreSyntaxChecks/history_quantified_var_1.lus b/tests/ounit/lustre/lustreSyntaxChecks/history_quantified_var_1.lus
@@ -0,0 +1,4 @@
+node N(x: int) returns (y: int); 
+let 
+    check forall (n: int) forall (z: history(n)) true; 
+tel
diff --git a/tests/ounit/lustre/lustreSyntaxChecks/history_quantified_var_2.lus b/tests/ounit/lustre/lustreSyntaxChecks/history_quantified_var_2.lus
@@ -0,0 +1,4 @@
+node N(x: int) returns (y: int); 
+let 
+    check forall (n: int; z: history(n)) true;  
+tel
diff --git a/tests/ounit/lustre/lustreSyntaxChecks/history_quantified_var_3.lus b/tests/ounit/lustre/lustreSyntaxChecks/history_quantified_var_3.lus
@@ -0,0 +1,4 @@
+node N(x: int) returns (y: int); 
+let 
+    check forall (z: history(z)) true;  
+tel
diff --git a/tests/ounit/lustre/testLustreFrontend.ml b/tests/ounit/lustre/testLustreFrontend.ml
@@ -170,6 +170,18 @@ let _ = run_test_tt_main ("frontend LustreSyntaxChecks error tests" >::: [
     match load_file "./lustreSyntaxChecks/transparent_no_body.lus" with
     | Error (`LustreSyntaxChecksError (_, TransparentWithoutBody _)) -> true
     | _ -> false);
+  mk_test "test history type constructor with quantified variable 1" (fun () ->
+    match load_file "./lustreSyntaxChecks/history_quantified_var_1.lus" with
+    | Error (`LustreSyntaxChecksError (_, IllegalHistoryVar _)) -> true
+    | _ -> false);
+  mk_test "test history type constructor with quantified variable 2" (fun () ->
+    match load_file "./lustreSyntaxChecks/history_quantified_var_2.lus" with
+    | Error (`LustreSyntaxChecksError (_, IllegalHistoryVar _)) -> true
+    | _ -> false);
+  mk_test "test history type constructor with quantified variable 3" (fun () ->
+    match load_file "./lustreSyntaxChecks/history_quantified_var_3.lus" with
+    | Error (`LustreSyntaxChecksError (_, IllegalHistoryVar _)) -> true
+    | _ -> false);
 ])
 
 (* *************************************************************************** *)