From 75f2476496c8c2958279a2603b55d7e3d40a6a1f Mon Sep 17 00:00:00 2001 From: Daniel Larraz Date: Tue, 3 Oct 2023 12:15:28 -0500 Subject: [PATCH 1/8] Update lexing and parsing to accept 'param' keyword Co-authored-by: Rob Lorch --- src/lustre/lustreLexer.mll | 3 ++- src/lustre/lustreParser.messages | 36 ++++++++++++++++++++++++++++++++ src/lustre/lustreParser.mly | 25 +++++++++++++++++++++- 3 files changed, 62 insertions(+), 2 deletions(-) diff --git a/src/lustre/lustreLexer.mll b/src/lustre/lustreLexer.mll index 00dd29ba3..2c81c31ab 100644 --- a/src/lustre/lustreLexer.mll +++ b/src/lustre/lustreLexer.mll @@ -240,8 +240,9 @@ let keyword_table = mk_hashtbl [ "struct", STRUCT ; "enum", ENUM ; - (* Constant declaration *) + (* Constant/parameter declaration *) "const", CONST ; + "param", PARAM ; (* Node / function declaration *) "imported", IMPORTED ; diff --git a/src/lustre/lustreParser.messages b/src/lustre/lustreParser.messages index 28f5896cb..5416d5642 100644 --- a/src/lustre/lustreParser.messages +++ b/src/lustre/lustreParser.messages @@ -2951,3 +2951,39 @@ Syntax Error! main: FUNCTION ASSUME LPAREN RPAREN RETURNS LPAREN RPAREN LET ASSERT CHOOSE ASSUME RPARAMBRACKET Syntax Error! + +main: PARAM XOR + +Syntax Error! + +main: PARAM ASSUME COLON ASSUME SEMICOLON XOR + +Syntax Error! + +main: PARAM ASSUME XOR + +Syntax Error! + +main: PARAM ASSUME COMMA XOR + +Syntax Error! + +main: PARAM ASSUME COMMA ASSUME SEMICOLON + +Syntax Error! + +main: PARAM ASSUME COMMA ASSUME COLON XOR + +Syntax Error! + +main: PARAM ASSUME COMMA ASSUME COLON ASSUME AND + +Syntax Error! + +main: PARAM ASSUME COLON XOR + +Syntax Error! + +main: PARAM ASSUME COLON ASSUME AND + +Syntax Error! diff --git a/src/lustre/lustreParser.mly b/src/lustre/lustreParser.mly index 60dcd6dbe..337eefb34 100644 --- a/src/lustre/lustreParser.mly +++ b/src/lustre/lustreParser.mly @@ -82,8 +82,9 @@ let mk_span start_pos end_pos = %token DOTDOT %token BAR -(* Token for constant declarations *) +(* Token for constant/parameter declarations *) %token CONST +%token PARAM (* Tokens for node declarations *) %token IMPORTED @@ -241,6 +242,9 @@ decl: | d = const_decl { List.map (function e -> A.ConstDecl (mk_span $startpos $endpos, e)) d } + | d = param_decl { List.map + (function e -> A.ConstDecl (mk_span $startpos $endpos, e)) + d } | d = type_decl { List.map (function e -> A.TypeDecl (mk_span $startpos $endpos, e)) d } @@ -272,6 +276,9 @@ decl: (* A constant declaration *) const_decl: CONST; l = nonempty_list(const_decl_body) { List.flatten l } +(* A constant declaration *) +param_decl: PARAM; l = nonempty_list(param_decl_body) { List.flatten l } + (* The body of a constant declaration *) const_decl_body: @@ -293,6 +300,19 @@ const_decl_body: | c = typed_ident; EQUALS; e = expr; SEMICOLON { let (_, s, t) = c in [A.TypedConst (mk_pos $startpos, s, e, t)] } +(* The body of a parameter declaration *) +param_decl_body: + + (* Imported (free) constant + + Separate rule for singleton list to avoid shift/reduce conflict *) + | h = ident; COLON; t = lustre_type; SEMICOLON + { [A.FreeConst (mk_pos $startpos, h, t)] } + + (* Imported (free) constant *) + | h = ident; COMMA; l = ident_list; COLON; t = lustre_type; SEMICOLON + { List.map (function e -> A.FreeConst (mk_pos $startpos, e, t)) (h :: l) } + (* ********************************************************************** *) @@ -555,6 +575,9 @@ node_local_decl: | c = const_decl { List.map (function e -> A.NodeConstDecl (mk_pos $startpos, e)) c } + | p = param_decl { List.map + (function e -> A.NodeConstDecl (mk_pos $startpos, e)) + p } | v = var_decls { List.map (function e -> A.NodeVarDecl (mk_pos $startpos, e)) v } From cfb5c79369d0f52a64f167acb31247b55fc77db8 Mon Sep 17 00:00:00 2001 From: Daniel Larraz Date: Wed, 4 Oct 2023 10:25:26 -0500 Subject: [PATCH 2/8] Create and store param subrange constraints --- src/certif/certifChecker.ml | 5 +++-- src/certif/jkindParser.ml | 5 +++-- src/lustre/lustreDeclarations.ml | 3 ++- src/lustre/lustreGlobals.ml | 2 ++ src/lustre/lustreGlobals.mli | 3 +++ src/lustre/lustreNodeGen.ml | 37 ++++++++++++++++++++++++++------ src/lustre/lustreTransSys.ml | 7 ++++++ src/nativeInput.ml | 3 ++- src/terms/type.mli | 2 +- src/transSys.ml | 9 ++++++++ src/transSys.mli | 14 +++++++++++- 11 files changed, 75 insertions(+), 15 deletions(-) diff --git a/src/certif/certifChecker.ml b/src/certif/certifChecker.ml index a57be8f21..8196c3c04 100644 --- a/src/certif/certifChecker.ml +++ b/src/certif/certifChecker.ml @@ -2517,8 +2517,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 diff --git a/src/certif/jkindParser.ml b/src/certif/jkindParser.ml index 68a5e6225..8897e9304 100644 --- a/src/certif/jkindParser.ml +++ b/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 diff --git a/src/lustre/lustreDeclarations.ml b/src/lustre/lustreDeclarations.ml index 3b40fbae2..c0231dd5a 100644 --- a/src/lustre/lustreDeclarations.ml +++ b/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 *)} (* diff --git a/src/lustre/lustreGlobals.ml b/src/lustre/lustreGlobals.ml index 50e443191..608c8df0a 100644 --- a/src/lustre/lustreGlobals.ml +++ b/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; } diff --git a/src/lustre/lustreGlobals.mli b/src/lustre/lustreGlobals.mli index 9316fdfba..a43a7a204 100644 --- a/src/lustre/lustreGlobals.mli +++ b/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 *) } diff --git a/src/lustre/lustreNodeGen.ml b/src/lustre/lustreNodeGen.ml index e8f15331c..bfe384534 100644 --- a/src/lustre/lustreNodeGen.ml +++ b/src/lustre/lustreNodeGen.ml @@ -56,6 +56,7 @@ type compiler_state = { other_constants : LustreAst.expr StringMap.t; state_var_bounds : (LustreExpr.expr LustreExpr.bound_or_fixed list) StateVar.StateVarHashtbl.t; + global_constraints: LustreExpr.t list; } type identifier_maps = { @@ -132,6 +133,7 @@ let empty_compiler_state () = { free_constants = []; other_constants = StringMap.empty; state_var_bounds = SVT.create 7; + global_constraints = []; } (* @@ -575,7 +577,8 @@ let rec compile ctx gids decls = in output.nodes, { G.free_constants = free_constants; - G.state_var_bounds = output.state_var_bounds} + G.state_var_bounds = output.state_var_bounds; + G.global_constraints = output.global_constraints } and compile_ast_type ?(expand=false) @@ -2201,11 +2204,24 @@ and compile_node_decl gids is_function cstate ctx i ext inputs outputs locals it 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) -> let ident = mk_ident i in let cty = compile_ast_type cstate ctx map ty in - let over_index = fun i ty vt -> + let over_index = fun i ty (vt, global_constraints) -> let possible_state_var = mk_state_var ?is_input:(Some false) ?is_const:(Some true) @@ -2219,13 +2235,20 @@ 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 - | None -> vt + 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) in - let vt = X.fold over_index cty X.empty in if ghost then cstate - else { cstate - with free_constants = (!map.node_name, i, vt) :: cstate.free_constants } + else ( + { cstate with + free_constants = (!map.node_name, i, vt) :: cstate.free_constants; + global_constraints + } + ) (* TODO: Old code does some subtyping checks for Typed constants Otherwise these other constants are used only for constant propagation *) | A.UntypedConst (_, id, expr) diff --git a/src/lustre/lustreTransSys.ml b/src/lustre/lustreTransSys.ml index 4c94abb85..9c725cd37 100644 --- a/src/lustre/lustreTransSys.ml +++ b/src/lustre/lustreTransSys.ml @@ -2154,6 +2154,12 @@ let rec trans_sys_of_node' ) stateful_vars in + let global_constraints = + List.map + (E.base_term_of_t TransSys.init_base) + globals.G.global_constraints + in + (* Order initial state equations by dependency and generate terms *) let init_terms, svar_dep_init, node_output_input_dep_init = @@ -2412,6 +2418,7 @@ let rec trans_sys_of_node' unconstrained_inputs globals.G.state_var_bounds global_consts + global_constraints ufs init_uf_symbol init_formals diff --git a/src/nativeInput.ml b/src/nativeInput.ml index 749194ccd..698164bfc 100644 --- a/src/nativeInput.ml +++ b/src/nativeInput.ml @@ -482,7 +482,8 @@ let of_channel in_ch = state_vars StateVar.StateVarSet.empty (* underapproximation *) (StateVar.StateVarHashtbl.create 7) - [] + [] (* global consts *) + [] (* global constraints *) [] (* ufs *) init_uf_symbol init_args diff --git a/src/terms/type.mli b/src/terms/type.mli index 8c653e882..2daaee239 100644 --- a/src/terms/type.mli +++ b/src/terms/type.mli @@ -188,7 +188,7 @@ val bounds_of_int_range : t -> (Numeral.t option * Numeral.t option) (** Return bounds of an enum type, fail with [Invalid_argument "bounds_of_enum"] if the type is not an integer range type. *) - val bounds_of_enum : t -> (Numeral.t * Numeral.t) +val bounds_of_enum : t -> (Numeral.t * Numeral.t) (** Generalize a type (remove actual intranges) *) diff --git a/src/transSys.ml b/src/transSys.ml index 8f8cf4481..0e91b4967 100644 --- a/src/transSys.ml +++ b/src/transSys.ml @@ -97,6 +97,8 @@ type t = global_consts : Var.t list; (** List of global free constants *) + global_constraints : Term.t list; + state_vars : StateVar.t list; (** State variables in the scope of this transition system @@ -478,6 +480,8 @@ let collect_instances ({ scope } as trans_sys) = (* Access the transition system *) (* ********************************************************************** *) +let global_constraints { global_constraints } = global_constraints + (* Close term by binding variables to terms with a let binding *) let close_term bindings term = if bindings = [] then term else Term.mk_let bindings term @@ -1079,6 +1083,9 @@ let define_and_declare_of_bounds declare_vars_of_bounds trans_sys declare lbound ubound +let assert_global_constraints { global_constraints } assert_term = + List.iter (fun c -> assert_term c) global_constraints + let init_uf_def { init_uf_symbol; init_formals; init } = (init_uf_symbol, (init_formals, init)) @@ -1673,6 +1680,7 @@ let mk_trans_sys unconstrained_inputs state_var_bounds global_consts + global_constraints ufs init_uf_symbol init_formals @@ -1841,6 +1849,7 @@ let mk_trans_sys state_var_bounds; subsystems; global_consts; + global_constraints; ufs; init_uf_symbol; init_formals; diff --git a/src/transSys.mli b/src/transSys.mli index 455d17962..b9d5ab16c 100644 --- a/src/transSys.mli +++ b/src/transSys.mli @@ -124,6 +124,9 @@ val pp_print_trans_sys_name : Format.formatter -> t -> unit (** {1 Accessors} *) +(** Return global constraints on free constants *) +val global_constraints : t -> Term.t list + (** Close the initial state constraint by binding all instance identifiers, and bump the state variable offsets to be at the given bound *) @@ -163,7 +166,6 @@ val init_flag_state_var : t -> StateVar.t (** Return the init flag at the given bound *) val init_flag_of_bound : t -> Numeral.t -> Term.t - (** Return the instance variables of this transition system, the initial state constraint at [init_base] and the transition relation at [trans_base] with the instance variables free. *) @@ -253,6 +255,9 @@ val mk_trans_sys : (* Global free constants *) Var.t list -> + (* Global constraints on free constants *) + Term.t list -> + (* Declarations of other function symbols *) UfSymbol.t list -> @@ -483,6 +488,13 @@ val define_and_declare_of_bounds : (Type.t -> unit) -> Numeral.t -> Numeral.t -> unit +(** [assert_global_constraints t a] uses function [a] to assert + the global constraints of transition system [t] + + The signature of [a] is that of {!SMTSolver.assert_term} + *) +val assert_global_constraints : t -> (Term.t -> unit) -> unit + (** Return predicate definitions of initial state and transition relation of the top system and all its subsystem in reverse topological order From 2c4eeaaaa631c4aa8f7925abb227112886d03313 Mon Sep 17 00:00:00 2001 From: Rob Lorch Date: Wed, 4 Oct 2023 13:44:28 -0500 Subject: [PATCH 3/8] Abstract interpretation int range fixes --- src/lustre/lustreAbstractInterpretation.ml | 52 +++++++++++++++------- 1 file changed, 37 insertions(+), 15 deletions(-) diff --git a/src/lustre/lustreAbstractInterpretation.ml b/src/lustre/lustreAbstractInterpretation.ml index cadc1bc6f..c0bfc88b2 100644 --- a/src/lustre/lustreAbstractInterpretation.ml +++ b/src/lustre/lustreAbstractInterpretation.ml @@ -151,26 +151,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 @@ -381,28 +385,46 @@ 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 l r + | Some l2, None -> + let l = Numeral.max l1 l2 in + subrange_from_bounds l r1 + | None, Some r2 -> + let r = Numeral.min r1 r2 in + subrange_from_bounds l1 r | _ -> t) | IntRange (_, (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 l r2 + | Some l2, None -> + let l = Numeral.max l1 l2 in subrange_from_lower l + | None, Some r2 -> + subrange_from_bounds l1 r2 | _ -> t) | IntRange (_, 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 l2 r + | Some l2, None -> + subrange_from_bounds l2 r1 + | None, Some r2 -> + let r = Numeral.min r1 r2 in subrange_from_upper r | _ -> t) - | IntRange (_, None, None) as t -> t + | IntRange (pos, None, None) -> Int pos | Int _ | IntRange _ -> 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 l r + | Some l, None -> subrange_from_lower l + | None, Some r -> subrange_from_upper r | _ -> LA.Int dpos) | t -> t From 73bb7a282ecba0fa84b5650176f526c4acd859a6 Mon Sep 17 00:00:00 2001 From: Rob Lorch Date: Wed, 4 Oct 2023 13:47:19 -0500 Subject: [PATCH 4/8] Remove unused pattern match --- src/lustre/lustreAbstractInterpretation.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/lustre/lustreAbstractInterpretation.ml b/src/lustre/lustreAbstractInterpretation.ml index c0bfc88b2..64dd35606 100644 --- a/src/lustre/lustreAbstractInterpretation.ml +++ b/src/lustre/lustreAbstractInterpretation.ml @@ -419,7 +419,7 @@ and interpret_expr_by_type node_id ctx ty_ctx ty proj expr : LA.lustre_type = subrange_from_upper r | _ -> t) | IntRange (pos, None, None) -> Int pos - | Int _ | IntRange _ -> + | Int _ -> 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 l r From 6ac7eee114e8a1d30be86a4887aa66fd3958dc7e Mon Sep 17 00:00:00 2001 From: Daniel Larraz Date: Wed, 4 Oct 2023 15:50:18 -0500 Subject: [PATCH 5/8] Use param subrange constraints in analyses --- src/c2i/C2I.ml | 6 +++++ src/certif/certifChecker.ml | 11 +++++++++- src/ic3/IC3.ml | 10 ++++++--- src/ic3ia/IC3IA.ml | 6 +++-- src/induction/base.ml | 2 ++ src/induction/step.ml | 2 ++ src/induction/step2.ml | 2 ++ src/interpreter.ml | 2 ++ src/invgen/lockStepDriver.ml | 3 +++ src/ivcMcs.ml | 4 ++++ src/lustre/assumption.ml | 17 ++++++++++---- src/realizability.ml | 7 +++++- src/testgen/testgenSolver.ml | 2 ++ src/transSys.ml | 22 ++++++++++++++++++- src/transSys.mli | 2 ++ .../success/param_type_constraint.lus | 10 +++++++++ 16 files changed, 96 insertions(+), 12 deletions(-) create mode 100644 tests/regression/success/param_type_constraint.lus diff --git a/src/c2i/C2I.ml b/src/c2i/C2I.ml index 009b17cdd..6e81a48e2 100644 --- a/src/c2i/C2I.ml +++ b/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 ; diff --git a/src/certif/certifChecker.ml b/src/certif/certifChecker.ml index 8196c3c04..925bb5cc8 100644 --- a/src/certif/certifChecker.ml +++ b/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 *) diff --git a/src/ic3/IC3.ml b/src/ic3/IC3.ml index 8f6de26c6..85a912dcb 100644 --- a/src/ic3/IC3.ml +++ b/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 diff --git a/src/ic3ia/IC3IA.ml b/src/ic3ia/IC3IA.ml index 68e97553c..6bbe6e20e 100644 --- a/src/ic3ia/IC3IA.ml +++ b/src/ic3ia/IC3IA.ml @@ -112,7 +112,8 @@ 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 = @@ -120,12 +121,13 @@ let sys_def_unrolling solver sys 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 diff --git a/src/induction/base.ml b/src/induction/base.ml index d97c91905..e5a3b28ed 100644 --- a/src/induction/base.ml +++ b/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 diff --git a/src/induction/step.ml b/src/induction/step.ml index 6e36de522..408f34711 100644 --- a/src/induction/step.ml +++ b/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 diff --git a/src/induction/step2.ml b/src/induction/step2.ml index b5fae5873..bbe54691d 100644 --- a/src/induction/step2.ml +++ b/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 ; diff --git a/src/interpreter.ml b/src/interpreter.ml index d7f932db0..fe7a31715 100644 --- a/src/interpreter.ml +++ b/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)) diff --git a/src/invgen/lockStepDriver.ml b/src/invgen/lockStepDriver.ml index b6591e66b..76578c7a3 100644 --- a/src/invgen/lockStepDriver.ml +++ b/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]." ; diff --git a/src/ivcMcs.ml b/src/ivcMcs.ml index 441746374..2f81f8e7d 100644 --- a/src/ivcMcs.ml +++ b/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 = diff --git a/src/lustre/assumption.ml b/src/lustre/assumption.ml index a417a0864..fa0eb9d9e 100644 --- a/src/lustre/assumption.ml +++ b/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)) diff --git a/src/realizability.ml b/src/realizability.ml index 0992c40e1..4829cf659 100644 --- a/src/realizability.ml +++ b/src/realizability.ml @@ -206,7 +206,10 @@ let realizability_check ?(include_invariants=false) vars_of_term let free_of_controllable_vars_at_0, contains_controllable_vars_at_0 = let init = TSys.init_of_bound None sys Numeral.zero in - term_partition controllable_vars_at_0 (get_conjucts init) + let constraints_at_0 = + (TransSys.global_constraints sys) @ (get_conjucts init) + in + term_partition controllable_vars_at_0 constraints_at_0 in let rec loop fp1 fp = @@ -742,6 +745,8 @@ let compute_deadlocking_trace_and_conflict (neg_vr :: (cex_assigns @ guarantee_mode_elts_term @ other_term)) in + TransSys.assert_global_constraints sys (SMTSolver.assert_term solver) ; + SMTSolver.assert_term solver constraints ; (*let cex', conflict_set = diff --git a/src/testgen/testgenSolver.ml b/src/testgen/testgenSolver.ml index fe5cbe3bc..63a1a919f 100644 --- a/src/testgen/testgenSolver.ml +++ b/src/testgen/testgenSolver.ml @@ -80,6 +80,8 @@ let mk sys = term_of_actlit fresh in + TransSys.assert_global_constraints sys (SMTSolver.assert_term solver) ; + (* Asserting init conditionally. *) S.trace_comment solver "|===| Conditional init." ; Term.mk_implies [ actlit ; diff --git a/src/transSys.ml b/src/transSys.ml index 0e91b4967..fc1a79ee6 100644 --- a/src/transSys.ml +++ b/src/transSys.ml @@ -548,6 +548,13 @@ let rec set_subsystem_equations t scope init trans = in { t with init; trans; subsystems } +let rec set_global_constraints t global_constraints = + let aux (t, instances) = + (set_global_constraints t global_constraints, instances) + in + let subsystems = List.map aux t.subsystems in + { t with subsystems ; global_constraints } + (* Return the state variable for the init flag *) let init_flag_state_var { init_flag_state_var } = init_flag_state_var @@ -2064,7 +2071,20 @@ let enforce_constantness_via_equations sys = in Term.mk_and (trans_eq :: eqs) in - set_subsystem_equations sys (scope_of_trans_sys sys) init_eq trans_eq + let sys' = + set_subsystem_equations sys (scope_of_trans_sys sys) init_eq trans_eq + in + let global = + global_constraints sys |> List.map (fun c -> + c |> Term.map_vars (fun v -> + let sv = Var.state_var_of_state_var_instance v in + if List.mem sv const_svars then + Var.mk_state_var_instance sv Numeral.zero + else + v) + ) + in + set_global_constraints sys' global ) in sys', const_svars diff --git a/src/transSys.mli b/src/transSys.mli index b9d5ab16c..601ab8356 100644 --- a/src/transSys.mli +++ b/src/transSys.mli @@ -174,6 +174,8 @@ val init_trans_open : t -> StateVar.t list * Term.t * Term.t (** Update the init and trans equations of a subsystem *) val set_subsystem_equations : t -> Scope.t -> Term.t -> Term.t -> t +val set_global_constraints : t -> Term.t list -> t + (** Set the logic of the transition system *) val set_logic : t -> TermLib.logic -> t diff --git a/tests/regression/success/param_type_constraint.lus b/tests/regression/success/param_type_constraint.lus new file mode 100644 index 000000000..8b9570670 --- /dev/null +++ b/tests/regression/success/param_type_constraint.lus @@ -0,0 +1,10 @@ + +type S = subrange [0,1] of int; + +const C: S; + +node N() returns (x: int); +let + x = 2 + C; + check x<4; +tel From 4b7fcc6605d494f775b02544303a701539d50117 Mon Sep 17 00:00:00 2001 From: Daniel Larraz Date: Wed, 4 Oct 2023 16:26:32 -0500 Subject: [PATCH 6/8] Add param enum constraints --- src/lustre/lustreTransSys.ml | 47 ++++++++++++------- .../success/param_type_constraint.lus | 5 +- 2 files changed, 35 insertions(+), 17 deletions(-) diff --git a/src/lustre/lustreTransSys.ml b/src/lustre/lustreTransSys.ml index 9c725cd37..25c7e0569 100644 --- a/src/lustre/lustreTransSys.ml +++ b/src/lustre/lustreTransSys.ml @@ -2031,17 +2031,19 @@ let rec trans_sys_of_node' ) in + let filter_enum_svars = + List.filter (fun state_var -> + let state_var_type = StateVar.type_of_state_var state_var in + if Type.is_array state_var_type then + let base_type = Type.last_elem_type_of_array state_var_type in + Type.is_enum base_type + else + Type.is_enum state_var_type + ) + in + let subrange_and_enum_state_vars = - let enum_state_vars = - all_state_vars |> List.filter (fun state_var -> - let state_var_type = StateVar.type_of_state_var state_var in - if Type.is_array state_var_type then - let base_type = Type.last_elem_type_of_array state_var_type in - Type.is_enum base_type - else - Type.is_enum state_var_type - ) - in + let enum_state_vars = filter_enum_svars all_state_vars in (* Inputs, defined outputs, and locals require a check. This is currently done in lustreDeclarations and lustreContext. *) @@ -2146,20 +2148,33 @@ let rec trans_sys_of_node' |> List.rev in - let global_consts_sv = + let global_const_svars = List.map Var.state_var_of_state_var_instance global_consts - |> SVS.of_list in - let stateful_vars = List.filter (fun sv -> - not (SVS.mem sv global_consts_sv) - ) stateful_vars in - + let global_constraints = List.map (E.base_term_of_t TransSys.init_base) globals.G.global_constraints in + let global_constraints = + let enum_consts = filter_enum_svars global_const_svars in + List.fold_left + (add_constraints_of_type true) + global_constraints + enum_consts + in + + let stateful_vars = + let global_const_svars = + SVS.of_list global_const_svars + in + List.filter + (fun sv -> not (SVS.mem sv global_const_svars)) + stateful_vars + in + (* Order initial state equations by dependency and generate terms *) let init_terms, svar_dep_init, node_output_input_dep_init = diff --git a/tests/regression/success/param_type_constraint.lus b/tests/regression/success/param_type_constraint.lus index 8b9570670..4caf65371 100644 --- a/tests/regression/success/param_type_constraint.lus +++ b/tests/regression/success/param_type_constraint.lus @@ -1,10 +1,13 @@ +type AB = enum {A,B}; type S = subrange [0,1] of int; const C: S; +const W: AB; node N() returns (x: int); let x = 2 + C; check x<4; -tel + check W=A or W=B; +tel \ No newline at end of file From 51aef99f64ec78ee1a8a61f639406df059a8bff2 Mon Sep 17 00:00:00 2001 From: Daniel Larraz Date: Thu, 5 Oct 2023 11:28:49 -0500 Subject: [PATCH 7/8] Fix IntRange type without bounds in interpret_expr_by_type --- src/lustre/lustreAbstractInterpretation.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/lustre/lustreAbstractInterpretation.ml b/src/lustre/lustreAbstractInterpretation.ml index 64dd35606..91cec3ffa 100644 --- a/src/lustre/lustreAbstractInterpretation.ml +++ b/src/lustre/lustreAbstractInterpretation.ml @@ -418,8 +418,7 @@ and interpret_expr_by_type node_id ctx ty_ctx ty proj expr : LA.lustre_type = let r = Numeral.min r1 r2 in subrange_from_upper r | _ -> t) - | IntRange (pos, None, None) -> Int pos - | Int _ -> + | Int _ | IntRange _ -> 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 l r From 313c6a9576e82619e1e4bd6a4bad7dfc066c374c Mon Sep 17 00:00:00 2001 From: Daniel Larraz Date: Thu, 5 Oct 2023 12:27:16 -0500 Subject: [PATCH 8/8] Fix evaluation of Gte and Gt in new frontend --- src/lustre/lustreAstInlineConstants.ml | 4 ++-- tests/regression/success/num_const_evaluation.lus | 11 +++++++++++ 2 files changed, 13 insertions(+), 2 deletions(-) create mode 100644 tests/regression/success/num_const_evaluation.lus diff --git a/src/lustre/lustreAstInlineConstants.ml b/src/lustre/lustreAstInlineConstants.ml index 1e57b3a48..2a57510bb 100644 --- a/src/lustre/lustreAstInlineConstants.ml +++ b/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 diff --git a/tests/regression/success/num_const_evaluation.lus b/tests/regression/success/num_const_evaluation.lus new file mode 100644 index 000000000..e18ed3813 --- /dev/null +++ b/tests/regression/success/num_const_evaluation.lus @@ -0,0 +1,11 @@ + +const M: int = 1; + +node main() returns (ok: bool); +let + check "EQ" M = 1; + check "LTE" M <= 1; + check "GTE" M >= 1; + check "LT" not (M < 1); + check "GT" not (M > 1); +tel