open Iabsyn open Vcform type vcgen_abst_body = form Aabsyn.abst_body type vcgen_impl_module = form Iabsyn.impl_module let is_cheating_for_spec_invokes = false let show_stmt s = Iabsynprinter.pstmt 2 Vcprint.isabelle_formula s let vcform_convert_abst_body (ast:string Aabsyn.abst_body) : vcgen_abst_body = let parse = Vcformparseutil.parse_formula in let rec vcform_clause_convert f = let rec vcform_clause_convert0 f = match f with | Aabsyn.LetClause (sd, c') -> failwith "not supporting let in aabsyn" | Aabsyn.IffClause (s, t) -> (mk_iff (vcform_clause_convert0 s, vcform_clause_convert0 t)) | Aabsyn.OrClause (s, t) -> (mk_or [vcform_clause_convert0 s; vcform_clause_convert0 t]) | Aabsyn.AndClause (s, t) -> (mk_and [vcform_clause_convert0 s; vcform_clause_convert0 t]) | Aabsyn.NotClause n -> (mk_not (vcform_clause_convert0 n)) | Aabsyn.FormulaClause f' -> (parse f') in Aabsyn.FormulaClause (vcform_clause_convert0 f) and vcform_set_defn_rhs_convert sd = match sd with | Aabsyn.IdForm id -> Aabsyn.IdForm id | Aabsyn.BaseForm bsd -> Aabsyn.BaseForm { Aabsyn.x = bsd.Aabsyn.x; Aabsyn.xt = bsd.Aabsyn.xt; Aabsyn.expr = vcform_clause_convert bsd.Aabsyn.expr; } | Aabsyn.UnionForm (l, r) -> Aabsyn.UnionForm (vcform_set_defn_rhs_convert l, vcform_set_defn_rhs_convert r) | Aabsyn.IntersectionForm (l, r) -> Aabsyn.IntersectionForm (vcform_set_defn_rhs_convert l, vcform_set_defn_rhs_convert r) | Aabsyn.DiffForm (l, r) -> Aabsyn.DiffForm (vcform_set_defn_rhs_convert l, vcform_set_defn_rhs_convert r) and vcform_set_defn_convert sd = (fst sd, vcform_set_defn_rhs_convert (snd sd)) in { Aabsyn.plugin = ast.Aabsyn.plugin; Aabsyn.invariants = List.map vcform_clause_convert ast.Aabsyn.invariants; Aabsyn.set_defns = List.map vcform_set_defn_convert ast.Aabsyn.set_defns; Aabsyn.pred_vars = ast.Aabsyn.pred_vars; Aabsyn.procs_to_analyze = ast.Aabsyn.procs_to_analyze; Aabsyn.formats = ast.Aabsyn.formats; Aabsyn.set_defining_procs = List.map (fun x -> { Aabsyn.proc_name = x.Aabsyn.proc_name; Aabsyn.proc_set_defns = List.map vcform_set_defn_convert x.Aabsyn.proc_set_defns; }) ast.Aabsyn.set_defining_procs; } let vcform_convert_impl_module (ast:string Iabsyn.impl_module) : vcgen_impl_module = let parse = Vcformparseutil.parse_formula in let rec vcform_convert_stmt s = match s with | EmptyStmt -> EmptyStmt | ChoiceStmt (t, u) -> ChoiceStmt (vcform_convert_stmt t, vcform_convert_stmt u) | CompoundStmt cs -> CompoundStmt (List.map vcform_convert_stmt cs) | LocalDeclStmt (v, t, e) -> LocalDeclStmt (v, t, e) | ExprStmt e -> ExprStmt e | ReturnStmt r -> ReturnStmt r | WhileStmt (i, e, w) -> let i' = match i with Some x -> Some (parse (Util.trim_quotes x)) | None -> None in WhileStmt (i', e, vcform_convert_stmt w) | AssertStmt(n, a) -> AssertStmt (n, parse (Util.trim_quotes a)) | AssumeStmt(n, a) -> AssumeStmt (n, parse (Util.trim_quotes a)) | PragmaStmt s -> PragmaStmt s | HavocStmt ids -> HavocStmt ids | IfStmt (e, t, f) -> IfStmt (e, vcform_convert_stmt t, vcform_convert_stmt f) in let vcform_convert_proc p = { proc_id = p.proc_id; proc_modifiers = p.proc_modifiers; formals = p.formals; ret_val = p.ret_val; ensures = (match p.ensures with None -> None | Some x -> Some (parse (Util.trim_quotes x))); modifies = p.modifies; requires = (match p.requires with None -> None | Some x -> Some (parse (Util.trim_quotes x))); proc_body = vcform_convert_stmt 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 vcform_convert_proc ast.procs; } let bail_if_proc_undef e p = if not (Ast.has_impl_proc_by_t p) & not (Ast.has_spec_proc_by_t p) then begin let (fn, pn) = Ast.lookup_expr_pos e in Util.err (fn ^ " " ^ pn) ("couldn't find either spec or impl proc for "^ (Id.module_of_proc p) ^ "." ^ (Id.name_of_proc p)); Util.print_errors (); end let subst_formals_to_actuals (fs:(Id.var_t * 'a) list) (a:Iabsyn.expr list) = let ae = List.map (fun e -> (* rely on jimplification *) match e with | VarExpr (LocalLvalue lv) -> Var lv | LiteralExpr (Int i) -> mk_int (Int32.to_int i) | _ -> let (fn, pn) = Ast.lookup_expr_pos e in Util.err (fn ^ " " ^ pn) "expected simple var for proc parameter"; Util.print_errors()) a in List.combine (List.map fst fs) ae (* CAVEAT: uses the version in the AST, not the one that's * been locally modified e.g. with invariants *) let summarize_invoke e p actuals = bail_if_proc_undef e p; let t = Vcform.Const (Vcform.BoolConst true) in let havoc_i = if (Ast.has_impl_proc_by_t p) then let pi = Ast.fetch_impl_proc_by_t p in (*List.concat (List.map (subst_formals_to_actuals_by_name pi.formals actuals) pi.modifies)*) pi.modifies else [] in let havoc_s = if (not is_cheating_for_spec_invokes) & (Ast.has_spec_proc_by_t p) then let ps = Ast.fetch_spec_proc_by_t p in ps.Sabsyn.modifies else [] in havoc_i @ havoc_s let summarize_statement s = let add id ids = if List.mem id ids then ids else id::ids in let rec collect s acc = match s with | ExprStmt e -> (match e with | AssignExpr (LocalLvalue lhs, InvokeExpr (p, actuals)) -> if not (Intrinsics.is_intrinsic p) then List.fold_right add (summarize_invoke e p actuals) acc else acc | InvokeExpr (p, actuals) -> if not (Intrinsics.is_intrinsic p) then List.fold_right add (summarize_invoke e p actuals) acc else acc | AssignExpr(LocalLvalue v,rhs) -> add v acc | AssignExpr(RefLvalue v,rhs) -> add v acc | AssignExpr(ArrayLvalue(VarExpr (LocalLvalue v),e2),rhs) -> add v acc | AssignExpr(ArrayLvalue(VarExpr (RefLvalue v),e2),rhs) -> add v acc | AssignExpr(FieldLvalue(base,fld),rhs) -> add (Id.name_of_field fld) acc | _ -> Util.warn ("Vcwp.wp: don't know how to handle expression statement " ^ Iabsynprinter.string_of_expr e); acc) | CompoundStmt ss -> List.fold_right collect ss acc | ChoiceStmt(s1,s2) -> collect s1 (collect s2 acc) | IfStmt(_,_,_) -> failwith "vcgen.extract_proof: if should be desugared" | WhileStmt(_,_,_) -> failwith "vcgen.extract_proof: while should be desugared" | _ -> acc in HavocStmt (collect s []) let parse_set_defns ma = let parse_set_defn sd = let (lhs, rhs) = sd in match rhs with | Aabsyn.BaseForm r -> let e = match r.Aabsyn.expr with Aabsyn.FormulaClause c -> c | _ -> failwith "conversion failed" in (lhs, Binder (Comprehension, [(r.Aabsyn.x, TypeObjRef r.Aabsyn.xt)], e)) | _ -> failwith "can't write derived set defns in vcgen" in List.map parse_set_defn ma.Aabsyn.set_defns let extract_obj_vars typeEnv = let add (v,t) acc = match t with Types.TObj _ -> v::acc | _ -> acc in List.fold_right add typeEnv [] let map_inv_names modn mi ab f = (* give proper internal names to global variables used in user-specified global invariant, a simpler case of apply_defs *) (* find set substitutions -- defined sets in this module *) let sdefs = parse_set_defns ab in let mk_ssubst (id,f) = (Vctrans.mk_set_var id,f) in let sdefs_s = List.map mk_ssubst sdefs in let mk_ssubst' (id,f) = (primed (Vctrans.mk_set_var id),prime_all f) in let sdefs_s' = List.map mk_ssubst' sdefs in (* find substitution for global variables *) let globals = List.map fst mi.references in let mk_gsubst id = (id, Var (Vctrans.mk_global_var modn id)) in let gdefs = List.map mk_gsubst globals in let mk_gsubst' id = (id, Var (Vctrans.mk_global_var modn (primed id))) in let gdefs' = List.map mk_gsubst' globals in (* find predvar substitutions *) let pdefs = ab.Aabsyn.pred_vars in let mk_psubst id = (Vctrans.mk_prop_var (Util.qualify_if_needed modn id), Var (Vctrans.mk_global_var modn id)) in let pdefs_s = List.map mk_psubst pdefs in let mk_psubst' id = (primed (Vctrans.mk_prop_var (Util.qualify_if_needed modn id)), Var (primed (Vctrans.mk_global_var modn id))) in let pdefs_s' = List.map mk_psubst' pdefs in (* apply substitution *) subst (sdefs_s @ sdefs_s' @ gdefs @ gdefs' @ pdefs_s @ pdefs_s') f let apply_defs modn mi (ab:form Aabsyn.abst_body) (locals:Id.var_t list) (f : Vcform.form) = (* map specification under abstraction function *) (* let _ = Util.msg ("\nDeabstracting formula " ^ Vcprint.isabelle_formula f ^ "\n") in *) (* find set substitutions -- defined sets in this module *) let sdefs = parse_set_defns ab in let mk_ssubst (id,f) = (Vctrans.mk_set_var id,map_inv_names modn mi ab f) in let sdefs_s = List.map mk_ssubst sdefs in let mk_ssubst' (id,f) = (primed (Vctrans.mk_set_var id), (prime_all (map_inv_names modn mi ab f))) in let sdefs_s' = List.map mk_ssubst' sdefs in let mk_ssubst1 (id,f) = (Util.unqualify id,map_inv_names modn mi ab f) in let sdefs_s1 = List.map mk_ssubst1 sdefs in let mk_ssubst1' (id,f) = (primed (Util.unqualify id), (prime_all (map_inv_names modn mi ab f))) in let sdefs_s1' = List.map mk_ssubst1' sdefs in (* find substitution for local variables as sets *) let mk_lsubst id = (Vctrans.mk_set_var id, Var (Vctrans.mk_local_var id)) in let ldefs_s = List.map mk_lsubst locals in let mk_lsubst' id = (primed (Vctrans.mk_set_var id), Var (primed (Vctrans.mk_local_var id))) in let ldefs_s' = List.map mk_lsubst' locals in (* find substitution for global variables as sets *) let globals = extract_obj_vars mi.references in let mk_gsubst id = (Vctrans.mk_set_var id, Var (Vctrans.mk_global_var modn id)) in let gdefs_s = List.map mk_gsubst globals in let mk_gsubst' id = (primed (Vctrans.mk_set_var id), Var (primed (Vctrans.mk_global_var modn id))) in let gdefs_s' = List.map mk_gsubst' globals in (* find predvar substitutions *) let pdefs = ab.Aabsyn.pred_vars in let mk_psubst id = (Vctrans.mk_prop_var (Util.qualify_if_needed modn id), Var (Vctrans.mk_global_var modn (Util.unqualify id))) in let pdefs_s = List.map mk_psubst pdefs in let mk_psubst' id = (primed (Vctrans.mk_prop_var (Util.qualify_if_needed modn id)), Var (primed (Vctrans.mk_global_var modn (Util.unqualify id)))) in let pdefs_s' = List.map mk_psubst' pdefs in (* apply substitution *) let res = subst (sdefs_s1 @ sdefs_s1' @ sdefs_s @ sdefs_s' @ ldefs_s @ ldefs_s' @ gdefs_s @ gdefs_s' @ pdefs_s @ pdefs_s') f in (* let _ = Util.msg ("\nDeabstracted formula into " ^ Vcprint.isabelle_formula res ^ "\n") in *) res let get_rep_invariants modn mi ab = let extract_formula c = match c with | Aabsyn.FormulaClause f -> f | _ -> failwith "analyze_module.extract_formula: expected formula clause" in let invs0 = mk_and (List.map extract_formula ab.Aabsyn.invariants) in map_inv_names modn mi ab invs0 let fetch_pre_post modn ms0 mi ma p subst = let mn = Id.module_of_proc p in let ms = if (mn = ms0.Sabsyn.module_name) then ms0 else Ast.fetch_spec mn in let t = Vcform.Const (Vcform.BoolConst true) in let callee_private = ref false in let (precond_i, postcond_i, formals_i) = if (Ast.has_impl_proc_by_t p) then let pi = Ast.fetch_impl_proc_by_t p in callee_private := pi.proc_modifiers.Id.is_private; let parse_option p = match p with | None -> t | Some pp -> Vcformparseutil.parse_formula (Util.trim_quotes pp) in (subst (parse_option pi.requires), subst (parse_option pi.ensures), Some pi.formals) else (t, t, None) in let (precond_s, postcond_s, formals_s) = if (not is_cheating_for_spec_invokes) & (Ast.has_spec_proc (Id.name_of_proc p) ms) then let ps = Ast.fetch_spec_proc (Id.name_of_proc p) ms in callee_private := ps.Sabsyn.proc_modifiers.Id.is_private; (subst (Vctrans.vcexpr_of_sabsyn_form ps.Sabsyn.requires), subst (Vctrans.vcexpr_of_sabsyn_form ps.Sabsyn.ensures), Some ps.Sabsyn.formals) else (t, t, None) in let formals = (match (formals_i, formals_s) with | (Some x, _) -> x | (_, Some y) -> y | _ -> failwith "oops") in let invs = if not !callee_private then get_rep_invariants modn mi ma else t in let locals = extract_obj_vars formals in (apply_defs modn mi ma locals (mk_and [invs; precond_i; precond_s]), apply_defs modn mi ma locals (mk_and [prime_all invs; postcond_i; postcond_s])) let assumify_and_ensurify ms mi ma ens pi s = let modn = mi.module_name in let clone_count = ref 0 in let rec assumify0 s = match s with | AssumeStmt (m, _) -> let wn = match m with | None -> "unlabelled assume stmt in input program" | Some mm -> ("assume stmt labelled "^mm^" in input program") in Util.warn wn; s | IfStmt (e, t, f) -> let t' = assumify0 t in let f' = assumify0 f in let (ve0,ve_well_formed0) = Vctrans.vcexpr_of_iabsyn modn e in let (ve, ve_well_formed) = (prime_all ve0, prime_all ve_well_formed0) in let notve = mk_not ve in CompoundStmt[AssertStmt (Some "if condition well-defined", ve_well_formed); ChoiceStmt (CompoundStmt [AssumeStmt (None, ve); t'], CompoundStmt [AssumeStmt (None, notve); f'])] | WhileStmt (Some inv, e, b) -> let (ve0,ve_well_formed0) = Vctrans.vcexpr_of_iabsyn modn e in let (ve, ve_well_formed) = (prime_all ve0, prime_all ve_well_formed0) in let notve = mk_not ve in let ab = assumify0 b in let b' = ChoiceStmt (CompoundStmt [AssumeStmt (Some "loop exp", ve); ab; AssertStmt (Some "loop inv", inv); AssumeStmt (None, App ((Const (BoolConst false)), []))], AssumeStmt (Some "loop termination", notve)) in CompoundStmt [AssertStmt (Some "while condition well-defined", ve_well_formed); AssertStmt (Some "while precondition", inv); summarize_statement ab; AssumeStmt (Some "while precondition", inv); b'] | WhileStmt (None, e, _) -> let (fn, p) = Ast.lookup_expr_pos e in Util.err (fn ^ " " ^ p) "vcgen needs your loop invariants"; Util.print_errors (); s | CompoundStmt cs -> CompoundStmt (List.map assumify0 cs) | ReturnStmt rs -> (match rs with | None -> CompoundStmt [AssertStmt (Some "ensures clause", ens); AssumeStmt (Some "stop at return", Const (BoolConst false))] | Some e -> let (ve0,ve_well_formed0) = Vctrans.vcexpr_of_iabsyn modn e in let (ve, ve_well_formed) = (prime_all ve0, prime_all ve_well_formed0) in let notve = mk_not ve in let returnParam = fst (Util.unsome pi.ret_val) in let ens' = Vcform.subst [(Vctrans.mk_prop_var returnParam,ve)] ens in CompoundStmt [AssertStmt (Some "return statement well-defined", ve_well_formed0); AssertStmt (Some "ensures clause", ens'); AssumeStmt (Some "stop at return", Const (BoolConst false))]) | ExprStmt e -> (let assumify_invoke p (actuals:Iabsyn.expr list) (rs:(Vcform.ident * Vcform.form) list) = (* we convert an invoke into an assert/havoc/assume triple. *) (* assert, assume get formals -> actuals substitution *) (* assert gets unprimed -> primed substitution *) (* for all modified sets, introduce havoc; create clone * of the modified set in pre-state (var_k) getting var's * pre-state value. *) (* assume gets a further substitution for postconditions: * primed stays; unprimed: if havoced, copy the var_k; * if unhavoced, copy the primed value. *) (* By example: // var c_1 = c // assert is primed precondition, substituting parameters: assert "1 <= i' & i' <= s' & 1 <= largest' & largest' <= s' & PQ' = PQ"; swap(i, largest); // havoc values of all things in modifies clause havoc c; // substitute parameters, and // substitute unprimed globals for the copied globals above assume "(c'[i'] = c_1'[largest']) & (c'[largest'] = c_1'[i']) & (forall k. (k ~= i' & k ~= largest') --> c'[k] = c_1'[k])"; *) if not (Ast.has_impl_proc_by_t p) & not (Ast.has_spec_proc_by_t p) then begin let (fn, pn) = Ast.lookup_expr_pos e in Util.err (fn ^ " " ^ pn) ("couldn't find either spec or impl proc for "^ (Id.module_of_proc p) ^ "." ^ (Id.name_of_proc p)); Util.print_errors (); end; let callee_formals = if (Ast.has_impl_proc_by_t p) then (Ast.fetch_impl_proc_by_t p).formals else (Ast.fetch_spec_proc_by_t p).Sabsyn.formals in let to_havoc = summarize_invoke e p actuals in let clone_map = List.map (fun x -> (x, x^"_"^(string_of_int !clone_count))) to_havoc in let clone_to_vc_map = List.map (fun x -> (x, Var (primed (x^"_"^(string_of_int !clone_count))))) to_havoc in let clones = List.map (fun (y, x) -> LocalDeclStmt (x, Types.TVoid, (*snd (List.find (fun (z, _) -> z = y) mi.references),*) VarExpr (RefLvalue y))) clone_map in clone_count := !clone_count + 1; let params = subst_formals_to_actuals callee_formals actuals in let s = Vcform.subst (List.concat [rs; params]) in let (precond, postcond) = fetch_pre_post modn ms mi ma p s in let unprimed_pcfv = List.filter (fun x -> not (Util.is_primed x)) (Vcform.fv postcond) in let (pc_modified, pc_preserved) = List.partition (fun x -> List.mem x to_havoc) unprimed_pcfv in let pc_subst = List.map (fun x -> (x, Var (primed x))) pc_preserved @ clone_to_vc_map in CompoundStmt (clones @ [AssertStmt (Some "invoke requires", Vcform.prime_all precond); HavocStmt to_havoc; AssumeStmt (Some "invoke ensures", Vcform.subst pc_subst postcond)]) in match e with | AssignExpr (LocalLvalue lhs, InvokeExpr (p, actuals)) -> if Intrinsics.is_intrinsic p then EmptyStmt else let cmn = Id.module_of_proc p in let cms = if (cmn = ms.Sabsyn.module_name) then ms else (Ast.fetch_spec cmn) in let callee = Ast.fetch_spec_proc p.Id.p_name cms in assumify_invoke p actuals [(fst (Util.unsome callee.Sabsyn.ret_val), Var (Vctrans.mk_local_var lhs))] | InvokeExpr (p, actuals) -> if Intrinsics.is_intrinsic p then EmptyStmt else assumify_invoke p actuals [] | _ -> s) | _ -> s in assumify0 s let rec concretize_specs modn mi ma proc (s:form Iabsyn.stmt) = (* map all specs in the assert and assume statements within desugared 's' *) let rec conc s0 = match s0 with | AssertStmt(msg,f) -> let locals = Iabsyn.collect_obj_locals s @ extract_obj_vars proc.formals in AssertStmt(msg,apply_defs modn mi ma locals f) | AssumeStmt(msg,f) -> let locals = Iabsyn.collect_obj_locals s @ extract_obj_vars proc.formals in AssumeStmt(msg,apply_defs modn mi ma locals f) | CompoundStmt ss -> CompoundStmt (List.map conc ss) | ChoiceStmt(s1,s2) -> ChoiceStmt(conc s1, conc s2) | WhileStmt(_,_,_) -> failwith "vcgen.concretize_specs: while should be desugared" | IfStmt(_,_,_) -> failwith "vcgen.concretize_specs: if should be desugared" | _ -> s0 in conc s let rec extract_proof (s:form Iabsyn.stmt) = match s with | PragmaStmt pragma -> if (String.sub pragma 0 6)="proof " then String.sub pragma 6 (String.length pragma - 6) else "" | CompoundStmt ss -> String.concat "\n" (List.filter (fun x -> x<>"") (List.map extract_proof ss)) | ChoiceStmt(s1,s2) -> let p1 = extract_proof s1 in let p2 = extract_proof s2 in if (p1<>"" & p2<>"") then failwith "ambiguous proof" else (if p1="" then p2 else p1) | WhileStmt(_,_,_) -> failwith "vcgen.extract_proof: while should be desugared" | _ -> "" type isabelleOutput = Ok | Error of string let parseIsabelleOutput (fn : string) : isabelleOutput = let okString = "val it = () : unit" in let errorString = "***" in let isErrorLine s = Str.string_match (Str.regexp_string errorString) s 0 in let foundOk = ref false in let foundError = ref false in let errorOutput = ref "" in let line = ref "" in let chn = open_in fn in begin line := input_line chn; (try while true do if !line = okString then foundOk := true else (); if isErrorLine !line then begin errorOutput := !errorOutput ^ !line ^ "\n"; foundError := true end else (); line := input_line chn done with End_of_file -> ()); close_in chn; if !foundOk & not (!foundError) then Ok else Error !errorOutput end let generate_sequents (f:form) : sequent list = let add hyp asms = match hyp with | App(Const And,fs) -> List.rev_append fs asms | _ -> hyp::asms in let rec gen asms f acc = match f with | App(Const Impl,[f1;f2]) -> gen (add f1 asms) f2 acc | App(Const And,fs) -> gens asms fs acc | Binder(Forall,vts,f1) -> gen asms f1 acc | _ -> (asms,f)::acc and gens asms fs acc = List.fold_right (gen asms) fs acc in gen [] f [] let pending_file_name = "pending-vc.thy" let pending_file = ref None let open_pending () = pending_file := Some (open_out pending_file_name) let close_pending () = match !pending_file with | None -> failwith "vcgen.write_pending: file not init!\n" | Some chn -> (close_out chn; pending_file := None) let write_pending str = match !pending_file with | None -> failwith "vcgen.write_pending: file not init!\n" | Some chn -> output_string chn str let reparse formula = let formula_string = Vcprint.isabelle_formula formula in (formula_string, Vcformparseutil.parse_formula formula_string) let timeout = 10 (* seconds *) let decide_sq (mod_name:string) (proc_name:string) (proof0:string) (sq:sequent) (sqno:int) = let default_simps = "array1_def array2_def array3_def array4_def array5_def cardeq1_def cardleq1_def " in let proof = "by (auto simp add: " ^ default_simps ^ proof0 ^ ")" in let isabelleName = "isabelle" in let vc_file = "vc.thy" in let vc_in = "vc.in" in let vc_out = "vc.out" in let vc_string = Vcprint.string_of_sequent sq in begin Util.msg ("Verification condition:\n" ^ vc_string ^ "\n"); let f = form_of_sequent sq in if Vclemmas.known_fact (reparse f) then (Util.msg ("The verification condition is cached as true.\n"); true) else begin let lemma_string = Vcprint.isabelle_input mod_name proof vc_string in let chn = open_out vc_file in output_string chn lemma_string; close_out chn; let _ = Util.run_with_timeout (isabelleName ^ " < " ^ vc_in ^ " > " ^ vc_out ^ " 2>&1") timeout in flush_all(); (match parseIsabelleOutput vc_out with | Ok -> (Util.msg "VC proved valid.\n"; true) | Error msg -> (Util.msg "Failed to show VC valid.\n"; write_pending ("lemma " ^ proc_name ^ (Printf.sprintf "%d: \"" sqno) ^ Vcprint.string_of_sequent sq ^ "\"\nsorry\n\n"); Util.msg msg; Util.msg "\n\n"; false)) end end let decide (mod_name:string) (proc_name:string) (proof:string) (f:form) = let sqs = generate_sequents f in let len = List.length sqs in let _ = write_pending "theory PendingVC = ArrayVC:\n\n" in let rec prove_all sqs k = match sqs with | [] -> true | sq::sqs1 -> begin Util.msg (Printf.sprintf "Proving sequent %d of %d." k len); if decide_sq mod_name proc_name proof sq k then prove_all sqs1 (k+1) else (prove_all sqs1 (k+1); false) end in begin prove_all sqs 0; end (* Verification of a desugared statement *) let analyze_stmt (p:Id.proc_t) (s:form Iabsyn.stmt) = let mod_name = Id.module_of_proc p in let proc_name = Id.name_of_proc p in Util.msg ("\nAnalyzing statement:\n" ^ Iabsynprinter.pstmt 2 Vcprint.isabelle_formula s ^ "\n"); let vc = unprime_all (Vcwp.wp mod_name s mk_true) in let svc = simplify vc in let proof = extract_proof s in decide mod_name proc_name proof svc let initial_state_formula mi = (* construct formula describing initial state of mi *) let init_of (v,t) = Vcwp.initial_value t v in smk_and (List.map init_of mi.Iabsyn.references) let check_init modn mi ma = (* check that representation invariants hold initially *) let _ = print_string "Checking that initial state implies rep invariants..." in let f = mk_impl(initial_state_formula mi, get_rep_invariants modn mi ma) in let res = decide mi.Iabsyn.module_name "INITIALIZATION" "" f in let _ = if res then print_string " ok.\n" else print_string "FAILED!\n Consider adding a guard.\n" in res let neutral_procs ((ma, ms, mi):string Aabsyn.abst_body * Sabsyn.spec_module * string Iabsyn.impl_module) = [] (* the top-level analysis of a module using vcgen plugin *) (* also uses all loaded spec modules in Ast.spec *) let analyze_module (modn:string) ((ma0,ms,mi0):(string Aabsyn.abst_body * Sabsyn.spec_module * string Iabsyn.impl_module)) (pn:string list) : bool = let mi = vcform_convert_impl_module mi0 in let ma = vcform_convert_abst_body ma0 in let _ = Vclemmas.init mi.module_name in let set_defns = parse_set_defns ma in let analyze_proc (pi:Vcform.form Iabsyn.proc_def) : bool = print_string ("Analyzing proc " ^ (Id.name_of_proc pi.proc_id) ^ "... "); flush_all (); let (precond, postcond) = fetch_pre_post modn ms mi ma pi.proc_id (fun x -> x) in (* desugar entire procedure and spec into a single statement *) let body = Itrans.flatten_compound_stmt (CompoundStmt [AssumeStmt (Some "requires", precond); assumify_and_ensurify ms mi ma postcond pi pi.proc_body; AssertStmt (Some "ensures", postcond)]) in let concretized_body = concretize_specs modn mi ma pi body in let p = Id.name_of_proc pi.proc_id in if (analyze_stmt pi.proc_id concretized_body) then begin Printf.printf "Procedure %s passes.\n" p; true end else begin Printf.printf "Procedure %s fails.\n" p; false end in let _ = open_pending() in let init_ok = check_init modn mi ma in let procs = if pn = [] then ms.Sabsyn.procs else List.filter (fun mm -> List.mem mm.Sabsyn.proc_name.Id.p_name pn) ms.Sabsyn.procs in let results = List.map (fun mm -> analyze_proc (Ast.fetch_impl_proc (Id.name_of_proc mm.Sabsyn.proc_name) mi)) procs in let truth = List.fold_left (fun x y -> x & y) init_ok results in let _ = write_pending "\nend\n" in let _ = close_pending() in truth