Merge pull request kind2-mc#999 from daniel-larraz/array-fixes

Array fixes

src/lustre/generatedIdentifiers.ml

@@ -68,6 +68,7 @@ type t = {
     * LustreAst.expr)
     list;
   nonvacuity_props: StringSet.t;
+  array_literal_vars: StringSet.t;
 }
 
 (* String constant used in lustreDesugarIfBlocks.ml and lustreDesugarFrameBlocks.ml
@@ -106,6 +107,7 @@ let union ids1 ids2 = {
     expanded_variables = StringSet.union ids1.expanded_variables ids2.expanded_variables;
     equations = ids1.equations @ ids2.equations;
     nonvacuity_props = StringSet.union ids1.nonvacuity_props ids2.nonvacuity_props;
+    array_literal_vars = StringSet.union ids1.array_literal_vars ids2.array_literal_vars;
   }
 
 (* Same as union_keys, but we don't assume that identifiers are unique *)
@@ -127,4 +129,5 @@ let union_keys2 key id1 id2 = match key, id1, id2 with
     expanded_variables = StringSet.empty;
     equations = [];
     nonvacuity_props = StringSet.empty;
+    array_literal_vars = StringSet.empty;
   }

src/lustre/generatedIdentifiers.mli

@@ -68,6 +68,7 @@ type t = {
     * LustreAst.expr)
     list;
   nonvacuity_props: StringSet.t;
+  array_literal_vars: StringSet.t; (* Variables equal to an array literal *)
 }
 
 (* String constant used in lustreDesugarIfBlocks.ml and lustreDesugarFrameBlocks.ml

src/lustre/lustreAstInlineConstants.ml

@@ -222,14 +222,18 @@ and simplify_array_index: TC.tc_context -> Lib.position -> LA.expr -> LA.expr ->
   = fun ctx pos e1 idx -> 
   let e1' = simplify_expr ctx e1 in
   let idx' = simplify_expr ctx idx in
+  let raise_error () =
+    raise (Out_of_bounds (pos, "Array element access out of bounds."))
+  in
   match e1' with
   | LA.GroupExpr (_, ArrayExpr, es) ->
      (match (eval_int_expr ctx idx) with
-      | Ok i -> if List.length es > i
-                then List.nth es i
-                else
-                  (raise (Out_of_bounds (pos, "Array element access out of bounds.")))
+      | Ok i -> if List.length es > i then List.nth es i else raise_error ()
       | Error _ -> LA.ArrayIndex (pos, e1', idx'))
+  | LA.ArrayConstr (_, v, s) ->
+     (match (eval_int_expr ctx idx), (eval_int_expr ctx s) with
+     | Ok i, Ok j -> if j > i then v else raise_error ()
+     | _, _ -> LA.ArrayIndex (pos, e1', idx'))
   | _ ->
     ArrayIndex (pos, e1', idx')
 (** picks out the idx'th component of an array if it can *)
@@ -353,10 +357,10 @@ and simplify_expr ?(is_guarded = false) ctx =
   | LA.ArrayConstr (pos, e1, e2) ->
      let e1' = simplify_expr ~is_guarded ctx e1 in
      let e2' = simplify_expr ~is_guarded ctx e2 in
-     let e' = LA.ArrayConstr (pos, e1', e2') in
-     (match (eval_int_expr ctx e2) with
+     let e' = LA.ArrayConstr (pos, e1', e2') in e'
+     (*(match (eval_int_expr ctx e2) with
       | Ok size -> LA.GroupExpr (pos, LA.ArrayExpr, Lib.list_init (fun _ -> e1') size)
-      | Error _ -> e')
+      | Error _ -> e')*)
   | LA.ArrayIndex (pos, e1, e2) -> simplify_array_index ctx pos e1 e2
   | LA.ArrayConcat (pos, e1, e2) as e->
      (match (simplify_expr ~is_guarded ctx e1, simplify_expr ~is_guarded ctx e2) with

src/lustre/lustreAstNormalizer.ml

@@ -334,13 +334,17 @@ let extract_array_size = function
 
 let generalize_to_array_expr name ind_vars expr nexpr = 
   let vars = AH.vars expr in
-  let ind_vars = List.map (fun (i, _) -> i) (StringMap.bindings ind_vars) in
+  let ind_vars = List.map fst (StringMap.bindings ind_vars) in
   let ind_vars = List.filter (fun x -> A.SI.mem x vars) ind_vars in
-  let (eq_lhs, nexpr) = if List.length ind_vars = 0
-    then A.StructDef (dpos, [SingleIdent (dpos, name)]), nexpr
-    else A.StructDef (dpos, [ArrayDef (dpos, name, ind_vars)]),
+  let (eq_lhs, nexpr) =
+    match ind_vars with
+    | [] ->
+      A.StructDef (dpos, [SingleIdent (dpos, name)]), nexpr
+    | _ ->
+      A.StructDef (dpos, [ArrayDef (dpos, name, ind_vars)]),
       A.ArrayIndex (dpos, nexpr, A.Ident (dpos, List.hd ind_vars))
-  in eq_lhs, nexpr
+  in
+  eq_lhs, nexpr
 
 let mk_fresh_local force info pos is_ghost ind_vars expr_type expr =
   match (LocalCache.find_opt local_cache expr, force) with
@@ -369,14 +373,15 @@ let mk_fresh_array_ctor info pos ind_vars expr_type expr size_expr =
     equations = [(info.quantified_variables, info.contract_scope, eq_lhs, expr)]; }
   in nexpr, gids
 
-let mk_fresh_node_arg_local info pos is_const ind_vars expr_type expr =
+let mk_fresh_node_arg_local info pos is_const expr_type expr =
   match NodeArgCache.find_opt node_arg_cache expr with
   | Some nexpr -> nexpr, empty ()
   | None ->
   i := !i + 1;
   let prefix = HString.mk_hstring (string_of_int !i) in
   let name = HString.concat2 prefix (HString.mk_hstring "_gklocal") in
   let nexpr = A.Ident (pos, name) in
+  let ind_vars = info.inductive_variables in
   let (eq_lhs, nexpr) = generalize_to_array_expr name ind_vars expr nexpr in
   let gids = { (empty ()) with
     node_args = [(name, is_const, expr_type, expr)];
@@ -1182,6 +1187,26 @@ and combine_args_with_const info args flags =
   |> snd |> List.rev
 
 and normalize_expr ?guard info map =
+  let abstract_array_literal info expr nexpr =
+    let ivars = info.inductive_variables in
+    let pos = AH.pos_of_expr expr in
+    let ty = if expr_has_inductive_var ivars expr |> is_some then
+      (StringMap.choose_opt info.inductive_variables) |> get |> snd
+    else Chk.infer_type_expr info.context expr |> unwrap
+    in
+    let nexpr, gids = mk_fresh_local false info pos false ivars ty nexpr in
+    let id =
+      match nexpr with
+      | A.Ident (_, name) -> name
+      | _ -> assert false
+    in
+    let gids =
+      { gids with 
+        array_literal_vars = StringSet.add id gids.array_literal_vars
+      }
+    in
+    nexpr, gids
+  in
   let abstract_node_arg ?guard force is_const info map expr =
     let nexpr, gids1, warnings = normalize_expr ?guard info map expr in
     if should_not_abstract force nexpr then
@@ -1193,7 +1218,7 @@ and normalize_expr ?guard info map =
         (StringMap.choose_opt info.inductive_variables) |> get |> snd
       else Chk.infer_type_expr info.context expr |> unwrap
       in
-      let iexpr, gids2 = mk_fresh_node_arg_local info pos is_const ivars ty nexpr in
+      let iexpr, gids2 = mk_fresh_node_arg_local info pos is_const ty nexpr in
       iexpr, union gids1 gids2, warnings
   in function
   (* ************************************************************************ *)
@@ -1321,6 +1346,14 @@ and normalize_expr ?guard info map =
     let ivars = info.inductive_variables in
     let iexpr, gids2= mk_fresh_array_ctor info pos ivars ty nexpr size_expr in
     ArrayConstr (pos, iexpr, size_expr), union gids1 gids2, warnings
+  | GroupExpr (pos, ArrayExpr, expr_list) as expr ->
+    let nexpr_list, gids1, warnings = normalize_list
+      (normalize_expr ?guard:None info map)
+      expr_list
+    in
+    let nexpr = A.GroupExpr (pos, ArrayExpr, nexpr_list) in
+    let nexpr, gids2 = abstract_array_literal info expr nexpr in
+    nexpr, union gids1 gids2, warnings
   (* ************************************************************************ *)
   (* Variable renaming to ease handling contract scopes                       *)
   (* ************************************************************************ *)

src/lustre/lustreExpr.ml

@@ -3562,8 +3562,7 @@ let type_of_select = function
 
     (function t -> 
 
-      (* Second argument must match index type of array *)
-      if Type.check_type (Type.index_type_of_array s) t then 
+      if (Type.is_int t || Type.is_int_range t) then
 
         (* Return type of array elements *)
         Type.elem_type_of_array s
@@ -3605,8 +3604,7 @@ let type_of_store = function
 
     (fun i v -> 
 
-      (* Second argument must match index type of array *)
-       if Type.check_type i (Type.index_type_of_array s) &&
+       if (Type.is_int i || Type.is_int_range i) &&
           Type.check_type (Type.elem_type_of_array s) v
        then 
 
@@ -3752,9 +3750,20 @@ let numeral_of_expr = Term.numeral_of_term
 let unsafe_term_of_expr e = (e : Term.t)
 let unsafe_expr_of_term t = t
 
+let push_select { expr_init; expr_step; expr_type } =
+  let expr_init' = Term.push_select expr_init in
+  let expr_step' = Term.push_select expr_step in
+  { expr_init = expr_init';
+    expr_step = expr_step';
+    expr_type
+  }
+
+let mk_select_and_push e1 e2 =
+  mk_select e1 e2 |> push_select
+
 (* 
    Local Variables:
    compile-command: "make -k -C .."
    indent-tabs-mode: nil
    End: 
-*)
+*)

src/lustre/lustreExpr.mli

@@ -558,6 +558,13 @@ val mk_let : (Var.t * expr) list -> t -> t
 
 val apply_subst : (Var.t * expr) list -> t -> t
 
+(** Return an expression where the top-level selects of the initial and/or
+    the step expressions (if any) have been pushed *)
+val push_select : t -> t
+
+(**  Make select from an array and push it *)
+val mk_select_and_push : t -> t -> t
+
 (* 
    Local Variables:
    compile-command: "make -k -C .."

src/lustre/lustreIndex.ml

@@ -266,6 +266,16 @@ let top_max_index t =
   with Not_found -> (-1)
 
 
+let filter_array_indices index = List.filter (
+  function
+  | ArrayVarIndex _
+  | ArrayIntIndex _ -> false
+  | RecordIndex _
+  | TupleIndex _
+  | ListIndex _
+  | AbstractTypeIndex _ -> true)
+  index
+
 let compatible_one_index i1 i2 = match i1, i2 with
   | RecordIndex s1, RecordIndex s2 -> s1 = s2
   | TupleIndex i1, TupleIndex i2 -> i1 = i2
@@ -309,7 +319,7 @@ let mk_scope_for_index index =
        |> String.length
        |> string_of_int
        |> Ident.of_string)
-    index
+    (filter_array_indices index)
   |> Scope.mk_scope
 
 

src/lustre/lustreIndex.mli

@@ -101,6 +101,7 @@ val array_vars_of_index : index -> StateVar.t list
     [Invalid_argument "top_max_index"] if the first index is not a list *)
 val top_max_index : 'a t -> int
 
+val filter_array_indices : index -> index
 
 val compatible_indexes : index -> index -> bool