From 046d397c66181612061b36555486b604c24fe938 Mon Sep 17 00:00:00 2001 From: alexandrina-k Date: Fri, 21 Apr 2023 16:11:56 +0200 Subject: [PATCH] clean version of records parser w/o records --- ast.mli | 13 +- common/hstring.ml | 5 + common/hstring.mli | 5 + enumerative.ml | 4 +- forward.ml | 8 +- forward.mli | 2 +- murphi.ml | 16 +-- parser.mly | 153 ++++++++--------------- pre.ml | 20 +-- ptree.ml | 160 +++++++++++++----------- ptree.mli | 36 ++++-- smt/alt_ergo.ml | 10 ++ smt/smt_sig.mli | 2 + smt/z3wrapper_fake.ml | 1 + trace.ml | 30 ++--- typing.ml | 277 +++++++++++++++++++++++++----------------- 16 files changed, 405 insertions(+), 337 deletions(-) diff --git a/ast.mli b/ast.mli index f10a6bfc..925a83bf 100644 --- a/ast.mli +++ b/ast.mli @@ -50,11 +50,11 @@ type transition_info = { tr_name : Hstring.t; (** name of the transition *) tr_args : Variable.t list; (** existentially quantified parameters of the transision *) - tr_reqs : SAtom.t; (** guard *) - tr_ureq : (Variable.t * dnf) list; + tr_reqs : SAtom.t * loc; (** guard *) + tr_ureq : (Variable.t * dnf * loc) list; (** global condition of the guard, i.e. universally quantified DNF *) tr_lets : (Hstring.t * Term.t) list; - tr_assigns : (Hstring.t * glob_update) list; (** updates of global variables *) + tr_assigns : (Hstring.t * glob_update * loc) list; (** updates of global variables *) tr_upds : update list; (** updates of arrays *) tr_nondets : Hstring.t list; (** non deterministic updates (only for global variables) *) @@ -72,11 +72,14 @@ type transition = { tr_reset : unit -> unit; } +type type_defs = + | Constructors of (loc * type_constructors) + type system = { globals : (loc * Hstring.t * Smt.Type.t) list; consts : (loc * Hstring.t * Smt.Type.t) list; - arrays : (loc * Hstring.t * (Smt.Type.t list * Smt.Type.t)) list; - type_defs : (loc * type_constructors) list; + arrays : (loc * Hstring.t * (Hstring.t list * Hstring.t)) list; + type_defs : type_defs list; init : loc * Variable.t list * dnf; invs : (loc * Variable.t list * SAtom.t) list; unsafe : (loc * Variable.t list * SAtom.t) list; diff --git a/common/hstring.ml b/common/hstring.ml index e1c3665f..0f289907 100644 --- a/common/hstring.ml +++ b/common/hstring.ml @@ -40,6 +40,11 @@ module HS = struct | [] -> raise Not_found | (y, v) :: l -> if equal x y then v else list_assoc x l + let rec list_assoc_triplet x = function + | [] -> raise Not_found + | (y, v, k) :: l -> if equal x y then v,k else list_assoc_triplet x l + + let rec list_assoc_inv x = function | [] -> raise Not_found | (y, v) :: l -> if equal x v then y else list_assoc_inv x l diff --git a/common/hstring.mli b/common/hstring.mli index c6c2eba1..f2c908bd 100644 --- a/common/hstring.mli +++ b/common/hstring.mli @@ -53,6 +53,11 @@ val list_assoc : t -> (t * 'a) list -> 'a pairs [l]. @raise Not_found if there is no value associated with [x] in the list [l].*) +val list_assoc_triplet: t -> (t * 'a * 'b) list -> 'a * 'b +(** [list_assoc_triplet x l] returns the element associated with [x] in the list of + triplets [l]. + @raise Not_found if there is no value associated with [x] in the list [l].*) + val list_assoc_inv : t -> ('a * t) list -> 'a (** [list_assoc_inv x l] returns the first element which is associated to [x] in the list of pairs [l]. diff --git a/enumerative.ml b/enumerative.ml index ba7190f4..a2df804b 100644 --- a/enumerative.ml +++ b/enumerative.ml @@ -752,7 +752,7 @@ let swts_to_stites env at sigma swts = let assigns_to_actions env sigma acc tr_assigns = List.fold_left - (fun acc (h, gu) -> + (fun acc (h, gu, _) -> let nt = Elem (h, Glob) in match gu with | UTerm t -> @@ -935,7 +935,7 @@ let ordered_fst_subst = function let transitions_to_func_aux procs env reduce acc { tr_info = { tr_args = tr_args; - tr_reqs = reqs; + tr_reqs = (reqs,_); tr_name = name; tr_ureq = ureqs; tr_assigns = assigns; diff --git a/forward.ml b/forward.ml index 6e5982ff..3a1c6376 100644 --- a/forward.ml +++ b/forward.ml @@ -469,7 +469,7 @@ let swts_to_ites at swts sigma = let apply_assigns assigns sigma = List.fold_left - (fun (nsa, terms) (h, gu) -> + (fun (nsa, terms) (h, gu, _) -> let nt = Elem (h, Glob) in let sa = match gu with @@ -510,7 +510,7 @@ let preserve_terms upd_terms sa = let uguard_dnf sigma args tr_args = function | [] -> [] - | [j, dnf] -> + | [j, dnf, _] -> let uargs = List.filter (fun a -> not (H.list_mem a tr_args)) args in List.map (fun i -> List.map (fun sa -> SAtom.subst ((j, i)::sigma) sa) dnf) uargs @@ -523,7 +523,7 @@ let possible_init args init reqs = (* try Prover.check_guard args init reqs; true *) (* with Smt.Unsat _ -> false *) -let possible_guard args all_args tr_args sigma init reqs ureqs = +let possible_guard args all_args tr_args sigma init (reqs,_) ureqs = let reqs = SAtom.subst sigma reqs in possible_init args init reqs && let t_args_ef = @@ -793,7 +793,7 @@ let mkinits procs ({t_init = ia, l_init}) = let instance_of_transition { tr_args = tr_args; - tr_reqs = reqs; + tr_reqs = (reqs,_); tr_name = name; tr_ureq = ureqs; tr_assigns = assigns; diff --git a/forward.mli b/forward.mli index 18213eb8..5abdd806 100644 --- a/forward.mli +++ b/forward.mli @@ -78,4 +78,4 @@ val conflicting_from_trace : t_system -> trace -> SAtom.t list val uguard_dnf : Variable.subst -> Variable.t list -> Variable.t list -> - (Variable.t * SAtom.t list) list -> SAtom.t list list + (Variable.t * SAtom.t list * 'a) list -> SAtom.t list list diff --git a/murphi.ml b/murphi.ml index 2eb35020..14dc4111 100644 --- a/murphi.ml +++ b/murphi.ml @@ -466,7 +466,7 @@ let print_swts ot fmt swts = end -let print_assign fmt (v, up) = +let print_assign fmt (v, up, _) = let tv = Elem (v, Glob) in match up with | UTerm t -> @@ -523,7 +523,7 @@ let rec print_is_other fmt (v, args) = match args with print_is_other (v, ra) -let print_forall_other args fmt (v, dnf) = +let print_forall_other args fmt (v, dnf,_) = let close_forall = print_forall fmt v in print_is_other fmt (v, args); fprintf fmt "(%a)" print_dnf dnf; @@ -537,10 +537,10 @@ let rec print_ureqs args fmt = function fprintf fmt "%a@ &@ %a" (print_forall_other args) u (print_ureqs args) ru -let print_guard fmt { tr_args; tr_reqs; tr_ureq } = +let print_guard fmt { tr_args; tr_reqs = (reqs,_); tr_ureq } = (* fprintf fmt " @["; *) - print_satom fmt tr_reqs; - if tr_ureq <> [] && not(SAtom.is_empty tr_reqs) then fprintf fmt " &@ "; + print_satom fmt reqs; + if tr_ureq <> [] && not(SAtom.is_empty reqs) then fprintf fmt " &@ "; print_ureqs tr_args fmt tr_ureq (* fprintf fmt "@]\n" *) @@ -765,9 +765,9 @@ let ordered_procs_globu = function let ordered_procs_up u = ordered_procs_swts u.up_swts let ordered_procs_trans { tr_info = t } = - ordered_procs_satom t.tr_reqs - || List.exists (fun (_, dnf) -> ordered_procs_dnf dnf) t.tr_ureq - || List.exists (fun (_, gu) -> ordered_procs_globu gu) t.tr_assigns + ordered_procs_satom (fst t.tr_reqs) + || List.exists (fun (_, dnf, _) -> ordered_procs_dnf dnf) t.tr_ureq + || List.exists (fun (_, gu, _) -> ordered_procs_globu gu) t.tr_assigns || List.exists ordered_procs_up t.tr_upds let ordered_procs_sys s = diff --git a/parser.mly b/parser.mly index 29a5489f..df18a705 100644 --- a/parser.mly +++ b/parser.mly @@ -24,7 +24,7 @@ (* Helper functions for location info *) - + let loc () = (symbol_start_pos (), symbol_end_pos ()) let loc_i i = (rhs_start_pos i, rhs_end_pos i) let loc_ij i j = (rhs_start_pos i, rhs_end_pos j) @@ -109,10 +109,12 @@ %right OR %right AND %nonassoc prec_ite -/* %left prec_relation EQ NEQ LT LE GT GE */ -/* %left PLUS MINUS */ + /* %left prec_relation EQ NEQ LT LE GT GE */ +%left PLUS MINUS +%left TIMES %nonassoc NOT -/* %left BAR */ + /* %left BAR */ +%left DOT %type system %start system @@ -128,7 +130,7 @@ EOF Smt.set_sum true; let b = [Hstring.make "@MTrue"; Hstring.make "@MFalse"] in List.iter Constructors.add b; - let ptype_defs = (loc (), (Hstring.make "mbool", b)) :: ptype_defs in + let ptype_defs = Constructors ((loc (), (Hstring.make "mbool", b))) :: ptype_defs in let pconsts, pglobals, parrays = $3 in psystem_of_decls ~pglobals ~pconsts ~parrays ~ptype_defs $4 |> encode_psystem @@ -200,13 +202,14 @@ size_proc: | { () } | SIZEPROC INT { Options.size_proc := Num.int_of_num $2 } ; + type_def: - | TYPE lident { (loc (), ($2, [])) } + | TYPE lident { Constructors ((loc (), ($2, []))) } | TYPE lident EQ constructors - { Smt.set_sum true; List.iter Constructors.add $4; (loc (), ($2, $4)) } + { Smt.set_sum true; List.iter Constructors.add $4; Constructors ((loc (), ($2, $4))) } | TYPE lident EQ BAR constructors - { Smt.set_sum true; List.iter Constructors.add $5; (loc (), ($2, $5)) } + { Smt.set_sum true; List.iter Constructors.add $5; Constructors ((loc (), ($2, $5))) } ; constructors: @@ -254,7 +257,7 @@ let_assigns_nondets_updates: | assigns_nondets_updates { [], $1 } | LET lident EQ term IN let_assigns_nondets_updates { let lets, l = $6 in - ($2, $4) :: lets, l} + ($2, TTerm $4) :: lets, l} ; assigns_nondets_updates: @@ -262,7 +265,7 @@ assigns_nondets_updates: | assign_nondet_update { match $1 with - | Assign (x, y) -> [x, y], [], [] + | Assign (x, y) -> [x, y,loc()], [], [] | Nondet x -> [], [x], [] | Upd x -> [], [], [x] } @@ -270,7 +273,7 @@ assigns_nondets_updates: { let assigns, nondets, upds = $3 in match $1 with - | Assign (x, y) -> (x, y) :: assigns, nondets, upds + | Assign (x, y) -> (x, y, loc()) :: assigns, nondets, upds | Nondet x -> assigns, x :: nondets, upds | Upd x -> assigns, nondets, x :: upds } @@ -283,31 +286,18 @@ assign_nondet_update: ; assignment: - | mident AFFECT term - { - if Consts.mem $1 then raise Parsing.Parse_error; - Assign ($1, PUTerm $3) - } - | mident AFFECT CASE switchs - { Assign ($1, PUCase $4) } + | mident AFFECT term { Assign ($1, PUTerm (TTerm $3)) } + | mident AFFECT CASE switchs { Assign ($1, PUCase $4) } ; nondet: - | mident AFFECT DOT - { - if Consts.mem $1 then raise Parsing.Parse_error; - Nondet $1 - } - | mident AFFECT QMARK - { - if Consts.mem $1 then raise Parsing.Parse_error; - Nondet $1 - } + | mident AFFECT DOT { Nondet $1 } + | mident AFFECT QMARK { Nondet $1 } ; require: - | { PAtom (AAtom (Atom.True)) } - | REQUIRE LEFTBR expr RIGHTBR { $3 } + | { PAtom (AAtom (Atom.True)),loc() } + | REQUIRE LEFTBR expr RIGHTBR { $3,loc() } ; update: @@ -325,84 +315,44 @@ update: c :: cube, j :: rjs) ([], []) $3 in let a = PAnd cube in let js = List.rev rjs in - let sw = [(a, $6); (PAtom (AAtom Atom.True), TTerm (Access($1, js)))] in + let sw = [(a, TTerm $6); (PAtom (AAtom Atom.True), TTerm (Access($1, js)))] in Upd { pup_loc = loc (); pup_arr = $1; pup_arg = js; pup_swts = sw} } + ; switchs: - | BAR UNDERSCORE COLON term { [(PAtom (AAtom (Atom.True)), $4)] } + | BAR UNDERSCORE COLON term { [(PAtom (AAtom (Atom.True)), TTerm $4)] } | BAR switch { [$2] } | BAR switch switchs { $2::$3 } ; switch: - | expr COLON term { $1, $3 } + | expr COLON term { $1, TTerm $3 } ; + -constnum: - | REAL { ConstReal $1 } - | INT { ConstInt $1 } -; - -var_term: - | mident { - if Consts.mem $1 then Const (MConst.add (ConstName $1) 1 MConst.empty) - else Elem ($1, sort $1) } +term: + | REAL { Const (MConst.add (ConstReal $1) 1 MConst.empty) } + | INT { Const (MConst.add (ConstInt $1) 1 MConst.empty) } | proc_name { Elem ($1, Var) } -; - -top_id_term: - | var_term { match $1 with - | Elem (v, Var) -> TVar v - | _ -> TTerm $1 } -; - - -array_term: - | mident LEFTSQ proc_name_list_plus RIGHTSQ { - Access ($1, $3) - } -; + | mident { + let t = if Consts.mem $1 then Const (MConst.add (ConstName $1) 1 MConst.empty) + else Elem ($1, sort $1) in t + } + | mident LEFTSQ proc_name_list_plus RIGHTSQ { Access ($1, $3) } -var_or_array_term: - | var_term { $1 } - | array_term { $1 } -; - -arith_term: - | var_or_array_term PLUS constnum - { Arith($1, MConst.add $3 1 MConst.empty) } - | var_or_array_term MINUS constnum - { Arith($1, MConst.add $3 (-1) MConst.empty) } - | var_or_array_term PLUS mident - { - if not (Consts.mem $3) then raise Parsing.Parse_error; - Arith($1, MConst.add (ConstName $3) 1 MConst.empty) - } - | var_or_array_term PLUS INT TIMES mident - { Arith($1, MConst.add (ConstName $5) (Num.int_of_num $3) MConst.empty) } - | var_or_array_term PLUS mident TIMES INT - { Arith($1, MConst.add (ConstName $3) (Num.int_of_num $5) MConst.empty) } - | var_or_array_term MINUS mident - { Arith($1, MConst.add (ConstName $3) (-1) MConst.empty) } - | var_or_array_term MINUS INT TIMES mident - { Arith($1, MConst.add (ConstName $5) (- (Num.int_of_num $3)) MConst.empty) } - | var_or_array_term MINUS mident TIMES INT - { Arith($1, MConst.add (ConstName $3) (- (Num.int_of_num $5)) MConst.empty) } - | INT TIMES mident - { Const(MConst.add (ConstName $3) (Num.int_of_num $1) MConst.empty) } - | MINUS INT TIMES mident - { Const(MConst.add (ConstName $4) (- (Num.int_of_num $2)) MConst.empty) } - | constnum { Const (MConst.add $1 1 MConst.empty) } + /*| MINUS term { UnOp(UMinus, $2) } + | term PLUS term { BinOp($1, Addition, $3) } + | term MINUS term { BinOp($1, Subtraction, $3) } + | term TIMES term { BinOp($1, Multiplication, $3) }*/ + + | term PLUS INT { Arith($1, MConst.add (ConstInt $3) 1 MConst.empty) } + | term PLUS mident { Arith($1, MConst.add (ConstName $3) 1 MConst.empty) } + | term MINUS INT { Arith($1, MConst.add (ConstInt $3) (-1) MConst.empty) } + | term MINUS mident { Arith($1, MConst.add (ConstName $3) (-1) MConst.empty) } ; -term: - | top_id_term { $1 } - | array_term { TTerm $1 } - | arith_term { Smt.set_arith true; TTerm $1 } - ; - lident: | LIDENT { Hstring.make $1 } ; @@ -465,12 +415,12 @@ literal: | TRUE { AAtom Atom.True } | FALSE { AAtom Atom.False } /* | lident { AVar $1 } RR conflict with proc_name */ - | term EQ term { AEq ($1, $3) } - | term NEQ term { ANeq ($1, $3) } - | term LT term { Smt.set_arith true; ALt ($1, $3) } - | term LE term { Smt.set_arith true; ALe ($1, $3) } - | term GT term { Smt.set_arith true; ALt ($3, $1) } - | term GE term { Smt.set_arith true; ALe ($3, $1) } + | term EQ term { AEq (TTerm $1, TTerm $3) } + | term NEQ term { ANeq (TTerm $1, TTerm $3) } + | term LT term { Smt.set_arith true; ALt (TTerm $1, TTerm $3) } + | term LE term { Smt.set_arith true; ALe (TTerm $1, TTerm $3) } + | term GT term { Smt.set_arith true; ALt (TTerm $3, TTerm $1) } + | term GE term { Smt.set_arith true; ALe (TTerm $3, TTerm $1) } ; expr: @@ -494,11 +444,12 @@ simple_expr: ; - expr_or_term_comma_list: | { [] } - | term { [PT $1] } + | term { [PT (TTerm $1)] } | expr { [PF $1] } - | term COMMA expr_or_term_comma_list { PT $1 :: $3 } + | term COMMA expr_or_term_comma_list { PT (TTerm $1) :: $3 } | expr COMMA expr_or_term_comma_list { PF $1 :: $3 } ; + + diff --git a/pre.ml b/pre.ml index aadc7683..0b86cbfd 100644 --- a/pre.ml +++ b/pre.ml @@ -103,7 +103,8 @@ let rec find_update a li = function exception Remove_lit_var of Hstring.t -let rec find_assign memo tr = function +let rec find_assign memo tr tt = + match tt with | Elem (x, sx) -> let gu = if H.list_mem x tr.tr_nondets then @@ -115,7 +116,7 @@ let rec find_assign memo tr = function memo := (Hstring.view x,nv) :: !memo; nv else - try H.list_assoc x tr.tr_assigns + try fst (H.list_assoc_triplet x tr.tr_assigns) with Not_found -> UTerm (Elem (x, sx)) in begin @@ -197,21 +198,22 @@ let postpone args p np = let sa2 = SAtom.filter (Atom.has_vars args) np in SAtom.equal sa2 sa1 -let uguard sigma args tr_args = function - | [] -> [SAtom.empty] - | [j, dnf] -> +let uguard sigma args tr_args tr_ureq = + match tr_ureq with + | [] -> [SAtom.empty] + | [j, dnf, _] -> let uargs = List.filter (fun a -> not (H.list_mem a tr_args)) args in List.fold_left (fun lureq z -> let m = List.map (SAtom.subst ((j, z)::sigma)) dnf in List.fold_left (fun acc sa -> - (List.map (fun zy-> SAtom.union zy sa) m) @ acc ) [] lureq + (List.map (fun zy-> SAtom.union zy sa) m) @ acc ) [] lureq ) [SAtom.empty] uargs - - | _ -> assert false + + | _ -> assert false let add_list n l = if List.exists (fun n' -> Node.subset n' n) l then l @@ -305,7 +307,7 @@ let make_cubes_new (ls, post) rargs s tr cnp = let pre { tr_info = tri; tr_tau = tau; tr_reset = reset } unsafe = (* let tau = tr.tr_tau in *) let pre_unsafe = - SAtom.union tri.tr_reqs + SAtom.union (fst tri.tr_reqs) (SAtom.fold (fun a -> SAtom.add (pre_atom tau a)) unsafe SAtom.empty) in let pre_u = Cube.create_normal pre_unsafe in diff --git a/ptree.ml b/ptree.ml index 744bc9f9..d31484b9 100644 --- a/ptree.ml +++ b/ptree.ml @@ -19,8 +19,6 @@ open Util open Ast open Format - - type term = | TVar of Variable.t | TTerm of Term.t @@ -145,7 +143,7 @@ let print_subst fmt = type pswts = (cformula * term) list -type pglob_update = PUTerm of term | PUCase of pswts +type pglob_update = PUTerm of term | PUCase of pswts type pupdate = { pup_loc : loc; @@ -154,22 +152,32 @@ type pupdate = { pup_swts : pswts; } +type parraye_update = { + paup : loc; + pup_array : Hstring.t; + pup_index: Num.num; + paup_swts :pswts; +} + + + type ptransition = { ptr_lets : (Hstring.t * term) list; ptr_name : Hstring.t; ptr_args : Variable.t list; - ptr_reqs : cformula; - ptr_assigns : (Hstring.t * pglob_update) list; + ptr_reqs : cformula * loc ; + ptr_assigns : (Hstring.t * pglob_update * loc) list; ptr_upds : pupdate list; ptr_nondets : Hstring.t list; ptr_loc : loc; } type psystem = { - pglobals : (loc * Hstring.t * Smt.Type.t) list; - pconsts : (loc * Hstring.t * Smt.Type.t) list; - parrays : (loc * Hstring.t * (Smt.Type.t list * Smt.Type.t)) list; - ptype_defs : (loc * Ast.type_constructors) list; + pglobals : (loc * Hstring.t * Hstring.t) list; + pconsts : (loc * Hstring.t * Hstring.t) list; + parrays : (loc * Hstring.t * (Hstring.t list * Hstring.t)) list; + (*ptype_defs : (loc * Ast.type_constructors) list;*) + ptype_defs : Ast.type_defs list; pinit : loc * Variable.t list * cformula; pinvs : (loc * Variable.t list * cformula) list; punsafe : (loc * Variable.t list * cformula) list; @@ -288,7 +296,7 @@ let rec apply_subst sigma (f:formula) = match f with let app_fun name args = try let vars, f = Hstring.H.find function_defs name in - (* eprintf "app fun %a (%a)@." Hstring.print name Variable.print_vars vars; *) + eprintf "app fun %a (%a)@." Hstring.print name Variable.print_vars vars; let nvars, nargs = List.length vars, List.length args in if nvars <> nargs then failwith (asprintf @@ -438,7 +446,7 @@ let rec up_quantifiers = function | PAnd l -> let l' = List.map up_quantifiers l in foralls_above_and ([],[]) l' - | POr l -> + | POr l -> let l' = List.map up_quantifiers l in exists_above_or ([],[]) l' | PEquiv _ | PImp _ | PIte _ | PNot _ -> assert false @@ -469,15 +477,17 @@ let satom_of_atom_list = | x -> eprintf "%a@." print x; assert false ) SAtom.empty -let satom_of_cube = function - | PAtom a -> SAtom.singleton (conv_atom a) - | PAnd l -> satom_of_atom_list l - | _ -> assert false - -let satoms_of_dnf = function - | PAtom _ | PAnd _ as c -> [satom_of_cube c] - | POr l -> List.map satom_of_cube l - | _ -> assert false +let satom_of_cube c = + match c with + | PAtom a -> SAtom.singleton (conv_atom a) + | PAnd l -> satom_of_atom_list l + | _ -> assert false + +let satoms_of_dnf dnf = + match dnf with + | PAtom _ | PAnd _ as c -> [satom_of_cube c] + | POr l -> List.map satom_of_cube l + | _ -> assert false let unsafes_of_formula f = match up_quantifiers (dnf f) with @@ -491,13 +501,13 @@ let inits_of_formula f = let rec forall_to_others tr_args f = match f with | PAtom _ -> f - | PNot f1 -> + | PNot f1 -> let f1' = forall_to_others tr_args f1 in if f1 == f1' then f else PNot f1' - | PAnd l -> + | PAnd l -> let l' = List.map (forall_to_others tr_args) l in if List.for_all2 (==) l l' then f else PAnd l' - | POr l -> + | POr l -> let l' = List.map (forall_to_others tr_args) l in if List.for_all2 (==) l l' then f else POr l' | PImp (a, b) -> @@ -519,8 +529,8 @@ let rec forall_to_others tr_args f = match f with | PForall _ | PExists _ | PForall_other _ | PExists_other _ -> f -let uguard_of_formula = function - | PForall_other ([v], f) -> v, satoms_of_dnf f +let uguard_of_formula loc = function + | PForall_other ([v], f) -> v, satoms_of_dnf f, loc | _ -> assert false let rec classify_guards (req, ureq) = function @@ -529,28 +539,30 @@ let rec classify_guards (req, ureq) = function | PAtom _ as f :: l -> classify_guards (f :: req, ureq) l | _ -> assert false -let rec guard_of_formula_aux = function - | PAtom _ as f -> [satom_of_cube f, []] - | PAnd l -> +let rec guard_of_formula_aux loc f = + match f with + | PAtom _ -> [satom_of_cube f, []] + | PAnd l -> let req, ureq = classify_guards ([],[]) l in - [satom_of_cube req, List.map uguard_of_formula ureq] - | POr l -> List.map guard_of_formula_aux l |> List.flatten - | f -> + [satom_of_cube req, List.map (uguard_of_formula loc) ureq] + | POr l -> List.map (guard_of_formula_aux loc) l |> List.flatten + | _ -> let req, ureq = classify_guards ([],[]) [f] in - [satom_of_cube req, List.map uguard_of_formula ureq] + [satom_of_cube req, List.map (uguard_of_formula loc) ureq] (* | _ -> assert false *) -let guard_of_formula tr_args f = +let guard_of_formula tr_args (f,loc) = match f |> forall_to_others tr_args |> dnf |> up_quantifiers with | PForall _ | PExists _ | PExists_other _ -> assert false - | f -> guard_of_formula_aux f + | f -> guard_of_formula_aux loc f (* Encodings of Ptree systems to AST systems *) -let encode_term = function - | TVar v -> Elem (v, Var) - | TTerm t -> t +let encode_term t = + match t with + | TVar v -> Elem (v, Var) + | TTerm e -> e let encode_pswts pswts = @@ -561,35 +573,43 @@ let encode_pswts pswts = ) [] pswts |> List.rev -let encode_pglob_update = function - | PUTerm t -> UTerm (encode_term t) - | PUCase pswts -> UCase (encode_pswts pswts) +let encode_pglob_update u = + match u with + | PUTerm t -> UTerm (encode_term t) + | PUCase pswts -> UCase (encode_pswts pswts) + -let encode_pupdate {pup_loc; pup_arr; pup_arg; pup_swts} = - { up_loc = pup_loc; - up_arr = pup_arr; - up_arg = pup_arg; - up_swts = encode_pswts pup_swts; +let encode_pupdate up = + { up_loc = up.pup_loc; + up_arr = up.pup_arr; + up_arg = up.pup_arg; + up_swts = encode_pswts up.pup_swts; } - -let encode_ptransition - {ptr_lets; ptr_name; ptr_args; ptr_reqs; ptr_assigns; - ptr_upds; ptr_nondets; ptr_loc;} = - let dguards = guard_of_formula ptr_args ptr_reqs in - let tr_assigns = List.map (fun (i, pgu) -> - (i, encode_pglob_update pgu)) ptr_assigns in - let tr_upds = List.map encode_pupdate ptr_upds in - let tr_lets = List.map (fun (x, t) -> (x, encode_term t)) ptr_lets in +(* +let encode_array_update up = + { + up_loc = up.pup_loc; + up_array = up.pup_array; + up_arg = up.pup_arg; + up_swts = encode_pswts up.pup_swts; + }*) + +let encode_ptransition tr = + let dguards = guard_of_formula tr.ptr_args tr.ptr_reqs in + let tr_assigns = + List.map (fun (i, pgu,loc) -> (i, encode_pglob_update pgu,loc)) tr.ptr_assigns in + let tr_upds = List.map encode_pupdate tr.ptr_upds in + let tr_lets = List.map (fun (x, t) -> (x, encode_term t)) tr.ptr_lets in List.rev_map (fun (req, ureq) -> - { tr_name = ptr_name; - tr_args = ptr_args; - tr_reqs = req; + { tr_name = tr.ptr_name; + tr_args = tr.ptr_args; + tr_reqs = (req, snd tr.ptr_reqs); tr_ureq = ureq; tr_lets = tr_lets; tr_assigns; tr_upds; - tr_nondets = ptr_nondets; - tr_loc = ptr_loc } + tr_nondets = tr.ptr_nondets; + tr_loc = tr.ptr_loc } ) dguards @@ -620,14 +640,14 @@ let encode_psystem List.fold_left (fun acc ptr -> List.fold_left (fun acc tr -> tr :: acc) acc (encode_ptransition ptr) ) [] ptrans - |> List.sort (fun t1 t2 -> + |> List.sort (fun t1 t2 -> let c = compare (List.length t1.tr_args) (List.length t2.tr_args) in if c <> 0 then c else let c = compare (List.length t1.tr_upds) (List.length t2.tr_upds) in if c <> 0 then c else let c = compare (List.length t1.tr_ureq) (List.length t2.tr_ureq) in if c <> 0 then c else - compare (SAtom.cardinal t1.tr_reqs) (SAtom.cardinal t2.tr_reqs) + compare (SAtom.cardinal (fst t1.tr_reqs)) (SAtom.cardinal (fst t2.tr_reqs)) ) in { @@ -643,7 +663,7 @@ let encode_psystem -let psystem_of_decls ~pglobals ~pconsts ~parrays ~ptype_defs pdecls = +let psystem_of_decls ~pglobals ~pconsts ~parrays ~ptype_defs pdecls = let inits, pinvs, punsafe, ptrans = List.fold_left (fun (inits, invs, unsafes, trans) -> function | PInit i -> i :: inits, invs, unsafes, trans @@ -678,7 +698,7 @@ let print_type_defs fmt = Hstring.print ty (Pretty.print_list (fun fmt -> fprintf fmt "@{%a@}" Hstring.print) - "@ | ") cstrs + "@ | ") cstrs (*TODO: new types*) ) let print_globals fmt = @@ -730,11 +750,11 @@ let print_invs fmt = let print_reqs fmt (tr_reqs, tr_ureq) = - if SAtom.for_all Atom.(equal True) tr_reqs && tr_ureq = [] then () + if SAtom.for_all Atom.(equal True) (fst tr_reqs) && tr_ureq = [] then () else fprintf fmt "@{requires@} @[{@ %a%a@ }@]@," - SAtom.print_inline tr_reqs - (fun fmt -> List.iter (fun (v, u) -> + SAtom.print_inline (fst tr_reqs) + (fun fmt -> List.iter (fun (v, u, _) -> fprintf fmt "@ &&@ @[(@{forall_other@} %a.@ %a)@]" Variable.print v print_dnf u )) tr_ureq @@ -757,7 +777,7 @@ let print_swts fmt swts = | _ -> assert false let print_assigns fmt tr_assigns = - List.iter (fun (g, gu) -> + List.iter (fun (g, gu, location) -> fprintf fmt "@[%a@ =@ " Hstring.print g; match gu with | UTerm t -> fprintf fmt "%a;@]@," Term.print t @@ -801,12 +821,16 @@ let print_trans fmt = let print_system fmt { type_defs; globals; - arrays; + arrays; consts; init; invs; unsafe; trans } = + let type_defs = + List.fold_left (fun (constrs) -> function + | Constructors i -> i::constrs + ) ([]) type_defs in print_type_defs fmt type_defs; pp_print_newline fmt (); print_globals fmt globals; diff --git a/ptree.mli b/ptree.mli index 049b998b..4cc0b4f5 100644 --- a/ptree.mli +++ b/ptree.mli @@ -69,8 +69,7 @@ type cformula = formula type pswts = (cformula * term) list -type pglob_update = PUTerm of term | PUCase of pswts - +type pglob_update = PUTerm of term | PUCase of pswts type pupdate = { pup_loc : loc; pup_arr : Hstring.t; @@ -78,22 +77,31 @@ type pupdate = { pup_swts : pswts; } + +type parraye_update = { + paup : loc; + pup_array : Hstring.t; + pup_index: Num.num; + paup_swts :pswts; +} + type ptransition = { ptr_lets : (Hstring.t * term) list; ptr_name : Hstring.t; ptr_args : Variable.t list; - ptr_reqs : cformula; - ptr_assigns : (Hstring.t * pglob_update) list; + ptr_reqs : cformula * loc; + ptr_assigns : (Hstring.t * pglob_update * loc) list; ptr_upds : pupdate list; ptr_nondets : Hstring.t list; ptr_loc : loc; } type psystem = { - pglobals : (loc * Hstring.t * Smt.Type.t) list; - pconsts : (loc * Hstring.t * Smt.Type.t) list; - parrays : (loc * Hstring.t * (Smt.Type.t list * Smt.Type.t)) list; - ptype_defs : (loc * Ast.type_constructors) list; + pglobals : (loc * Hstring.t * Hstring.t) list; + pconsts : (loc * Hstring.t * Hstring.t) list; + parrays : (loc * Hstring.t * (Hstring.t list * Hstring.t)) list; + (* ptype_defs : (loc * Ast.type_constructors) list;*) + ptype_defs : Ast.type_defs list; pinit : loc * Variable.t list * cformula; pinvs : (loc * Variable.t list * cformula) list; punsafe : (loc * Variable.t list * cformula) list; @@ -116,12 +124,16 @@ val app_fun : Hstring.t -> term_or_formula list -> formula val encode_psystem : psystem -> Ast.system val psystem_of_decls: - pglobals : (loc * Hstring.t * Smt.Type.t) list -> - pconsts : (loc * Hstring.t * Smt.Type.t) list -> - parrays : (loc * Hstring.t * (Smt.Type.t list * Smt.Type.t)) list -> - ptype_defs : (loc * Ast.type_constructors) list -> + pglobals : (loc * Hstring.t * Hstring.t) list -> + pconsts : (loc * Hstring.t * Hstring.t) list -> + parrays : (loc * Hstring.t * (Hstring.t list * Hstring.t)) list -> + +(*ptype_defs : (loc * Ast.type_constructors) list*) ptype_defs : Ast.type_defs list -> pdecl list -> psystem (** {2 Pretty printing ASTs} *) + +val print_swts : Format.formatter -> Ast.swts -> unit +val print_trans: Format.formatter -> Ast.transition_info list -> unit val print_system : Format.formatter -> Ast.system -> unit diff --git a/smt/alt_ergo.ml b/smt/alt_ergo.ml index 2bff6ed5..417472a6 100644 --- a/smt/alt_ergo.ml +++ b/smt/alt_ergo.ml @@ -76,6 +76,16 @@ module Type = struct H.add decl_symbs c (Symbols.name ~kind:Symbols.Constructor c, [], ty) + let declare_enum t constrs = + if H.mem decl_types t then raise (Error (DuplicateTypeName t)); + match constrs with + | [] -> + H.add decl_types t (Ty.Tabstract t) + | _ -> + let ty = Ty.Tsum (t, constrs) in + H.add decl_types t ty; + List.iter (fun c -> declare_constructor t c) constrs + let declare t constrs = if H.mem decl_types t then raise (Error (DuplicateTypeName t)); match constrs with diff --git a/smt/smt_sig.mli b/smt/smt_sig.mli index 3f727be3..4128efda 100644 --- a/smt/smt_sig.mli +++ b/smt/smt_sig.mli @@ -62,6 +62,8 @@ module type S = sig name [n] and constructors [cstrs].} {- [declare n []] declares a new abstract type with name [n].}}*) + val declare_enum : Hstring.t -> Hstring.t list -> unit + val all_constructors : unit -> Hstring.t list (** [all_constructors ()] returns a list of all the defined constructors. *) diff --git a/smt/z3wrapper_fake.ml b/smt/z3wrapper_fake.ml index f2f3c06b..e48cdcfa 100644 --- a/smt/z3wrapper_fake.ml +++ b/smt/z3wrapper_fake.ml @@ -39,6 +39,7 @@ module Type = struct let type_bool = hfake let type_proc = hfake let declare _ _ = unsupported () + let declare_enum _ _ = unsupported () let all_constructors _ = unsupported () let constructors _ = unsupported () let declared_types _ = unsupported () diff --git a/trace.ml b/trace.ml index 84013b41..30d1a148 100644 --- a/trace.ml +++ b/trace.ml @@ -254,9 +254,9 @@ module AltErgo = struct let rec add_assign_list globals fmt = function | [] -> globals - | [g,t] -> fprintf fmt "%a" print_assign (g,t); + | [g,t,_] -> fprintf fmt "%a" print_assign (g,t); HSet.remove g globals - | (g,t) :: r -> + | (g,t,_) :: r -> fprintf fmt "%a and\n" print_assign (g,t); add_assign_list (HSet.remove g globals) fmt r @@ -267,12 +267,12 @@ module AltErgo = struct print_assigns_unchanged r - let print_assigns globals fmt ass = + let print_assigns globals fmt ags = let globals = List.fold_left (fun acc g -> HSet.add g acc) HSet.empty globals in - let remaining = add_assign_list globals fmt ass in + let remaining = add_assign_list globals fmt ags in let remaining = HSet.elements remaining in - if ass <> [] && remaining <> [] then fprintf fmt " and\n"; + if ags <> [] && remaining <> [] then fprintf fmt " and\n"; print_assigns_unchanged fmt remaining let print_update fmt {up_arr=a; up_arg=args; up_swts=swts} = @@ -394,8 +394,8 @@ module AltErgo = struct print_args args print_distinct args end; fprintf fmt "( (* requires *)\n"; - print_satom ~prime:false fmt t.tr_reqs; - List.iter (fun (j, disj) -> + print_satom ~prime:false fmt (fst t.tr_reqs); + List.iter (fun (j, disj, _) -> fprintf fmt "\nand (forall %a:int." print_proc j; distinct_from_params_imp fmt j args; fprintf fmt "\n%a" (print_disj ~prime:false) disj; @@ -787,9 +787,9 @@ module Why3 = struct let rec add_assign_list globals fmt = function | [] -> globals - | [g,t] -> fprintf fmt "%a" print_assign (g,t); + | [g,t,_] -> fprintf fmt "%a" print_assign (g,t); HSet.remove g globals - | (g,t) :: r -> + | (g,t,_) :: r -> fprintf fmt "%a /\\@ " print_assign (g,t); add_assign_list (HSet.remove g globals) fmt r @@ -929,8 +929,8 @@ module Why3 = struct print_args args print_distinct args end; fprintf fmt "@[( (* requires *)@\n"; - print_satom ~prime:false fmt t.tr_reqs; - List.iter (fun (j, disj) -> + print_satom ~prime:false fmt (fst t.tr_reqs); + List.iter (fun (j, disj, _) -> fprintf fmt "\n/\\ (forall %a:int." print_proc j; distinct_from_params_imp fmt j args; fprintf fmt "\n%a" (print_disj ~prime:false) disj; @@ -1590,9 +1590,9 @@ module Why3_INST = struct let rec add_assign_list globals fmt = function | [] -> globals - | [g,t] -> fprintf fmt "%a" print_assign (g,t); + | [g,t,_] -> fprintf fmt "%a" print_assign (g,t); HSet.remove g globals - | (g,t) :: r -> + | (g,t,_) :: r -> fprintf fmt "%a /\\\n" print_assign (g,t); add_assign_list (HSet.remove g globals) fmt r @@ -1730,8 +1730,8 @@ module Why3_INST = struct print_args args print_distinct args end; fprintf fmt "( (* requires *)\n"; - print_satom ~prime:false fmt t.tr_reqs; - List.iter (fun (j, disj) -> + print_satom ~prime:false fmt (fst t.tr_reqs); + List.iter (fun (j, disj, _) -> fprintf fmt "\n/\\ (forall %a:int." print_proc j; distinct_from_params_imp fmt j args; fprintf fmt "\n%a" (print_disj ~prime:false) disj; diff --git a/typing.ml b/typing.ml index b4dc8ed7..3e24434a 100644 --- a/typing.ml +++ b/typing.ml @@ -18,7 +18,7 @@ open Util open Ast open Types open Atom -open Stdlib +(*open Pervasives*) type error = | UnknownConstr of Hstring.t @@ -40,6 +40,7 @@ type error = | NotATerm of Hstring.t | WrongNbArgs of Hstring.t * int | Smt of Smt.error + exception Error of error * loc @@ -47,6 +48,10 @@ let print_htype fmt (args, ty) = fprintf fmt "%a%a" (fun fmt -> List.iter (fprintf fmt "%a -> " Hstring.print)) args Hstring.print ty + +let print_missing_fields fmt fields = + fprintf fmt "%a" + (fun fmt -> List.iter (fprintf fmt " %a " Hstring.print)) fields let report fmt = function | UnknownConstr e -> @@ -89,11 +94,15 @@ let report fmt = function | Smt (Smt.DuplicateTypeName s) -> fprintf fmt "duplicate type name for %a" Hstring.print s | Smt (Smt.DuplicateSymb e) -> - fprintf fmt "duplicate name for %a" Hstring.print e + fprintf fmt "duplicate name for %a" Hstring.print e + | Smt (Smt.UnknownType s) -> - fprintf fmt "unknown type %a" Hstring.print s + fprintf fmt "unknown type %a" Hstring.print s + | Smt (Smt.UnknownSymb s) -> - fprintf fmt "unknown symbol %a" Hstring.print s + fprintf fmt "unknown symbol %a" Hstring.print s + + let error e l = raise (Error (e,l)) @@ -101,9 +110,12 @@ let rec unique error = function | [] -> () | x :: l -> if Hstring.list_mem x l then error x; unique error l + + let unify loc (args_1, ty_1) (args_2, ty_2) = if not (Hstring.equal ty_1 ty_2) || Hstring.compare_list args_1 args_2 <> 0 - then error (IncompatibleType (args_1, ty_1, args_2, ty_2)) loc + then error (IncompatibleType (args_1, ty_1, args_2, ty_2)) loc + let refinements = Hstring.H.create 17 @@ -111,7 +123,7 @@ let infer_type x1 x2 = try let h1 = match x1 with | Const _ | Arith _ -> raise Exit - | Elem (h1, _) | Access (h1, _) -> h1 + | Elem (h1, _) | Access (h1, _) -> h1 in let ref_ty, ref_cs = try Hstring.H.find refinements h1 with Not_found -> [], [] in @@ -123,32 +135,35 @@ let infer_type x1 x2 = let refinement_cycles () = (* TODO *) () -let rec term loc args = function - | Const cs -> + + +let rec term loc args t = + match t with + | Const cs -> let c, _ = MConst.choose cs in (match c with - | ConstInt _ -> [], Smt.Type.type_int - | ConstReal _ -> [], Smt.Type.type_real + | ConstInt _ -> t, ([], Smt.Type.type_int) + | ConstReal _ -> t, ([], Smt.Type.type_real) | ConstName x -> - try Smt.Symbol.type_of x - with Not_found -> error (UnknownName x) loc) - | Elem (e, Var) -> - if Hstring.list_mem e args then [], Smt.Type.type_proc + try t, Smt.Symbol.type_of x + with Not_found -> error (UnknownName x) loc) + | Elem (e, Var) -> + if Hstring.list_mem e args then t,([], Smt.Type.type_proc) else begin - try Smt.Symbol.type_of e with Not_found -> + try t, Smt.Symbol.type_of e with Not_found -> error (UnknownName e) loc end - | Elem (e, _) -> Smt.Symbol.type_of e + | Elem (e, _) -> t, Smt.Symbol.type_of e | Arith (x, _) -> begin - let args, tx = term loc args x in + let _, (args, tx) = term loc args x in if not (Hstring.equal tx Smt.Type.type_int) && not (Hstring.equal tx Smt.Type.type_real) then error (MustBeNum x) loc; - args, tx + t, (args, tx) end | Access(a, li) -> - let args_a, ty_a = + let args_a, ty_a = try Smt.Symbol.type_of a with Not_found -> error (UnknownArray a) loc in if List.length args_a <> List.length li then error (WrongNbArgs (a, List.length args_a)) loc @@ -167,44 +182,53 @@ let rec term loc args = function if not (Hstring.equal ty_i Smt.Type.type_proc) then error (MustBeOfTypeProc i) loc; ) li; - [], ty_a + t,([], ty_a) -let assignment ?(init_variant=false) g x (_, ty) = + + +let rec assignment ?(init_variant=false) g x (_, ty) = + (*Format.eprintf "GG: %a; x : %a; ty: %a@." Hstring.print g Types.Term.print x Hstring.print ty;*) if ty = Smt.Type.type_proc || ty = Smt.Type.type_bool - || ty = Smt.Type.type_int + || ty = Smt.Type.type_int then () else match x with | Elem (n, Constr) -> Smt.Variant.assign_constr g n - | Elem (n, _) | Access (n, _) -> + | Elem (n, _) | Access (n, _) -> Smt.Variant.assign_var g n; if init_variant then Smt.Variant.assign_var n g | _ -> () -let atom loc init_variant args = function - | True | False -> () - | Comp (Elem(g, Glob) as x, Eq, y) - | Comp (y, Eq, (Elem(g, Glob) as x)) - | Comp (y, Eq, (Access(g, _) as x)) - | Comp (Access(g, _) as x, Eq, y) -> - let ty = term loc args y in - unify loc (term loc args x) ty; - if init_variant then assignment ~init_variant g y ty - | Comp (x, op, y) -> - unify loc (term loc args x) (term loc args y) - | Ite _ -> assert false +let atom loc init_variant args a = + match a with + | True | False -> a + | Comp (Elem(g, Glob) as x, Eq, y) + | Comp (y, Eq, (Elem(g, Glob) as x)) + | Comp (y, Eq, (Access(g, _) as x)) + | Comp (Access(g, _) as x, Eq, y) -> + let x', tx = term loc args x in + let y',ty = term loc args y in + unify loc tx ty; + if init_variant then assignment ~init_variant g y' ty; + Comp(x', Eq, y') + | Comp (x, op, y) -> + let x', tx = term loc args x in + let y',ty = term loc args y in + unify loc tx ty; + Comp (x', op, y') + | Ite _ -> assert false let atoms loc ?(init_variant=false) args = - SAtom.iter (atom loc init_variant args) - -let init (loc, args, lsa) = List.iter (atoms loc ~init_variant:true args) lsa + SAtom.map (atom loc init_variant args) +let init (loc, args, lsa) = loc,args, List.map (atoms loc ~init_variant:true args) lsa + let unsafe (loc, args, sa) = unique (fun x-> error (DuplicateName x) loc) args; - atoms loc args sa + (loc, args, atoms loc args sa) let nondets loc l = unique (fun c -> error (DuplicateAssign c) loc) l; @@ -219,82 +243,106 @@ let nondets loc l = (* error (MustBeOfTypeProc g) *) with Not_found -> error (UnknownGlobal g) loc) l -let assigns loc args = + +let assigns args la = let dv = ref [] in - List.iter - (fun (g, gu) -> + List.map + (fun (g, gu, loc) -> if Hstring.list_mem g !dv then error (DuplicateAssign g) loc; let ty_g = try Smt.Symbol.type_of g with Not_found -> error (UnknownGlobal g) loc in - begin + let gu = match gu with - | UTerm x -> - let ty_x = term loc args x in - unify loc ty_x ty_g; - assignment g x ty_x; - | UCase swts -> - List.iter (fun (sa, x) -> - atoms loc args sa; - let ty_x = term loc args x in - unify loc ty_x ty_g; - assignment g x ty_x; - ) swts - end; - dv := g ::!dv) - + | UTerm x-> + let tx, ty_x = term loc args x in + unify loc ty_x ty_g; + assignment g tx ty_x; + UTerm tx + | UCase swts -> + let swts = + List.map (fun (sa, t) -> + let sa = atoms loc args sa in + let tx, ty_x = term loc args t in + unify loc ty_x ty_g; + assignment g tx ty_x; + sa, tx + ) swts + in UCase swts + in + dv := g ::!dv; + g,gu,loc) la + let switchs loc a args ty_e l = - List.iter + List.map (fun (sa, t) -> - atoms loc args sa; - let ty = term loc args t in - unify loc ty ty_e; - assignment a t ty) l + let sa = atoms loc args sa in + let tt,ty = term loc args t in + unify loc ty ty_e; + + assignment a tt ty; + sa, tt) l -let updates args = + +let updates args upds = let dv = ref [] in - List.iter - (fun {up_loc=loc; up_arr=a; up_arg=lj; up_swts=swts} -> + List.map + (fun ({up_loc=loc; up_arr=a; up_arg=lj; up_swts=swts} as upd) -> if Hstring.list_mem a !dv then error (DuplicateUpdate a) loc; List.iter (fun j -> - if Hstring.list_mem j args then error (ClashParam j) loc) lj; + if Hstring.list_mem j args then error (ClashParam j)loc) lj; let args_a, ty_a = try Smt.Symbol.type_of a with Not_found -> error (UnknownArray a) loc in if args_a = [] then error (MustBeAnArray a) loc; dv := a ::!dv; - switchs loc a (lj @ args) ([], ty_a) swts) + let up_swts = switchs loc a (lj @ args) ([], ty_a) swts in + {upd with up_swts} + ) upds + let check_lets loc args l = - List.iter - (fun (x, t) -> - let _ = term loc args t in () - ) l + List.map + (fun (x, t) -> let tt,_ = term loc args t in x, tt) l -let transitions = - List.iter - (fun ({tr_args = args; tr_loc = loc} as t) -> - unique (fun x-> error (DuplicateName x) loc) args; - atoms loc args t.tr_reqs; - List.iter - (fun (x, cnf) -> - List.iter (atoms loc (x::args)) cnf) t.tr_ureq; - check_lets loc args t.tr_lets; - updates args t.tr_upds; - assigns loc args t.tr_assigns; - nondets loc t.tr_nondets) +let transitions tl = + List.map + (fun tr -> + unique (fun x -> error (DuplicateName x) tr.tr_loc) tr.tr_args; + let reqs, loc_reqs = tr.tr_reqs in + let tr_reqs = atoms loc_reqs tr.tr_args reqs, loc_reqs in + let tr_ureq = + List.map + (fun (ur, dnf, loc_req) -> + let dnf = + List.map (atoms tr.tr_loc (ur::tr.tr_args)) dnf in + ur, dnf, loc_req) tr.tr_ureq in + let tr_lets = check_lets tr.tr_loc tr.tr_args tr.tr_lets in + let tr_upds = updates tr.tr_args tr.tr_upds in + let tr_assigns = assigns tr.tr_args tr.tr_assigns in + nondets tr.tr_loc tr.tr_nondets; + { tr with tr_reqs; tr_ureq; tr_lets; tr_upds; tr_assigns } + + ) tl + let declare_type (loc, (x, y)) = - try Smt.Type.declare x y + try Smt.Type.declare_enum x y with Smt.Error e -> error (Smt e) loc +let declare_t = function + | Constructors (loc, (x,y)) -> declare_type (loc,(x,y)) + let declare_symbol loc n args ret = try Smt.Symbol.declare n args ret with Smt.Error e -> error (Smt e) loc +let declare_array loc n args ret = + declare_symbol loc n args ret + let init_global_env s = - List.iter declare_type s.type_defs; + List.iter declare_t s.type_defs; (* patch completeness on Boolean *) (*let mybool = Hstring.make "mbool" in let mytrue = Hstring.make "@MTrue" in @@ -313,7 +361,8 @@ let init_global_env s = List.iter (fun (loc, n, (args, ret)) -> declare_symbol loc n args ret; - l := (n, ret)::!l) s.arrays; + l := (n, ret)::!l) s.arrays; + !l @@ -386,7 +435,7 @@ let create_init_instances (iargs, l_init) invs = let init_instances = Hashtbl.create 11 in begin match l_init with - | [init] -> + | [init] -> let sa, cst = SAtom.partition (fun a -> List.exists (fun z -> has_var z a) iargs) init in let ar0 = ArrayAtom.of_satom cst in @@ -403,7 +452,7 @@ let create_init_instances (iargs, l_init) invs = incr cpt; v_acc) [] Variable.procs) - | _ -> + | _ -> let dnf_sa0, dnf_ar0 = List.fold_left (fun (dnf_sa0, dnf_ar0) sa -> let sa0 = SAtom.filter (fun a -> @@ -466,6 +515,7 @@ let debug_init_instances insts = let create_node_rename kind vars sa = let sigma = Variable.build_subst vars Variable.procs in let c = Cube.subst sigma (Cube.create vars sa) in + (*let c = Cube.create c.vars (Prover.normalize c.litterals) in*) let c = Cube.normal_form c in Node.create ~kind c @@ -476,30 +526,30 @@ let fresh_args ({ tr_args = args; tr_upds = upds} as tr) = let sigma = Variable.build_subst args Variable.freshs in { tr with tr_args = List.map (Variable.subst sigma) tr.tr_args; - tr_reqs = SAtom.subst sigma tr.tr_reqs; + tr_reqs = (SAtom.subst sigma (fst tr.tr_reqs), snd tr.tr_reqs) ; tr_ureq = List.map - (fun (s, dnf) -> s, List.map (SAtom.subst sigma) dnf) tr.tr_ureq; + (fun (s, dnf, loc) -> s, List.map (SAtom.subst sigma) dnf, loc) tr.tr_ureq; tr_assigns = List.map (function - | x, UTerm t -> x, UTerm (Term.subst sigma t) - | x, UCase swts -> - let swts = - List.map - (fun (sa, t) -> - SAtom.subst sigma sa, Term.subst sigma t) swts in - x, UCase swts - ) tr.tr_assigns; + | x, UTerm t, loc -> x, UTerm (Term.subst sigma t),loc + | x, UCase swts, loc -> + let swts = + List.map + (fun (sa, t) -> + SAtom.subst sigma sa, Term.subst sigma t) swts in + x, UCase swts, loc + ) tr.tr_assigns; tr_upds = List.map (fun ({up_swts = swts} as up) -> - let swts = + let swts = List.map (fun (sa, t) -> SAtom.subst sigma sa, Term.subst sigma t) swts - in + in { up with up_swts = swts }) upds} - + let add_tau tr = (* (\* let tr = fresh_args tr in *\) *) @@ -510,27 +560,30 @@ let add_tau tr = tr_tau = pre; tr_reset = reset_memo; } + let system s = let l = init_global_env s in - if not Options.notyping then init s.init; - if Options.subtyping then Smt.Variant.init l; - if not Options.notyping then List.iter unsafe s.unsafe; - if not Options.notyping then List.iter unsafe (List.rev s.invs); - if not Options.notyping then transitions s.trans; + let s_init = if not Options.notyping then init s.init else s.init in + (*List.iter (fun (f,t) -> Format.eprintf "system: f: %a; t: %a @." Hstring.print f Hstring.print t) l;*) + if Options.subtyping then Smt.Variant.init l; + let s_unsafe = if not Options.notyping then List.map unsafe s.unsafe else s.unsafe in + let s_invs = if not Options.notyping then List.map unsafe (List.rev s.invs) else s.invs in + let s_trans = if not Options.notyping then transitions s.trans else s.trans in if Options.(subtyping && not murphi) then begin Smt.Variant.close (); if Options.debug then Smt.Variant.print (); end; - let init_woloc = let _,v,i = s.init in v,i in + let init_woloc = let _,v,i = s_init in v,i in let invs_woloc = - List.map (fun (_,v,i) -> create_node_rename Inv v i) s.invs in + List.map (fun (_,v,i) -> create_node_rename Inv v i) s_invs in let unsafe_woloc = - List.map (fun (_,v,u) -> create_node_rename Orig v u) s.unsafe in + List.map (fun (_,v,u) -> create_node_rename Orig v u) s_unsafe in let init_instances = create_init_instances init_woloc invs_woloc in - if Options.debug && Options.verbose > 0 then - debug_init_instances init_instances; + if Options.debug && Options.verbose > 0 then + debug_init_instances init_instances; + { t_globals = List.map (fun (_,g,_) -> g) s.globals; t_consts = List.map (fun (_,c,_) -> c) s.consts; @@ -539,5 +592,5 @@ let system s = t_init_instances = init_instances; t_invs = invs_woloc; t_unsafe = unsafe_woloc; - t_trans = List.map add_tau s.trans; + t_trans = List.map add_tau s_trans; }