Merge branch 'develop' into global-const-static-checks

src/c2i/C2I.ml

@@ -195,14 +195,20 @@ let mk_solvers sys =
     (SMTSolver.declare_sort solver3)
     Numeral.zero Numeral.one ;
 
+  TransSys.assert_global_constraints sys (SMTSolver.assert_term solver1) ;
+
   (* Asserting init in [solver1]. *)
   TransSys.init_of_bound (Some (SMTSolver.declare_fun solver1)) sys Numeral.zero
   |> SMTSolver.assert_term solver1 ;
 
+  TransSys.assert_global_constraints sys (SMTSolver.assert_term solver2) ;
+
   (* Asserting trans in [solver2]. *)
   TransSys.trans_of_bound (Some (SMTSolver.declare_fun solver2)) sys Numeral.one
   |> SMTSolver.assert_term solver2 ;
 
+  TransSys.assert_global_constraints sys (SMTSolver.assert_term solver3) ;
+
   (* Asserting trans in [solver3]. *)
   TransSys.trans_of_bound (Some (SMTSolver.declare_fun solver3)) sys Numeral.one
   |> SMTSolver.assert_term solver3 ;

src/certif/certifChecker.ml

@@ -491,6 +491,8 @@ let under_approx sys k invs prop =
   if Flags.BmcKind.compress () then
     Compress.init (SMTSolver.declare_fun solver) sys ;
 
+  TransSys.assert_global_constraints sys (SMTSolver.assert_term solver) ;
+
   (* Asserting transition relation up to k *)
   for i = 1 to k do
     TransSys.trans_of_bound
@@ -1174,6 +1176,8 @@ let minimize_invariants sys props invs_predicate =
     (* Declaring path compression function if needed. *)
     if Flags.BmcKind.compress () then
       Compress.init (SMTSolver.declare_fun solver) sys ;
+
+    TransSys.assert_global_constraints sys (SMTSolver.assert_term solver) ;
 
     (* The property we want to re-verify is the conjunction of all properties *)
     let prop = Term.mk_and props in
@@ -1456,7 +1460,12 @@ let export_system_defs
     add_section fmt "Constants";
     List.iter (fun sv ->
         declare_const fmt (StateVar.uf_symbol_of_state_var sv)
-    ) consts
+    ) consts ;
+    let constraints = TS.global_constraints sys in
+    if constraints <> [] then (
+      add_section fmt "Constant constraints";
+      List.iter (fun c -> assert_expr fmt c) constraints
+    )
   ) ;
 
   (* Declaring function symbols *)
@@ -2517,8 +2526,9 @@ let merge_systems lustre_vars kind2_sys jkind_sys =
       state_vars
       unconstrained_inputs
       bounds
-      []
-      []
+      [] (* Global consts *)
+      [] (* Global constraints *)
+      [] (* Ufs *)
       init_uf
       init_args
       init_term

src/certif/jkindParser.ml

@@ -455,8 +455,9 @@ let of_channel in_ch =
       allstatevars
       StateVar.StateVarSet.empty (* underapproximation *)
       (StateVar.StateVarHashtbl.create 3)
-      []
-      []
+      [] (* Global consts *)
+      [] (* Global constraints *)
+      [] (* Ufs *)
       init_uf_symbol
       init_args
       init_term

src/ic3/IC3.ml

@@ -674,14 +674,15 @@ let extrapolate trans_sys state f g =
   (* Construct term to be generalized with the transition relation and
      the invariants *)
   let term = 
-    Term.mk_and 
+    Term.mk_and
+      ((TransSys.global_constraints trans_sys) @
       [f; 
        TransSys.trans_of_bound None trans_sys Numeral.one; 
 (*
        TransSys.invars_of_bound trans_sys ~one_state_only:true Numeral.zero; 
        TransSys.invars_of_bound trans_sys Numeral.one; 
 *)
-       Term.bump_state Numeral.one g]
+       Term.bump_state Numeral.one g])
   in
 
   (* Get primed variables in the transition system *)
@@ -809,7 +810,8 @@ let abstr_simulate trace trans_sys raise_cex =
   in
 
   let interpolizers =
-    (Term.mk_and ((TransSys.init_of_bound
+    (Term.mk_and ((TransSys.global_constraints trans_sys) @
+                  (TransSys.init_of_bound
                      (Some (SMTSolver.declare_fun intrpo))
                      trans_sys Numeral.zero)
                   :: List.hd interpolizers))
@@ -3111,6 +3113,8 @@ let main_ic3 input_sys aparam trans_sys =
       Numeral.zero
   in
 
+  TransSys.assert_global_constraints trans_sys (SMTSolver.assert_term solver) ;
+
   (* Assert invariants for current state if not empty *)
   if invars_0 <> [] then
 

src/ic3ia/IC3IA.ml

@@ -112,20 +112,22 @@ let sys_def solver sys offset =
         Term.mk_not init_term_prev
       ]
    in
-   Term.mk_or [init; trans]
+   Term.mk_and (TransSys.global_constraints sys @
+     [Term.mk_or [init; trans]])
 
 let sys_def_unrolling solver sys offset =
   let init_term_curr =
     get_init offset
   in
   if Numeral.(equal offset zero) then
     Term.mk_and
+      (TransSys.global_constraints sys @
       [TransSys.init_of_bound
         (Some (SMTSolver.declare_fun solver))
         sys
         offset;
         Term.mk_not init_term_curr
-      ]
+      ])
   else
     Term.mk_and
       [TransSys.trans_of_bound

src/induction/base.ml

@@ -381,6 +381,8 @@ let init input_sys aparam trans skip =
     (SMTSolver.declare_sort solver)
     Numeral.zero Numeral.zero ;
 
+  TransSys.assert_global_constraints trans (SMTSolver.assert_term solver) ;
+
   (* Asserting init. *)
   TransSys.init_of_bound
     (Some (SMTSolver.declare_fun solver)) trans Numeral.zero

src/induction/step.ml

@@ -686,6 +686,8 @@ let launch input_sys aparam trans =
     (* Declaring path compression function. *)
     Compress.init (SMTSolver.declare_fun solver) trans ;
 
+  TransSys.assert_global_constraints trans (SMTSolver.assert_term solver) ;
+
   (* Invariants of the system at 0. *)
   TransSys.invars_of_bound ~one_state_only:true trans Numeral.zero
   |> Term.mk_and

src/induction/step2.ml

@@ -110,6 +110,8 @@ let mk_ctx in_sys param sys =
     (Smt.declare_sort solver)
     Numeral.zero Numeral.(succ one) ;
 
+  TransSys.assert_global_constraints sys (SMTSolver.assert_term solver) ;
+
   (* Invariants of the system at 0, 1 and 2. *)
   add_all_invariants solver sys ;
 

src/interpreter.ml

@@ -178,6 +178,8 @@ let main input_file input_sys _ trans_sys =
     (SMTSolver.declare_sort solver)
     Numeral.(~- one) Numeral.(of_int steps) ;
 
+  TransSys.assert_global_constraints trans_sys (SMTSolver.assert_term solver) ;
+
   (* Assert initial state constraint *)
     SMTSolver.assert_term solver
       (TransSys.init_of_bound (Some (SMTSolver.declare_fun solver))

src/invgen/lockStepDriver.ml

@@ -138,6 +138,7 @@ let mk_base_checker_solver sys k =
     (SMTSolver.declare_sort solver)
     Numeral.zero Numeral.zero ;
 
+  TransSys.assert_global_constraints sys (SMTSolver.assert_term solver) ;
 
   Smt.trace_comment solver (* Logging stuff in smt trace. *)
     "Conditional initial predicate." ;
@@ -540,6 +541,8 @@ let mk_pruning_checker_solver sys two_state =
     (SMTSolver.declare_sort solver)
     Numeral.zero (if two_state then Numeral.one else Numeral.zero);
 
+  TransSys.assert_global_constraints sys (SMTSolver.assert_term solver) ;
+
   Smt.trace_comment solver (* Logging stuff in smt trace. *)
     "Asserting invariants at [0]." ;
 

src/ivcMcs.ml

@@ -885,6 +885,8 @@ let compute_local_cs sys prop_names enter_nodes cex keep test =
     (SMTSolver.declare_sort solver)
     Numeral.zero num_k;
 
+  TransSys.assert_global_constraints sys (SMTSolver.assert_term solver) ;
+
   TS.init_of_bound None sys Numeral.zero
   |> SMTSolver.assert_term solver;
   for i = 0 to (k - 1) do
@@ -1199,6 +1201,8 @@ let compute_unsat_core ?(pathcomp=None) ?(approximate=false)
     )
   else TS.define_subsystems sys (SMTSolver.define_fun solver) ;
 
+  TransSys.assert_global_constraints sys (SMTSolver.assert_term solver) ;
+
   SMTSolver.assert_term solver t |> ignore ;
 
   let check_sat =

src/lustre/assumption.ml

@@ -177,12 +177,16 @@ let dump_contract_for_assumption in_sys scope assumption path contract_name =
 
 let create_assumpion_init fmt_assump sys solver vars fp prop =
 
-  let init = TSys.init_of_bound None sys Numeral.zero in
+  let premise =
+    Term.mk_and
+      ((TransSys.global_constraints sys) @
+       [TSys.init_of_bound None sys Numeral.zero])
+  in
 
   let conclusion = Term.mk_and [prop.Property.prop_term; fp] in
 
   let assump_init =
-    Abduction.abduce_simpl solver vars init conclusion
+    Abduction.abduce_simpl solver vars premise conclusion
     |> SMTSolver.simplify_term solver
   in
 
@@ -201,7 +205,8 @@ let create_assumpion_trans fmt_assump sys solver vars fp prop =
       TransSys.invars_of_bound sys Numeral.one
     in  
     Term.mk_and
-      (TSys.trans_of_bound None sys Numeral.one :: invars)
+      ((TransSys.global_constraints sys) @
+       TSys.trans_of_bound None sys Numeral.one :: invars)
   in
 
   let premises = Term.mk_and [fp ; trans] in
@@ -828,7 +833,7 @@ let generate_assumption_for_k_and_below one_state assump_svars last_abduct sys p
     let system_unrolling =
       if n=0 then
         let init = TSys.init_of_bound None sys Numeral.zero in
-        [init]
+        (TransSys.global_constraints sys) @ [init]
       else
         system_unrolling @ [TSys.trans_of_bound None sys num_n]
     in
@@ -1092,6 +1097,10 @@ let generate_assumption ?(one_state=false) analyze in_sys param sys =
 
 let generate_assumption_vg in_sys sys var_filters prop =
 
+  (* The current implementation does not restrict global free constants.
+     Should we offer a version that allows it?
+  *)
+
   let vars_at_0 =
     TSys.vars_of_bounds ~with_init_flag:true sys Numeral.zero Numeral.zero
     |> List.filter (fun v -> not (Var.is_const_state_var v))

src/lustre/lustreAbstractInterpretation.ml

@@ -169,26 +169,30 @@ let rec restrict_type_by ty restrict = match ty, restrict with
       | (Some Const (_, Num l1)), (Some Const (_, Num l2)) -> 
         let l1 = Numeral.of_string (HString.string_of_hstring l1) in
         let l2 = Numeral.of_string (HString.string_of_hstring l2) in
-        let lnum = Numeral.min l1 l2 in
+        let lnum = Numeral.max l1 l2 in
         let l = HString.mk_hstring (Numeral.string_of_numeral lnum) in
         Some (LA.Const (dpos, Num l)), not (Numeral.equal l1 lnum)
-      | Some _, None -> None, true
-      | _ -> None, false 
+      | (Some _ as l), None -> l, false
+      | None, (Some _ as l) -> l, true 
+      | _ -> None, false
 
     in
     let upper, is_restricted2 = match u1, u2 with 
       | (Some Const (_, Num u1)), (Some Const (_, Num u2)) ->
         let u1 = Numeral.of_string (HString.string_of_hstring u1) in
         let u2 = Numeral.of_string (HString.string_of_hstring u2) in
-        let unum = Numeral.max u1 u2 in
+        let unum = Numeral.min u1 u2 in
         let u = HString.mk_hstring (Numeral.string_of_numeral unum) in
         Some (LA.Const (dpos, Num u)), not (Numeral.equal u1 unum)
-      | Some _, None -> None, true
-      | _ -> None, false 
+      | (Some _ as u), None -> u, false
+      | None, (Some _ as u) -> u, true
+      | _ -> None, false  
     in
     (*IntRange (dpos, lower, upper)*)
     let is_restricted = is_restricted1 || is_restricted2 in
-    IntRange (dpos, lower, upper), is_restricted
+    if (lower = None && upper = None) 
+    then Int dpos, is_restricted
+    else IntRange (dpos, lower, upper), is_restricted
   | IntRange _ as t, Int _ -> t, false
   | Int _, (IntRange _ as t) -> t, true
   | t, _ -> t, false
@@ -400,28 +404,45 @@ and interpret_expr_by_type node_id ctx ty_ctx ty proj expr : LA.lustre_type =
     | Some l2, Some r2 ->
       let l, r = Numeral.max l1 l2, Numeral.min r1 r2 in
       subrange_from_bounds pos l r
+    | Some l2, None ->
+      let l = Numeral.max l1 l2 in 
+      subrange_from_bounds pos l r1
+    | None, Some r2 ->
+      let r = Numeral.min r1 r2 in 
+      subrange_from_bounds pos l1 r
     | _ -> t)
   | IntRange (pos, (Some Const (_, Num l1)), None) as t ->
     let l1 = Numeral.of_string (HString.string_of_hstring l1) in
-    let l2, _ = interpret_int_expr node_id ctx ty_ctx proj expr in
-    (match l2  with
-    | Some l2 ->
-      let l  = Numeral.max l1 l2  in
+    let l2, r2 = interpret_int_expr node_id ctx ty_ctx proj expr in
+    (match l2, r2  with
+    | Some l2, Some r2 ->
+      let l = Numeral.max l1 l2 in
+      subrange_from_bounds pos l r2
+    | Some l2, None ->
+      let l = Numeral.max l1 l2 in 
       subrange_from_lower pos l 
+    | None, Some r2 ->
+      subrange_from_bounds pos l1 r2
     | _ -> t)
   | IntRange (pos, None, (Some Const (_, Num r1))) as t ->
     let r1 = Numeral.of_string (HString.string_of_hstring r1) in
-    let _, r2 = interpret_int_expr node_id ctx ty_ctx proj expr in
-    (match r2 with
-    | Some r2 ->
+    let l2, r2 = interpret_int_expr node_id ctx ty_ctx proj expr in
+    (match l2, r2 with
+    | Some l2, Some r2 ->
       let r = Numeral.min r1 r2 in
+      subrange_from_bounds pos l2 r
+    | Some l2, None ->
+      subrange_from_bounds pos l2 r1
+    | None, Some r2 ->
+      let r = Numeral.min r1 r2 in 
       subrange_from_upper pos r
     | _ -> t)
-  | IntRange (_, None, None) as t -> t
-  | Int pos | IntRange (pos, _, _) ->
+  | Int pos | IntRange (pos, None, None) ->
     let l, r = interpret_int_expr node_id ctx ty_ctx proj expr in
     (match l, r with
     | Some l, Some r -> subrange_from_bounds pos l r
+    | Some l, None -> subrange_from_lower pos l
+    | None, Some r -> subrange_from_upper pos r
     | _ -> LA.Int dpos)
   | t -> t
 

src/lustre/lustreAstInlineConstants.ml

@@ -212,8 +212,8 @@ and eval_comp_op: TC.tc_context -> LA.comparison_operator
   | Neq -> R.ok (v1 <> v2)
   | Lte -> R.ok (v1 <= v2)
   | Lt -> R.ok (v1 < v2)
-  | Gte -> R.ok (v1 > v2)
-  | Gt -> R.ok (v1 >= v2)
+  | Gte -> R.ok (v1 >= v2)
+  | Gt -> R.ok (v1 > v2)
 (** try and evalutate comparison op expression to bool, return error otherwise *)
 
 and simplify_array_index: TC.tc_context -> Lib.position -> LA.expr -> LA.expr -> LA.expr

src/lustre/lustreDeclarations.ml

@@ -2405,7 +2405,8 @@ let declarations_to_nodes decls =
 
   (* Return nodes in context *)
   C.get_nodes ctx, { G.free_constants = C.get_free_constants ctx;
-                     G.state_var_bounds = C.get_state_var_bounds ctx }
+                     G.state_var_bounds = C.get_state_var_bounds ctx;
+                     G.global_constraints = [] (* Not implemented *)}
 
 
 (*

src/lustre/lustreGlobals.ml

@@ -29,5 +29,7 @@ type t =
     (* register bounds of state variables for later use *)
     state_var_bounds : (E.expr E.bound_or_fixed list) StateVar.StateVarHashtbl.t;
 
+    (* Constraints on free constants *)
+    global_constraints: E.t list;
   }
 

src/lustre/lustreGlobals.mli

@@ -30,5 +30,8 @@ type t =
       (LustreExpr.expr LustreExpr.bound_or_fixed list)
         StateVar.StateVarHashtbl.t;
     (** Register bounds of state variables for later use *)
+
+    global_constraints: LustreExpr.t list;
+    (** Constraints on free constants *)
   }