(* Typestate Plugin *) open Iabsyn open Types type typestate_impl_module = Sabsyn.form Iabsyn.impl_module type typestate_access_pattern = Id.format_t * Id.field_t let loop_widening_count = 3 let check_antecedents = ref false let ignore_invariants = ref false let decide_implications_quickly = ref true let typestate_convert_impl_module (ms:Sabsyn.spec_module) (ast:string Iabsyn.impl_module) (pn:string list) : typestate_impl_module = let w = { Spec.s = Spec.collect_all_sets ms; Spec.b = Spec.collect_all_bools ms } in let typestate_convert_stmt pi s = let rec tcs s = match s with | EmptyStmt -> EmptyStmt | HavocStmt n -> HavocStmt n | ChoiceStmt (t, u) -> ChoiceStmt (tcs t, tcs u) | CompoundStmt cs -> CompoundStmt (List.map tcs cs) | LocalDeclStmt (v, t, e) -> LocalDeclStmt (v, t, e) | ExprStmt e -> ExprStmt e | ReturnStmt r -> ReturnStmt r | WhileStmt (i, e, b) -> let i' = match i with Some x -> Some (Specchecker.parse_checked_formula ms w pi x) | None -> None in WhileStmt (i', e, tcs b) | AssertStmt (n, a) -> AssertStmt (n, Specchecker.parse_checked_formula ms w pi a) | AssumeStmt (n, a) -> AssumeStmt (n, Specchecker.parse_checked_formula ms w pi a) | PragmaStmt s -> PragmaStmt s | IfStmt (e, t, f) -> IfStmt (e, tcs t, tcs f) in tcs s in let typestate_convert_proc p = { proc_id = p.proc_id; proc_modifiers = p.proc_modifiers; formals = p.formals; ret_val = p.ret_val; requires = (match p.requires with None -> None | Some x -> Some (Specchecker.parse_checked_formula ms w p x)); modifies = p.modifies; ensures = (match p.ensures with None -> None | Some x -> Some (Specchecker.parse_checked_formula ms w p x)); proc_body = typestate_convert_stmt p p.proc_body } in { module_name = ast.module_name; instantiated_from = ast.instantiated_from; param_subst = ast.param_subst; formats = ast.formats; references = ast.references; procs = List.map typestate_convert_proc (List.filter (fun p -> List.mem (Id.name_of_proc p.proc_id) pn) ast.procs); } let id_regexp = "[a-zA-Z$_][a-zA-Z0-9$_]*" let set_exp = Str.regexp ("\\("^id_regexp ^ "\\)\\.\\(" ^ id_regexp ^ "\\)[ \t]*=" ^ "[ \t]*\\([0-9\\|true\\|false]+\\)") type typestate_pred = { o : string; f : string; v : int32 } let parse_typestate_pred s = if not (Str.string_match set_exp s 0) or (Str.matched_string s <> s) then failwith ("Typestate predicate "^s^" does not parse."); let v0 = Str.matched_group 3 s in { o = Str.matched_group 1 s; f = Str.matched_group 2 s; v = if v0 = "true" then 1l else if v0 = "false" then 0l (*else if v0 = "false" or v0 = "0" then failwith ("Bad initial value (0, false) for typestate predicate.")*) else Int32.of_string (Str.matched_group 3 s) } let compute_access_pattern modn (ma:string Aabsyn.abst_body) = List.concat (List.map (function d -> (match (snd d) with | Aabsyn.BaseForm sd -> (match sd.Aabsyn.expr with Aabsyn.FormulaClause se -> [(sd.Aabsyn.xt, Id.fetch_field modn (parse_typestate_pred se).f)] | _ -> failwith "typestate plugin only handles direct forms") | Aabsyn.IntersectionForm _ -> [] (* assume that the base forms tell you all... *) | _ -> failwith "shoulda desugared the formula")) ma.Aabsyn.set_defns) let proc_hits (p:string Iabsyn.proc_def) (ap:typestate_access_pattern list) = let rec lhs_hits lvalue = (match lvalue with | LocalLvalue v -> false | RefLvalue rv -> false | FieldLvalue (e', f) -> List.mem f (List.map snd ap) | ArrayLvalue (e', i) -> expr_hits e' || expr_hits i) and expr_hits e = match e with | LiteralExpr _ -> false | VarExpr lvalue -> (match lvalue with | LocalLvalue v -> false | RefLvalue rv -> false | FieldLvalue (e', f) -> expr_hits e' | ArrayLvalue (e', i) -> expr_hits e' || expr_hits i) | FieldAccessExpr (e', f) -> expr_hits e' | ArrayLengthExpr e' -> expr_hits e' | ArrayAccessExpr (e', i) -> expr_hits e' || expr_hits i | NewExpr n -> false | NewArrayExpr (t, e', d) -> List.exists expr_hits e' | InvokeExpr (p, args) -> List.exists expr_hits args | AssignExpr (lhs, e') -> lhs_hits lhs || expr_hits e' | PreIncExpr e' | PostIncExpr e' | PreDecExpr e' | PostDecExpr e' -> lhs_hits e' | NegExpr e' | NotExpr e' -> expr_hits e' | PlusExpr (l, r) | MinusExpr (l, r) | MultExpr (l, r) | DivExpr (l, r) | ModExpr (l, r) | AndExpr (l, r) | OrExpr (l, r) | EqExpr (l, r) | NeqExpr (l, r) | LtExpr (l, r) | GtExpr (l, r) | LteqExpr (l, r) | GteqExpr (l, r) | BitAndExpr (l, r) | BitOrExpr (l, r) | BitXorExpr (l, r) | ShiftLeftExpr (l, r) | SignedShiftRightExpr (l, r) | UnsignedShiftRightExpr (l, r) -> expr_hits l || expr_hits r in let rec stmt_hits s = match s with | EmptyStmt -> false | HavocStmt n -> false | ChoiceStmt (t, u) -> stmt_hits t || stmt_hits s | CompoundStmt cs -> List.exists stmt_hits cs | LocalDeclStmt (v, t, e) -> expr_hits e | ExprStmt e -> expr_hits e | ReturnStmt None -> false | ReturnStmt (Some e) -> expr_hits e | WhileStmt (i, e, b) -> expr_hits e || stmt_hits b | AssertStmt (n, a) -> false | AssumeStmt (n, a) -> false | PragmaStmt s -> false | IfStmt (e, t, f) -> expr_hits e || stmt_hits t || stmt_hits f in stmt_hits p.proc_body let neutral_procs ((ma, ms, mi):string Aabsyn.abst_body * Sabsyn.spec_module * string Iabsyn.impl_module) = let ap = compute_access_pattern ms.Sabsyn.module_name ma in List.concat (List.map (fun p -> if (proc_hits p ap) then [] else [p.proc_id]) mi.procs) (* helpers *) let strip s = let s' = if String.contains s '^' then Str.string_before s (String.index s '^') else s in if String.contains s' '\'' then Str.string_before s' (String.index s '\'') else s' let primed x = x ^ "'" let hatted i x = x ^ "^" ^ string_of_int i let make_v_empty v = BA.Atom (BA.Eq (v, BA.Emptyset)) let exclude_v_from_s v s = BA.Atom (BA.Eq ((BA.Var (primed s)), BA.Diff ((BA.Var s), v))) let add_v_to_s v s = BA.Atom (BA.Eq ((BA.Var (primed s)), BA.Union [(BA.Var s); (BA.Var v)])) let frame_one x = BA.Atom (BA.Eq ((BA.Var (primed x)), (BA.Var x))) let frame_one_bool x = BA.mk_iff (BA.Atom (BA.Propvar (primed x)), BA.Atom (BA.Propvar x)) let all_sets_but all_sets x = List.filter (fun y -> not (y = x)) all_sets let frame_except all_sb not_stable = let unstable y = not (List.mem y not_stable) in BA.mk_and (List.map frame_one (List.filter unstable all_sb.Spec.s) @ List.map frame_one_bool (List.filter unstable all_sb.Spec.b)) let to_relation all_sb (f:BA.form) : BA.form = (* conjoin with S'=S for all sets S *) BA.mk_and [f; frame_except all_sb []] let universal_close_bool_vars (bool_vars:BA.ident list) f = let bool_vars' = List.map (fun x -> primed x) bool_vars in BA.mk_forallProp (bool_vars @ bool_vars',f) let existential_close_bool_vars (bool_vars:BA.ident list) f = let bool_vars' = List.map (fun x -> primed x) bool_vars in BA.mk_existsProp (bool_vars @ bool_vars',f) (* gives both primed and unprimed versions *) let compute_BA_set_names fetch_type (all_sets:BA.ident list) = let mkbv s = (s, fetch_type s) in let vts = List.map mkbv all_sets in let mkbv' s = (primed s, fetch_type s) in let vts' = List.map mkbv' all_sets in vts @ vts' let decide_implication msg fetch_type all_sb extra_conjs f g = let free_vars = compute_BA_set_names fetch_type all_sb.Spec.s in let antecedent = BA.mk_and [f; extra_conjs] in (* if the antecedent is false, then something's bad! *) if !check_antecedents then begin let antecedent' = BA.mk_existsSet (free_vars, existential_close_bool_vars all_sb.Spec.b antecedent) in if (not (BA.MONA.valid ("antecedent of "^msg) antecedent')) then begin BA.MONA.log "*** warning: antecedent always false! ***\n"; Util.amsg "*** warning: antecedent always false! ***\n" end end; let f' = if (!decide_implications_quickly & !BA.optimize_formulas) then BA.mk_not (BA.mk_existsSet (free_vars, existential_close_bool_vars all_sb.Spec.b (BA.mk_and [antecedent; BA.mk_not g]))) else BA.mk_forallSet (free_vars, universal_close_bool_vars all_sb.Spec.b (BA.mk_impl (antecedent, g))) in if (BA.MONA.valid msg f') then true else begin Util.msg (BA.MONA.getCounterexample (List.map fst free_vars) f'); false end (* incorporation is the result of quantifier elimination on: \exists \hat{S_1}, ..., \hat{S_n}. B[S_i' -> \hat{S_i}] /\ B_s[S_i -> \hat{S_i}] *) let rec extract_vars f = match f with | BA.ExistsSet (vts,f') -> vts @ extract_vars f' | _ -> [] let rec extract_body f = match f with | BA.ExistsSet (_,BA.And cs) -> BA.flatten cs [] | BA.ExistsSet (_,f') -> extract_body f' | BA.And cs -> BA.flatten cs [] | _ -> [f] let incorp msg (ic:int ref) fetch_type all_sb (b2:BA.form) (b1:BA.form) = ic := !ic + 1; let b1_subst = List.map (fun s -> (primed s, BA.Var (hatted !ic s))) all_sb.Spec.s in let b1_bool_subst = List.map (fun s -> (primed s, BA.Propvar (hatted !ic s))) all_sb.Spec.b in let b1' = BA.subst_propvar b1_bool_subst (BA.subst b1_subst b1) in let b2_subst = List.map (fun s -> (s, BA.Var (hatted !ic s))) all_sb.Spec.s in let b2_bool_subst = List.map (fun s -> (s, BA.Propvar (hatted !ic s))) all_sb.Spec.b in let b2' = BA.subst_propvar b2_bool_subst (BA.subst b2_subst b2) in let boundVars = List.map (fun x -> (hatted !ic x, fetch_type x)) all_sb.Spec.s in let vars1 = extract_vars b1' in let body1 = extract_body b1' in let vars2 = extract_vars b2' in let body2 = extract_body b2' in let res1 = BA.mk_existsProp (List.map (fun s -> hatted !ic s) all_sb.Spec.b, BA.mk_existsSet (boundVars @ vars1 @ vars2, BA.mk_and (body1 @ body2))) in let res = BA.simplify res1 in begin (* BA.MONA.log ("INCORPORATION:" ^ msg ^ "\n"); BA.MONA.log " INCORP FIRST: "; BA.MONA.log (BA.MONA.form_to_mona b1); BA.MONA.log "\n\n"; BA.MONA.log " INCORP SECOND: "; BA.MONA.log (BA.MONA.form_to_mona b2); BA.MONA.log "\n\n"; BA.MONA.log " INCORP RES: "; BA.MONA.log (BA.MONA.form_to_mona res); BA.MONA.log "\n\n"; *) res end exception Impl_failed let rec convert_set_defn_form f munge = match f with | Aabsyn.BaseForm b -> failwith "shoulda transformed the formula" | Aabsyn.IdForm id -> BA.Var (munge id) | Aabsyn.UnionForm (a, b) -> BA.Union [convert_set_defn_form a munge; convert_set_defn_form b munge] | Aabsyn.IntersectionForm (a, b) -> BA.Inter [convert_set_defn_form a munge; convert_set_defn_form b munge] | Aabsyn.DiffForm (a, b) -> BA.Diff (convert_set_defn_form a munge, convert_set_defn_form b munge) (* also uses all loaded spec modules in Ast.spec *) let analyze_module (modn:string) ((ma, ms0, mi0):string Aabsyn.abst_body * Sabsyn.spec_module * string Iabsyn.impl_module) (pn:string list) (rsM:Iabsyn.expr list) (augment_with_invariants:Id.proc_t -> Sabsyn.form -> bool -> Sabsyn.form) : bool = let impl_failed_reasons = ref [] in let translated_specs = let s' = List.filter (fun x -> not (x.Sabsyn.module_name = ms0.Sabsyn.module_name)) !Ast.spec in let s = ms0 :: s' in List.map Vctrans.interpret_uninterpreted_strings s in let fetch_translated_spec (name : string) : Sabsyn.spec_module = try (List.find (fun x -> x.Sabsyn.module_name = name) translated_specs) with Not_found -> failwith ("Couldn't find spec module "^name) in let ms = fetch_translated_spec ms0.Sabsyn.module_name in let mi = typestate_convert_impl_module ms mi0 pn in let alts_raw = Hashtbl.create 1 in let (triggers:((string * Id.format_t * int32),BA.ident) Hashtbl.t) = Hashtbl.create 1 in let derived_set_idents = ref [] in let derived_set_defns = ref [] in List.iter (function d -> match (snd d) with (* assume post-transform: base or cpd *) (Aabsyn.BaseForm sd) -> (match sd.Aabsyn.expr with (Aabsyn.FormulaClause se) -> let sdp = (parse_typestate_pred se) in let a = (try Hashtbl.find alts_raw (sdp.f, sd.Aabsyn.xt) with Not_found -> let l = ref [] in Hashtbl.add alts_raw (sdp.f, sd.Aabsyn.xt) l; l) in a := (fst d, sdp.v) :: !a; Hashtbl.add triggers (sdp.f, sd.Aabsyn.xt, sdp.v) (fst d); | _ -> failwith "typestate plugin only handles direct forms") | _ -> let cd = snd d in let lhs = BA.Var (fst d) in let lhs' = BA.Var (primed (fst d)) in let rhs = convert_set_defn_form cd (fun x -> x) in let rhs' = convert_set_defn_form cd primed in derived_set_idents := (fst d) :: !derived_set_idents; derived_set_defns := BA.Atom (BA.Eq (lhs, rhs)):: BA.Atom (BA.Eq (lhs', rhs')) :: !derived_set_defns) ma.Aabsyn.set_defns; (* frame with derived set defns *) let frame_except_d all_sb non_stable = frame_except all_sb (non_stable @ !derived_set_idents) in let alts : (BA.ident, BA.ident list) Hashtbl.t = Hashtbl.create 1 in List.iter (function (_, Aabsyn.BaseForm sd) -> (match sd.Aabsyn.expr with Aabsyn.FormulaClause se -> let sdp = (parse_typestate_pred se) in let av = Hashtbl.find alts_raw (sdp.f, sd.Aabsyn.xt) in List.iter (fun (x, _) -> Hashtbl.add alts x (List.map fst (List.filter (fun (y, _) -> y <> x) !av))) !av | _ -> failwith "typestate plugin only handles direct forms") | _ -> ()) ma.Aabsyn.set_defns; let disjtness_conds = let varify x = (BA.Var x) in let varify' x = (BA.Var (primed x)) in let a = ref [] in Hashtbl.iter (fun (f, _) vsp -> if (List.length !vsp) > 1 then if ((Util.find_dups (List.map snd !vsp)) = []) then (* all disj; in this case, can generate disjoint (A,B,C,D,E) *) let a_alts = List.map fst !vsp in a := BA.Atom (BA.Disjoint (List.map varify a_alts)) :: BA.Atom (BA.Disjoint (List.map varify' a_alts)) :: !a else begin (* S: x.f=1, D: x.f=1, E: x.f=2 *) (* in this case, disjoint (S,E) & disjoint (D,E) *) List.iter (fun ((s:BA.ident), v) -> let s_alts = List.map fst (List.filter (fun (s', v') -> v' <> v) !vsp) in if (List.length s_alts) > 1 then a := BA.Atom (BA.Disjoint (varify s::(List.map varify s_alts))) :: BA.Atom (BA.Disjoint (varify' s::(List.map varify' s_alts))) :: !a) !vsp end) alts_raw; !a in (* used to record what we've ensured at return statements *) let extra_results = ref [] in let analyze_proc (p:string) : bool = let ps = Ast.fetch_spec_proc p ms in let pi = Ast.fetch_impl_proc p mi in (* global means in-scope *) let global_sets = let global_sets_abst = Abst.collect_all_sets ma in let global_sets_spec = Spec.collect_all_sets ms in Util.remove_dups (List.merge compare (List.sort compare global_sets_abst) (List.sort compare global_sets_spec)) in let global_bools = let global_bools_abst = Abst.collect_all_bools ma in let global_bools_spec = Spec.collect_all_bools ms in Util.remove_dups (List.merge compare (List.sort compare global_bools_abst) (List.sort compare global_bools_spec)) in (* local means in proc *) let (local_sets, local_bools, tenv) = collect_local_obj_type_map pi in let all_sb = { Spec.s = global_sets @ local_sets; Spec.b = global_bools @ local_bools; } in let fetch_type (s:Id.var_t) = let s' = strip s in try Hashtbl.find tenv s' with Not_found -> try TObj (Abst.fetch_local_set_type s' ma) with Not_found -> (Spec.fetch_set_type s' ms) in let enforce_impl msg f g : unit = let res = decide_implication msg fetch_type all_sb (BA.mk_and (disjtness_conds @ !derived_set_defns)) f g in if not res then begin impl_failed_reasons := msg :: !impl_failed_reasons; raise Impl_failed end in let diagnose_fault_in_implication sp ps : unit = if not (decide_implication "trying impl without extra_ensures" fetch_type all_sb (BA.mk_and (disjtness_conds @ !derived_set_defns)) sp (BA.ba_of_sabsyn ps.Sabsyn.ensures)) then Util.amsg "Base formula wrong.\n" else List.iter (fun (c, r) -> if not (decide_implication ("trying impl extra_ensures" ^ r) fetch_type all_sb (BA.mk_and (disjtness_conds @ !derived_set_defns)) sp (BA.ba_of_sabsyn c)) then begin Util.amsg ("Extra ensures clause '"^r^"' broken.\n"); if r = Sabsyn.reason_frame then (* ok, track down which things are modified *) let bc = BA.ba_of_sabsyn c in let cs = match bc with | BA.And cls -> cls | _ -> [bc] in let (modifies_sets, modifies_props) = List.partition (fun x -> match x with | BA.Iff (BA.Atom (BA.Propvar p), BA.Atom (BA.Propvar p')) -> false | BA.Atom (BA.Eq (BA.Var s, BA.Var s')) -> true | _ -> failwith "not equiv in modified") cs in let decide_with_modifies m = decide_implication "trying impl without modifies" fetch_type all_sb (BA.mk_and (disjtness_conds @ !derived_set_defns)) sp m in List.iter (fun x -> if not (decide_with_modifies x) then Util.amsg ("Found modified set, or set needs havoc: " ^ BA.MONA.form_to_mona x ^ "\n")) modifies_sets; List.iter (fun x -> if not (decide_with_modifies x) then Util.amsg ("Found modified prop, or prop needs havoc: " ^ BA.MONA.form_to_mona x ^ "\n")) modifies_props end) ps.Sabsyn.extra_ensures in let ic = ref 0 in (* transfer function helpers *) let inc msg = incorp msg ic fetch_type all_sb in let set_v_to_null (v:Id.var_t) = let fram = frame_except_d all_sb [v] in BA.mk_and [make_v_empty (BA.Var (primed v)); fram] in let y_gets_x (y:Id.var_t) (x:Id.var_t) = let fram = frame_except_d all_sb [y] in BA.mk_and [BA.Atom (BA.Eq (BA.Var (primed y), BA.Var x)); fram] in let y_iff_x (y:Id.var_t) (x:Id.var_t) = let fram = frame_except_d all_sb [y] in BA.mk_and [BA.Iff (BA.Atom (BA.Propvar (primed y)), (BA.Atom (BA.Propvar x))); fram] in let b'_gets_not_b b' b = let fram = frame_except_d all_sb [b'] in BA.mk_and [BA.Iff (BA.Atom (BA.Propvar (primed b')), BA.Not (BA.Atom (BA.Propvar b))); fram] in let assign_new_to_v (v:Id.var_t) = let fram = frame_except_d all_sb [v] in let v_disj_all = BA.mk_and (List.map (fun x -> BA.Atom (BA.Disjoint [(BA.Var (primed v)); (BA.Var (primed x))])) (all_sets_but (all_sb.Spec.s) v)) in BA.mk_and [BA.Atom (BA.Cardeq (BA.Var (primed v), 1)); v_disj_all; fram] in let put_v_in_r (v:Id.var_t) (r:Id.var_t) = let r_alts = Hashtbl.find alts r in let fram = frame_except_d all_sb (r::r_alts) in BA.mk_and [(add_v_to_s v r); fram] in (* end helpers *) (* intrinsics *) let have_summary (proc:Id.proc_t) : bool = match ((Id.module_of_proc proc), (Id.name_of_proc proc)) with | ("Sockets", "accept") -> true | _ -> false in let handle_call (lhs0, (proc:Id.proc_t), actuals) f = match ((Id.module_of_proc proc), (Id.name_of_proc proc)) with | ("Sockets", "accept") -> let lhs = (match lhs0 with Some a -> a | None -> failwith "accept w/no retval") in inc "new statement" (assign_new_to_v lhs) f | _ -> f in (* end intrinsics *) let rec analyze_stmt (f:BA.form) (s:Sabsyn.form Iabsyn.stmt) = let rec compute_if_cond (e:Iabsyn.expr) : (BA.form * BA.form) option = let handle_true_branch v r = BA.Atom (BA.Sub (v, r)) in let handle_false_branch v r = BA.Atom (BA.Disjoint [v; r]) in let blow_up_result_tf v r = (handle_true_branch v r, handle_false_branch v r) in let blow_up_result_tt v r r' = (handle_true_branch v r, handle_true_branch v r') in let rec handle_if_cond0 e : (BA.form * BA.form) option = (match e with | EqExpr (FieldAccessExpr (VarExpr (LocalLvalue x), fd), LiteralExpr (Int c)) -> (try let xt = match fetch_type x with TObj t -> t | _ -> raise Not_found in let r = Hashtbl.find triggers (Id.name_of_field fd, xt, c) in Some (blow_up_result_tf (BA.Var x) (BA.Var r)) with Not_found -> None) | EqExpr (FieldAccessExpr (VarExpr (LocalLvalue x), fd), LiteralExpr (Bool false)) -> (* never triggered, due to jimplification? *) (* should be now: less-aggressive jimplification *) (try let xt = match fetch_type x with TObj t -> t | _ -> raise Not_found in let r = Hashtbl.find triggers (Id.name_of_field fd, xt, 0l) in Some (blow_up_result_tf (BA.Var x) (BA.Var r)) with Not_found -> None) | EqExpr (VarExpr (LocalLvalue x), LiteralExpr n) when n = Iabsyn.null_obj & not (is_primitive_value_type (Hashtbl.find tenv x)) -> Some (BA.Atom (BA.Eq (BA.Var x, BA.Emptyset)), BA.Atom (BA.Cardeq (BA.Var x, 1))) | NeqExpr (VarExpr (LocalLvalue x), rhs) -> (match handle_if_cond0 (EqExpr (VarExpr (LocalLvalue x), rhs)) with | Some (f1, f2) -> Some (f2, f1) | None -> None) | FieldAccessExpr (VarExpr (LocalLvalue x), fd) -> (* guaranteed to be bool field, due to typechecking *) (try let xt = match fetch_type x with TObj t -> t | _ -> raise Not_found in let r = Hashtbl.find triggers (Id.name_of_field fd, xt, 1l) in (try let r' = Hashtbl.find triggers (Id.name_of_field fd, xt, 0l) in Some (blow_up_result_tt (BA.Var x) (BA.Var r) (BA.Var r')) with Not_found -> Some (blow_up_result_tf (BA.Var x) (BA.Var r))) with Not_found -> None) | AndExpr (e1, e2) -> (match (handle_if_cond0 e1, handle_if_cond0 e2) with | (Some (f1p, f1m), Some (f2p, f2m)) -> Some (BA.mk_and [f1p; f2p], BA.mk_or [f1m; f2m]) | _ -> None) | VarExpr (LocalLvalue b) -> Some (BA.Atom (BA.Propvar b), BA.Not (BA.Atom (BA.Propvar b))) | VarExpr (RefLvalue b) -> let bn = ms0.Sabsyn.module_name ^ "." ^ b in Some (BA.Atom (BA.Propvar bn), BA.Not (BA.Atom (BA.Propvar bn))) | LiteralExpr (Bool true) -> Some (BA.Atom BA.True, BA.Atom BA.False) | LiteralExpr (Bool false) -> Some (BA.Atom BA.False, BA.Atom BA.True) | NotExpr (e) -> (match handle_if_cond0 e with | Some (f1, f2) -> Some (f2, f1) | None -> None) | _ -> None) in match handle_if_cond0 e with | Some (fp, fm) -> let set_subst = List.map (fun s -> (s, BA.Var (primed s))) (all_sb.Spec.s) in let bool_subst = List.map (fun s -> (s, BA.Propvar (primed s))) (all_sb.Spec.b) in let fp' = BA.subst_propvar bool_subst (BA.subst set_subst fp) in let fm' = BA.subst_propvar bool_subst (BA.subst set_subst fm) in Some (fp', fm') | None -> None in let compute_if_cond_for_branches e = match compute_if_cond e with Some (fp, fm) -> (fp, fm) | None -> (BA.Atom BA.True, BA.Atom BA.True) in let handle_if_cond (e:Iabsyn.expr) (f:BA.form) : (BA.form * BA.form) = let (fp', fm') = compute_if_cond_for_branches e in (BA.mk_and [f;fp'], BA.mk_and [f;fm']) in let verify_while ((inv1:BA.form), expr, body) = let get_assign_modified x fd = (try let xt = match Hashtbl.find tenv x with TObj t -> t | _ -> raise Not_found in List.map fst (!(Hashtbl.find alts_raw (Id.name_of_field fd, xt))) with Not_found -> []) in let infer_modifies all_sb s = let rec infer_modifies0 s = let rec unmunge_frame_cond f = let unmunge_frame_cond_atom a = (match a with | BA.Eq (BA.Var se1, BA.Var se2) -> if (Util.is_primed se1) then [se2] else [se1] | _ -> failwith "not frame cond") in (match f with | BA.And cs -> List.concat (List.map unmunge_frame_cond cs) | BA.Iff (BA.Atom (BA.Propvar p1), (BA.Atom (BA.Propvar p2))) -> if (Util.is_primed p1) then [p2] else [p1] | BA.Atom a -> unmunge_frame_cond_atom a | _ -> failwith "not frame cond") in match s with | EmptyStmt -> [] | HavocStmt _ -> failwith "havoc inappropriate for typestate" | CompoundStmt sl -> List.concat (List.map infer_modifies0 sl) | ChoiceStmt _ -> failwith "choice inappropriate for typestate" | LocalDeclStmt (v, t, expr) -> v :: (infer_modifies0 (ExprStmt expr)) | ExprStmt expr -> (match expr with | AssignExpr (LocalLvalue lv, NewExpr _) -> [lv] | AssignExpr (LocalLvalue y, VarExpr (LocalLvalue x)) -> [y] | AssignExpr (LocalLvalue x, FieldAccessExpr (VarExpr (LocalLvalue y), fd)) -> [x] | AssignExpr (FieldLvalue (VarExpr (LocalLvalue x), fd), _) | AssignExpr (FieldLvalue (VarExpr (RefLvalue x), fd), _) -> x :: get_assign_modified x fd | AssignExpr (LocalLvalue lhs, InvokeExpr (p, actuals)) -> if Intrinsics.is_intrinsic p then [] else let callee = Ast.fetch_spec_proc p.Id.p_name (fetch_translated_spec p.Id.p_module) in lhs :: callee.Sabsyn.modifies | AssignExpr (LocalLvalue lhs, rhs) -> [lhs] | AssignExpr (RefLvalue lhs, rhs) -> [ms0.Sabsyn.module_name ^ "." ^ lhs] | AssignExpr (ArrayLvalue _, _) -> [] | InvokeExpr (p, actuals) -> if Intrinsics.is_intrinsic p then [] else let callee = Ast.fetch_spec_proc p.Id.p_name (fetch_translated_spec p.Id.p_module) in callee.Sabsyn.modifies | LiteralExpr _ | PreIncExpr _ | PostIncExpr _ | PreDecExpr _ | PostDecExpr _ -> [] | _ -> print_string "punting an expr!\n"; []) | ReturnStmt _ -> [] | WhileStmt (_, _, body) -> infer_modifies0 body | AssertStmt (n, a) -> [] | AssumeStmt (n, a) -> [] | PragmaStmt s -> (* ignore pragmas *) [] | IfStmt (_, then_cond, else_cond) -> let t = infer_modifies0 then_cond in let e = infer_modifies0 else_cond in t @ e in frame_except all_sb (!derived_set_idents @ Util.remove_dups (infer_modifies0 s)) in let inv = BA.mk_and (inv1 :: (BA.ba_of_sabsyn (Sabsyn.extract_frame_cond ps)) :: (infer_modifies all_sb pi.Iabsyn.proc_body) :: (BA.ba_of_sabsyn ps.Sabsyn.requires) :: (disjtness_conds @ !derived_set_defns)) in let (fplus, fminus) = handle_if_cond expr inv in let inv' = analyze_stmt fplus body in begin enforce_impl ("prestate must imply loop invariant\n"(* ^ BA.MONA.form_to_mona inv*)) f inv; enforce_impl ("preservation of loop invariant\n" (*^ BA.wrap (BA.MONA.form_to_mona inv') ^ "\n ==>\n" ^ BA.wrap (BA.MONA.form_to_mona inv)*)) inv' inv; end; BA.mk_and [inv1; fminus] in let infer_loop_inv cond body f : BA.form = let count = ref 0 in let (fplus, fminus) = compute_if_cond_for_branches cond in let decide_implication_with_disjt f g = decide_implication "testing implication" fetch_type all_sb (BA.mk_and (disjtness_conds @ !derived_set_defns)) f g in let try_to_verify_loop_inv (f, c, b) = let buf = !impl_failed_reasons in try (ignore (verify_while (f, c, b))); true with Impl_failed -> (* it's ok, we weren't serious anyway. *) (* don't really fail. *) impl_failed_reasons := buf; false in let rec iterate_through_loop f0 panicked = let f0' = (BA.simplify (analyze_stmt (BA.mk_and [f0;fplus]) body)) in (* selects conjuncts of f' which are implied by f *) let pick_implied_parts f f' : BA.form = let rec drop_references_to vts (e:BA.form) = let rec drop_reference_to v e = (match e with | BA.And cs -> let cs' = List.map (fun c -> drop_reference_to v c) cs in BA.mk_and (List.filter (fun c -> not (BA.occurs v c)) cs') | BA.ExistsSet (vts', e') -> BA.ExistsSet (vts', drop_reference_to v e') | _ -> e) in (match vts with | [] -> e | v::tl -> drop_reference_to v (drop_references_to tl e)) in let rec pick_implied_parts0 form_closer f f' = match f' with | BA.And cs -> BA.mk_and (List.map (fun x -> pick_implied_parts0 form_closer f x) cs) | BA.ExistsSet (vts, BA.And e) -> if (decide_implication_with_disjt f (form_closer f')) then f' else (* we do this because the conjuncts might imply f' * severally but not jointly *) let cand = BA.mk_existsSet (vts, BA.mk_and (List.map (fun x -> pick_implied_parts0 (fun y -> BA.mk_existsSet(vts,form_closer y)) f x) e)) in if (decide_implication_with_disjt f (form_closer cand)) then cand else BA.Atom BA.True | BA.ExistsProp (vts, BA.And e) -> if (decide_implication_with_disjt f (form_closer f')) then f' else let cand = BA.mk_existsProp (vts, BA.mk_and (List.map (fun x -> pick_implied_parts0 (fun y -> BA.mk_existsProp(vts,form_closer y)) f x) e)) in if (decide_implication_with_disjt f (form_closer cand)) then cand else pick_implied_parts0 form_closer f (drop_references_to vts (BA.And e)) | _ -> if (decide_implication_with_disjt f (form_closer f')) then f' else BA.Atom BA.True in pick_implied_parts0 (fun x -> x) f f' in let old_implied_by_new = pick_implied_parts f0' f0 in let new_implied_by_old = if panicked then BA.Atom BA.True else (pick_implied_parts f0 f0') in (*Util.msg ("\n f"^(string_of_int !count)^": "); BA.show_form f0; Util.msg ("\n f"^(string_of_int !count)^"': "); BA.show_form f0';*) count := !count + 1; let next_is_panic = panicked or !count >= loop_widening_count in let f1 = BA.mk_and [old_implied_by_new; new_implied_by_old] in Util.msg "\nLoop invariant candidate: "; BA.show_form f1; Util.msg "\n"; if not (try_to_verify_loop_inv (f1, cond, body)) then begin if next_is_panic then Util.warn "Entering super-conservative mode for loop invariant inference."; iterate_through_loop f1 next_is_panic end else f1 in let inv = iterate_through_loop f false in Util.msg "Synthesized loop invariant: "; BA.show_form inv; Util.msg "\n"; (* check loop invariant *) let free_vars = (List.map fst (compute_BA_set_names fetch_type (all_sb.Spec.s))) in let f' = BA.mk_forallSetId (free_vars, universal_close_bool_vars (all_sb.Spec.b) (BA.mk_impl (inv, BA.Atom BA.False))) in if BA.MONA.valid "checking loop invariant dumbness" f' then Util.err "[syn-loop-inv]" "loop invariant implies false!"; inv in (match s with | EmptyStmt -> f | HavocStmt _ -> failwith "havoc inappropriate for typestate" | CompoundStmt sl -> List.fold_left analyze_stmt f sl | ChoiceStmt _ -> failwith "choice inappropriate for typestate" | LocalDeclStmt (v, t, expr) -> analyze_stmt f (ExprStmt (AssignExpr (LocalLvalue v, expr))) | ExprStmt expr -> let analyze_invoke apply_bool_subst rv_subst rv_names p' actuals f = let callee_mod_name = Id.module_of_proc p' in let callee_spec_mod = fetch_translated_spec callee_mod_name in let callee = Ast.fetch_spec_proc p'.Id.p_name callee_spec_mod in (* create formals -> actuals map *) let formals_sub0 = List.map2 (fun (x, xt) y -> ((x, xt), y)) callee.Sabsyn.formals actuals in let formals_sub1 = List.filter (fun (x, _) -> not (is_primitive_value_type (snd x))) formals_sub0 in let formals_sub = List.map (fun (x, y) -> match y with VarExpr (LocalLvalue y') -> (fst x, BA.Var y') | _ -> failwith "not simple actual") formals_sub1 in let formals_sub1_b = List.filter (fun (x, _) -> snd x = TBool) formals_sub0 in let formals_sub_b = List.map (fun (x, y) -> match y with | LiteralExpr (Bool true) -> (fst x, BA.True) | LiteralExpr (Bool false) -> (fst x, BA.False) | VarExpr (LocalLvalue y') -> (fst x, BA.Propvar y') | VarExpr (RefLvalue y') -> let y'' = Util.qualify_if_needed ms.Sabsyn.module_name y' in (fst x, BA.Propvar y'') | _ -> failwith "not simple actual") formals_sub1_b in (* apply formals -> actuals map *) let req1 = BA.subst_propvar formals_sub_b (BA.subst formals_sub (BA.ba_of_sabsyn (augment_with_invariants callee.Sabsyn.proc_name callee.Sabsyn.requires false))) and ens1 = BA.subst_propvar formals_sub_b (BA.subst formals_sub (BA.subst rv_subst (BA.ba_of_sabsyn (augment_with_invariants callee.Sabsyn.proc_name (Sabsyn.construct_ensures callee) true)))) in (* don't forget the return value, if it's a boolean *) let ens2 = apply_bool_subst ens1 in (* prime all sets for requires *) (* must prime all bools too!*) let req' = BA.subst_propvar (List.map (fun x -> (x, BA.Propvar (primed x))) all_sb.Spec.b) (BA.subst (List.map (fun x -> (x, BA.Var (primed x))) all_sb.Spec.s) req1) in (* preserve all local sets for ensures set *) (* preserve relevant global sets too, except those directly in * modifies clause of callee *) let relevant_minus_modifies = { Spec.s = Util.difference all_sb.Spec.s callee.Sabsyn.modifies; Spec.b = Util.difference all_sb.Spec.b callee.Sabsyn.modifies; } in let ens' = BA.mk_and [ens2; frame_except { Spec.s = local_sets @ relevant_minus_modifies.Spec.s; Spec.b = local_bools @ relevant_minus_modifies.Spec.b; } rv_names] in let ens'' = BA.mk_and (ens' :: disjtness_conds @ !derived_set_defns) in let msg = Printf.sprintf "requires clause in a call to procedure %s.%s" callee_mod_name (Id.name_of_proc p') in enforce_impl msg f req'; inc "proc call" ens'' f in let get_assign_fn_unknown x fd = (try let xt = match Hashtbl.find tenv x with TObj t -> t | _ -> raise Not_found in let removals = List.map fst (!(Hashtbl.find alts_raw (Id.name_of_field fd, xt))) in let r = (List.map (exclude_v_from_s (BA.Var x)) removals) in let fram = frame_except_d all_sb (removals) in BA.mk_and (fram :: r) with Not_found -> frame_except_d all_sb []) in let get_assign_fn x fd c = let xt = match Hashtbl.find tenv x with TObj t -> t | _ -> failwith "field read on non-Obj" in if (not (Hashtbl.mem alts_raw (Id.name_of_field fd, xt))) then frame_except_d all_sb [] (* don't care about this write *) else let removals = List.map fst (!(Hashtbl.find alts_raw (Id.name_of_field fd, xt))) in if (Hashtbl.mem triggers (Id.name_of_field fd, xt, c)) then let new_set = Hashtbl.find triggers (Id.name_of_field fd, xt, c) in let removals' = List.filter (fun x -> x != new_set) removals in let r = List.map (exclude_v_from_s (BA.Var x)) removals' in BA.mk_and ((put_v_in_r x new_set) :: r) else get_assign_fn_unknown x fd in let explicit_bool lhs e = match e with | LiteralExpr (Bool true) -> Some (BA.Atom (BA.Propvar (primed lhs))) | LiteralExpr (Bool false) -> Some (BA.Not (BA.Atom (BA.Propvar (primed lhs)))) | _ -> None in (match expr with (* booleans *) (* objects *) | AssignExpr (LocalLvalue lv, NewExpr _) -> inc "new statement" (assign_new_to_v lv) f | AssignExpr (LocalLvalue y, VarExpr (LocalLvalue x)) -> let xt = fetch_type x in (match xt with | TBool -> inc "assignment to local" (y_iff_x y x) f | TInt | TFloat | TString | TByte | TArray _ -> f | TObj _ -> inc "assignment to local" (y_gets_x y x) f | _ -> failwith "unexpected assignment") (* x = y.f *) | AssignExpr (LocalLvalue x, FieldAccessExpr (VarExpr (LocalLvalue y), fd)) -> let xt = fetch_type x in if (xt = TBool) then begin let yt = string_of_value_type (fetch_type y) in let fram = frame_except_d all_sb [x] in let trigger_t = (Id.name_of_field fd, yt, 1l) in let trigger_f = (Id.name_of_field fd, yt, 0l) in let a1 = if Hashtbl.mem triggers trigger_t then let new_set = Hashtbl.find triggers trigger_t in BA.Iff (BA.Atom (BA.Propvar (primed x)), BA.Atom (BA.Sub (BA.Var y, BA.Var new_set))) else BA.Atom BA.True in let a2 = if Hashtbl.mem triggers trigger_f then let new_set' = Hashtbl.find triggers trigger_f in BA.Iff (BA.Not (BA.Atom (BA.Propvar (primed x))), BA.Atom (BA.Sub (BA.Var y, BA.Var new_set'))) else BA.Atom BA.True in inc "field assignment" (BA.mk_and [a1; a2; fram]) f end else let fram = frame_except_d all_sb [x] in inc "dropping value for field assignment" fram f (* x.f = y *) | AssignExpr (FieldLvalue (VarExpr (LocalLvalue x), fd), LiteralExpr (Int c)) | AssignExpr (FieldLvalue (VarExpr (RefLvalue x), fd), LiteralExpr (Int c)) -> inc "assignment of const to field" (get_assign_fn x fd c) f | AssignExpr (FieldLvalue (VarExpr (LocalLvalue x), fd), LiteralExpr (Bool b)) | AssignExpr (FieldLvalue (VarExpr (RefLvalue x), fd), LiteralExpr (Bool b)) -> inc "assignment of bool to field" (get_assign_fn x fd (if b then 1l else 0l)) f | AssignExpr (FieldLvalue (VarExpr (LocalLvalue x), fd), VarExpr (LocalLvalue y)) | AssignExpr (FieldLvalue (VarExpr (RefLvalue x), fd), VarExpr (LocalLvalue y)) -> let yt = fetch_type y in if (yt = TBool) then let a1 = BA.mk_and [BA.Atom (BA.Propvar y); (get_assign_fn x fd 1l)] in let a2 = BA.mk_and [BA.Not (BA.Atom (BA.Propvar y)); (get_assign_fn x fd 0l)] in inc "assignment to field" (BA.Or [a1; a2]) f else f | AssignExpr (FieldLvalue (VarExpr (LocalLvalue x), fd), _) | AssignExpr (FieldLvalue (VarExpr (RefLvalue x), fd), _) -> inc "unknown assignment to field" (get_assign_fn_unknown x fd) f (* x = foo() *) | AssignExpr (LocalLvalue lhs, InvokeExpr (p, actuals)) -> if Intrinsics.is_intrinsic p then (* doesn't account for side effects of p, but at least accounts for return value *) if have_summary p then handle_call (Some lhs, p, actuals) f else inc "dropping retval from intrinsic " (frame_except_d all_sb [lhs]) f else (* also should support local calls by inlining, * without need for spec. *) let callee = Ast.fetch_spec_proc p.Id.p_name (fetch_translated_spec p.Id.p_module) in let rv = match callee.Sabsyn.ret_val with None -> failwith "assigning from retval of a void fn" | Some x -> x in let rv_type = snd rv in let apply_bool_subst f = if (rv_type = TBool) then BA.subst_propvar [(primed (fst rv), BA.Propvar (primed lhs)); (fst rv, BA.Propvar (primed lhs))] f else f in let rv_subst = if (is_primitive_value_type rv_type) then [] else [(primed (fst rv), BA.Var (primed lhs)); (fst rv, BA.Var (primed lhs))] in let rv_names = [lhs] in analyze_invoke apply_bool_subst rv_subst rv_names p actuals f (* uncaught assignments *) | AssignExpr (LocalLvalue lhs, rhs) -> if (rhs = LiteralExpr null_obj & not (is_primitive_value_type (Hashtbl.find tenv lhs))) then inc "local gets null" (set_v_to_null lhs) f else (let f0 = explicit_bool lhs rhs in match f0 with | Some ef -> let fram = frame_except_d all_sb [lhs] in let f1 = BA.mk_and [ef; fram] in inc "assignment of bool to local" f1 f | None -> (match rhs with | NotExpr (VarExpr (LocalLvalue b)) -> inc "assignment to bool" (b'_gets_not_b lhs b) f | _ -> (let t = fetch_type lhs in match t with | TBool -> let lp = BA.Atom (BA.Propvar (primed lhs)) in (match (compute_if_cond rhs) with | Some (fp, fm) -> inc "assignment to bool" (BA.mk_and [BA.mk_iff (lp, fp); BA.mk_iff (BA.Not lp, fm); frame_except_d all_sb [lhs]]) f | None -> inc "dropping bool" (frame_except_d all_sb [lhs]) f) | TObj _ -> if (BA.occurs (primed lhs) f) then (* if we don't do that check, we explode *) let fram = frame_except_d all_sb [lhs] in inc "assignment" fram f else f | _ -> f))) | AssignExpr (RefLvalue lhs0, rhs) -> (let t = snd (List.find (fun x -> fst x = lhs0) mi.references) in match t with | TBool -> let lhs = Util.qualify_if_needed ms.Sabsyn.module_name lhs0 in if (BA.occurs (primed lhs) f) then (* if we don't do that check, we explode *) let fram = frame_except_d all_sb [lhs] in (* could also use compute_if_cond, which is stronger *) (let f0 = explicit_bool lhs rhs in match f0 with | Some ef -> let f1 = BA.mk_and [ef; fram] in inc "assignment" f1 f | None -> inc "assignment" fram f) else f | _ -> f) | AssignExpr (ArrayLvalue _, _) -> f | InvokeExpr (p, actuals) -> if Intrinsics.is_intrinsic p then f else (* hide return value if appropriate *) let callee = Ast.fetch_spec_proc p.Id.p_name (fetch_translated_spec p.Id.p_module) in let apply_bool_subst f = match callee.Sabsyn.ret_val with | Some (rvn, TBool) -> BA.mk_existsProp ([primed rvn; rvn], f) | _ -> f in analyze_invoke apply_bool_subst [] [] p actuals f (* inc, dec *) | PreIncExpr lv | PostIncExpr lv | PreDecExpr lv | PostDecExpr lv -> (match lv with | FieldLvalue (VarExpr (LocalLvalue x), fd) -> inc "post/pre inc/dec" (get_assign_fn_unknown x fd) f | FieldLvalue _ -> failwith "unjimplified" | _ -> f) | _ -> print_string "punting an expr!\n"; BA.Atom BA.True) | ReturnStmt None -> extra_results := f :: !extra_results; BA.Atom BA.False | ReturnStmt Some expr -> (match ps.Sabsyn.ret_val with None -> failwith "no retval" | Some (rv, _) -> let f' = analyze_stmt f (ExprStmt (AssignExpr (LocalLvalue rv, expr))) in extra_results := f' :: !extra_results; BA.Atom BA.False) | WhileStmt (inv0, expr, body) -> let inv = (match inv0 with Some inv1 -> if !ignore_invariants then begin let inv_explicit = BA.ba_of_sabsyn inv1 in let inv_inferred = infer_loop_inv expr body f in Util.amsg ("[typestate] inferred a loop invariant; comparing to stated invariant...\n"); let inf_implies_explicit = decide_implication "inferred -> explicit" fetch_type all_sb (BA.mk_and (disjtness_conds @ !derived_set_defns)) inv_inferred inv_explicit in let explicit_implies_inf = decide_implication "explicit -> inferred" fetch_type all_sb (BA.mk_and (disjtness_conds @ !derived_set_defns)) inv_explicit inv_inferred in Util.amsg ("inferred invariant is: "^(BA.MONA.form_to_mona inv_inferred)^"\n"); Util.amsg ("explicit invariant was: "^(BA.MONA.form_to_mona inv_explicit)^"\n"); Util.amsg ("inferred implies explicit: "^(string_of_bool inf_implies_explicit)^"\n"); Util.amsg ("explicit implies inferred: "^(string_of_bool explicit_implies_inf)^"\n"); inv_inferred end else BA.ba_of_sabsyn inv1 | None -> infer_loop_inv expr body f) in verify_while (inv, expr, body) | AssertStmt (n, a) -> begin let nm = match n with Some s -> s | None -> "" in enforce_impl ("assertion " ^ nm) f (BA.ba_of_sabsyn a); f end | AssumeStmt (n, a) -> let ba = BA.ba_of_sabsyn a in Util.amsg ("[typestate] making the assumption: " ^ (BA.MONA.form_to_mona ba)^".\n"); BA.mk_and [f; ba] | PragmaStmt s -> (* ignore pragmas *) Format.printf "Warning: ignoring pragma %s\n" s; f | IfStmt (expr, then_cond, else_cond) -> let (fplus, fminus) = handle_if_cond expr f in BA.mk_optimized_or [(analyze_stmt fplus then_cond); (analyze_stmt fminus else_cond)]) in let req = BA.ba_of_sabsyn ps.Sabsyn.requires in let initial_fact = to_relation all_sb req in let ens = (BA.ba_of_sabsyn (Sabsyn.construct_ensures ps)) in try begin print_string ("Analyzing proc " ^ p ^ "... "); flush_all (); extra_results := []; let primary_result = analyze_stmt initial_fact pi.proc_body in (match pi.ret_val with | None -> BA.MONA.log "Checking ensures clause..."; (try enforce_impl ("procedure "^p^"() end ensures clause") primary_result ens with Impl_failed -> begin diagnose_fault_in_implication primary_result ps; raise Impl_failed end) | Some _ -> if not (primary_result = BA.Atom BA.False) then Util.err "[proc]" "apparently falling off the end of a non-void proc"); if (!extra_results <> []) then BA.MONA.log "Checking additional ensures clauses..."; List.iter (fun e -> enforce_impl "return statement additional ensures clause" e ens) !extra_results; Printf.printf "Procedure %s passes.\n" p; true end with Impl_failed -> begin print_string ("Error(s) found analyzing procedure " ^ p ^ ": \n"); List.iter (fun msg -> print_string msg; print_string ".\n") !impl_failed_reasons; Printf.printf "Procedure %s FAILS.\n" p; false end (* end of analyze_proc *) in let truth = let results = List.map analyze_proc pn in List.fold_left (fun x y -> x & y) true results in if (!Util.verbose) then BA.print_stats (); truth