Merge pull request kind2-mc#1092 from daniel-larraz/free-const-subran…

…ge-array

Create param subrange constraints for arrays

src/lustre/lustreAstNormalizer.ml

@@ -416,7 +416,7 @@ let mk_range_expr ctx node_id expr_type expr =
         [disj, true]
     )
     | A.IntRange (_, l, u) ->
-      let original_ty, _ = Chk.infer_type_expr ctx (Some node_id) expr |> unwrap in
+      let original_ty, _ = Chk.infer_type_expr ctx node_id expr |> unwrap in
       let original_ty = Chk.expand_type_syn_reftype_history ctx original_ty |> unwrap in
       let user_prop, is_original = match original_ty with
         | A.IntRange (_, l', u') ->
@@ -632,7 +632,7 @@ let add_subrange_constraints info node_id kind vars =
   |> List.fold_left (fun acc (p, id) ->
     let ty = get_type_of_id info node_id id in
     let ty = AIC.inline_constants_of_lustre_type info.context ty in
-    union acc (mk_fresh_subrange_constraint kind info p node_id id ty))
+    union acc (mk_fresh_subrange_constraint kind info p (Some node_id) id ty))
     (empty ())
 
 let add_ref_type_constraints info kind vars =
@@ -1128,7 +1128,7 @@ and normalize_node info map
       | A.NodeConstDecl (p, TypedConst (_, id, _, _)) ->  
         let ty = get_type_of_id info node_id id in
         let ty = AIC.inline_constants_of_lustre_type info.context ty in
-        let gids = union acc (mk_fresh_subrange_constraint Local info p node_id id ty)
+        let gids = union acc (mk_fresh_subrange_constraint Local info p (Some node_id) id ty)
         in union gids (mk_fresh_refinement_type_constraint Local info p (A.Ident (p, id)) ty)
       | A.NodeConstDecl (_, UntypedConst _)-> assert false)
       (empty ())
@@ -1469,7 +1469,7 @@ and normalize_contract info node_id map ivars ovars (p, items) =
                 if Ctx.type_contains_subrange info.context ty || Ctx.type_contains_ref info.context ty then
                   (pos, i, ty),
                   union gids (
-                  union (mk_fresh_subrange_constraint Ghost info pos node_id new_id ty)
+                  union (mk_fresh_subrange_constraint Ghost info pos (Some node_id) new_id ty)
                         (mk_fresh_refinement_type_constraint Ghost info pos (A.Ident (pos, new_id)) ty)), 
                   warnings
                 else (pos, i, ty), gids, []
@@ -1679,8 +1679,10 @@ and normalize_expr ?guard info node_id map =
       List.fold_left
         (fun acc (_, id, ty) ->
           let expr = A.Ident(dpos, id) in
-          let range_exprs =  List.map fst (mk_range_expr info.context node_id ty expr) @ 
-                             List.map snd (mk_ref_type_expr info.context expr Local ty) in
+          let range_exprs =
+            List.map fst (mk_range_expr info.context (Some node_id) ty expr) @
+            List.map snd (mk_ref_type_expr info.context expr Local ty)
+          in
           range_exprs :: acc
         )
         []

src/lustre/lustreAstNormalizer.mli

@@ -82,6 +82,12 @@ val warning_message : warning_kind -> string
 
 val mk_fresh_dummy_index : 'a -> HString.t
 
+val mk_range_expr : TypeCheckerContext.tc_context ->
+  HString.t option ->
+  LustreAst.lustre_type ->
+  LustreAst.expr ->
+  (LustreAst.expr * bool) list
+
 val normalize : TypeCheckerContext.tc_context ->
   LustreAbstractInterpretation.context ->
   LustreAst.t ->

src/lustre/lustreNodeGen.ml

@@ -25,6 +25,7 @@ open LustreReporting
 
 module A = LustreAst
 module AH = LustreAstHelpers
+module AN = LustreAstNormalizer
 module GI = GeneratedIdentifiers
 module G = LustreGlobals
 module N = LustreNode
@@ -2335,24 +2336,12 @@ and compile_node_decl gids_map is_function cstate ctx i ext params inputs output
     nodes = node :: cstate.nodes;
   }
 
-and add_type_constraints global_constraints v ty =
-  match Type.node_of_type ty with
-  | Type.IntRange (Some n1, Some n2) ->
-    E.mk_and
-      (E.mk_lte (E.mk_int n1) (E.mk_var v))
-      (E.mk_lte (E.mk_var v) (E.mk_int n2))
-    :: global_constraints
-  | IntRange (Some n1, None) ->
-    (E.mk_lte (E.mk_int n1) (E.mk_var v)) :: global_constraints
-  | IntRange (None, Some n2) ->
-    (E.mk_lte (E.mk_var v) (E.mk_int n2)) :: global_constraints
-  | _ -> global_constraints
 
 and compile_const_decl ?(ghost = false) cstate ctx map scope = function
-  | A.FreeConst (_, i, ty) ->
+  | A.FreeConst (p, i, ty) ->
     let ident = mk_ident i in
     let cty = compile_ast_type cstate ctx map ty in
-    let over_index = fun i ty (vt, global_constraints) ->
+    let over_index = fun i ty vt ->
       let possible_state_var = mk_state_var
         ?is_input:(Some false)
         ?is_const:(Some true)
@@ -2366,17 +2355,27 @@ and compile_const_decl ?(ghost = false) cstate ctx map scope = function
       in
       match possible_state_var with
       | Some state_var ->
-        let v = Var.mk_const_state_var state_var in
-        X.add i v vt, add_type_constraints global_constraints state_var ty
-      | None -> vt, global_constraints
-    in
-    let vt, global_constraints =
-      X.fold over_index cty (X.empty, cstate.global_constraints)
+        X.add i (Var.mk_const_state_var state_var) vt
+      | None -> vt
     in
+    let vt = X.fold over_index cty X.empty in
     let var_bounds = SVT.fold (fun k v a -> (k, v) :: a) !map.bounds [] in
     List.iter (fun (k, v) -> SVT.add cstate.state_var_bounds k v) var_bounds;
     if ghost then cstate
     else (
+      let global_constraints =
+        let ty = Ctx.expand_type_syn ctx ty in
+        if Ctx.type_contains_subrange ctx ty then (
+          let range_exprs =
+            AN.mk_range_expr ctx None ty (A.Ident (p, i)) |> List.map fst
+          in
+          List.map (fun expr ->
+            let c_expr = compile_ast_expr cstate ctx [] map expr in
+            X.max_binding c_expr |> snd
+          ) range_exprs @ cstate.global_constraints
+        )
+        else cstate.global_constraints
+      in
       { cstate with
         free_constants = (!map.node_name, i, vt) :: cstate.free_constants;
         global_constraints

src/lustre/typeCheckerContext.ml

@@ -676,6 +676,11 @@ let rec type_contains_subrange ctx = function
     (match lookup_ty ctx id with 
     | Some ty -> type_contains_subrange ctx ty
     | _ -> assert false)
+  | UserType (_, ty_args, id) -> (
+    match lookup_ty_syn ctx id ty_args with
+    | Some ty -> type_contains_subrange ctx ty
+    | None -> assert false
+  )
   | _ -> false
 
   let rec type_contains_ref ctx = function

src/transSys.ml

@@ -1101,7 +1101,7 @@ let define_and_declare_of_bounds
 
 
 let assert_global_constraints { global_constraints } assert_term =
-  List.iter (fun c -> assert_term c) global_constraints
+  List.iter (fun c -> assert_term (Term.convert_select c)) global_constraints
 
 let init_uf_def { init_uf_symbol; init_formals; init } = 
   (init_uf_symbol, (init_formals, init))

tests/regression/success/free_const_subrange.lus

@@ -0,0 +1,14 @@
+
+type Nat = subrange [0,*] of int;
+
+type T = [Nat,bool];
+type Rec = struct { f:T };
+
+const R: Rec;
+const C: Nat^2;
+
+node N() returns (ok: bool)
+let
+  check "P1" C[0] >= 0;
+  check "P2" R.f.%0 >= 0;
+tel