Merge pull request kind2-mc#1021 from daniel-larraz/pre-in-array-def

Fix application of pre operator to bound variables and arrays

src/lustre/lustreAstNormalizer.ml

@@ -1301,11 +1301,11 @@ and normalize_expr ?guard info map =
     normalize_expr ?guard info map expr
   | Pre (pos, expr) ->
     let ivars = info.inductive_variables in
-    let ty = if expr_has_inductive_var ivars expr then
-        (StringMap.choose_opt info.inductive_variables) |> get |> snd
-      else Chk.infer_type_expr info.context expr |> unwrap
+    let ty, force = if expr_has_inductive_var ivars expr then
+        (StringMap.choose_opt info.inductive_variables) |> get |> snd, true
+      else Chk.infer_type_expr info.context expr |> unwrap, false
       in
-    let nexpr, gids1, warnings1 = abstract_expr ?guard:None false info map false expr in
+    let nexpr, gids1, warnings1 = abstract_expr ?guard:None force info map false expr in
     let guard, gids2, warnings2, previously_guarded = match guard with
       | Some guard -> guard, empty (), [], true
       | None ->
@@ -1315,13 +1315,21 @@ and normalize_expr ?guard info map =
     in
     let gids = union gids1 gids2 in
     let warnings = warnings1 @ warnings2 in
-    let nexpr' = match nexpr with
-      | A.ArrayIndex (pos2, expr1, expr2) ->
-        A.ArrayIndex (pos2, Pre (pos, expr1), expr2)
-      | e -> Pre (pos, e)
-    in
-    if previously_guarded then nexpr', gids, warnings
-    else Arrow (pos, guard, nexpr'), gids, warnings
+    if previously_guarded then
+      let nexpr' = match nexpr with
+        | A.ArrayIndex (pos2, expr1, expr2) ->
+          A.ArrayIndex (pos2, Pre (pos, expr1), expr2)
+        | e -> Pre (pos, e)
+      in
+      nexpr', gids, warnings
+    else
+      let nexpr' =
+        match nexpr with
+        | A.ArrayIndex (pos2, expr1, expr2) ->
+          A.ArrayIndex (pos2, A.Arrow (pos, guard, Pre (pos, expr1)), expr2)
+        | e -> Arrow (pos, guard, Pre (pos, e))
+      in
+      nexpr', gids, warnings
   (* ************************************************************************ *)
   (* Misc. abstractions                                                       *)
   (* ************************************************************************ *)

src/lustre/lustreNodeGen.ml

@@ -1689,7 +1689,8 @@ and compile_node_decl gids is_function cstate ctx i ext inputs outputs locals it
     let over_oracles (oracles, osvm) (id, expr_type, expr) =
       let oracle_ident = mk_ident id in
       let closed_sv = match expr with
-        | A.Ident (_, id') ->
+        | A.Ident (_, id')
+        | A.ArrayIndex (_, A.Ident (_, id'), _) ->
           let ident = mk_ident id' in
           let closed_sv = H.find !map.state_var ident in
           Some closed_sv

src/lustre/lustreSyntaxChecks.ml

@@ -46,6 +46,7 @@ type error_kind = Unknown of string
   | UndefinedNode of HString.t
   | UndefinedContract of HString.t
   | DanglingIdentifier of HString.t
+  | QuantifiedVariableInPre of HString.t
   | QuantifiedVariableInNodeArgument of HString.t * HString.t
   | SymbolicArrayIndexInNodeArgument of HString.t * HString.t
   | ChooseOpInFunction
@@ -89,6 +90,8 @@ let error_message kind = match kind with
     ^ HString.string_of_hstring id ^ "' is undefined"
   | DanglingIdentifier id -> "Unknown identifier '"
     ^ HString.string_of_hstring id ^ "'"
+  | QuantifiedVariableInPre var -> "Quantified variable '"
+    ^ HString.string_of_hstring var ^ "' is not allowed in an argument to pre operator"
   | QuantifiedVariableInNodeArgument (var, node) -> "Quantified variable '"
     ^ HString.string_of_hstring var ^ "' is not allowed in an argument to the node call '"
     ^ HString.string_of_hstring node ^ "'"
@@ -547,6 +550,16 @@ let no_quant_var_or_symbolic_index_in_node_call ctx = function
     in
     let check = List.map over_vars (LA.SI.elements vars) in
     List.fold_left (>>) (Ok ()) check
+  | LA.Pre (_, ArrayIndex (_, _, _)) -> Ok ()
+  | LA.Pre (pos, e) ->
+    let vars = LAH.vars_without_node_call_ids e in
+    let over_vars j = 
+      let found_quant = StringMap.mem j ctx.quant_vars in
+      if found_quant then syntax_error pos (QuantifiedVariableInPre j)
+      else Ok ()
+    in
+    let check = List.map over_vars (LA.SI.elements vars) in
+    List.fold_left (>>) (Ok ()) check
   | _ -> Ok ()
 
 let no_calls_to_node ctx = function

src/lustre/lustreSyntaxChecks.mli

@@ -27,6 +27,7 @@ type error_kind = Unknown of string
   | UndefinedNode of HString.t
   | UndefinedContract of HString.t
   | DanglingIdentifier of HString.t
+  | QuantifiedVariableInPre of HString.t
   | QuantifiedVariableInNodeArgument of HString.t * HString.t
   | SymbolicArrayIndexInNodeArgument of HString.t * HString.t
   | ChooseOpInFunction

tests/ounit/lustre/lustreSyntaxChecks/pre_of_quantified_var.lus

@@ -0,0 +1,8 @@
+
+const n: int;
+
+node N() returns (B: int^n);
+let
+  B[i] = 0 -> i;
+  check forall (i: int) 0 <= i and i < n => B[i]=(0 -> pre i);
+tel

tests/ounit/lustre/testLustreFrontend.ml

@@ -170,6 +170,10 @@ let _ = run_test_tt_main ("frontend LustreSyntaxChecks error tests" >::: [
     match load_file "./lustreSyntaxChecks/var_redefinition3.lus" with
     | Error (`LustreSyntaxChecksError (_, DuplicateLocal _)) -> true
     | _ -> false);
+  mk_test "test applying pre operator to quantified variable" (fun () ->
+    match load_file "./lustreSyntaxChecks/pre_of_quantified_var.lus" with
+    | Error (`LustreSyntaxChecksError (_, QuantifiedVariableInPre _)) -> true
+    | _ -> false);
 ])
 
 (* *************************************************************************** *)

tests/regression/success/pre_in_array_def.lus

@@ -0,0 +1,13 @@
+
+node F(x:int) returns (y:int);
+let
+  y = x + 1;
+tel
+
+const n: int = 3;
+
+node N(A: int^n) returns (B: int^n);
+let
+  B[i] = pre (A[i] + 1) -> F(pre i);
+  check true -> B[0]=1;
+tel