diff --git a/GillianCore/GIL_Syntax/Gil_syntax.mli b/GillianCore/GIL_Syntax/Gil_syntax.mli index 33fccd51..47bb5dac 100644 --- a/GillianCore/GIL_Syntax/Gil_syntax.mli +++ b/GillianCore/GIL_Syntax/Gil_syntax.mli @@ -1154,6 +1154,8 @@ module Prog : sig (** Print indexed *) val pp_indexed : Format.formatter -> ?pp_annot:'a Fmt.t -> ('a, int) t -> unit + + val make_callgraph : ('a, 'b) t -> Call_graph.t end (** @canonical Gillian.Gil_syntax.Visitors *) diff --git a/GillianCore/GIL_Syntax/Prog.ml b/GillianCore/GIL_Syntax/Prog.ml index f0bd3b94..bf7d8588 100644 --- a/GillianCore/GIL_Syntax/Prog.ml +++ b/GillianCore/GIL_Syntax/Prog.ml @@ -253,3 +253,27 @@ let add_macro (prog : ('a, 'b) t) (macro : Macro.t) : ('a, 'b) t = let add_bispec (prog : ('a, 'b) t) (bi_spec : BiSpec.t) : ('a, 'b) t = Hashtbl.add prog.bi_specs bi_spec.bispec_name bi_spec; prog + +let make_callgraph (prog : ('a, 'b) t) = + let fcalls = + Hashtbl.fold + (fun _ proc acc -> + Proc.(proc.proc_name, proc.proc_aliases, proc.proc_calls) :: acc) + prog.procs [] + in + let call_graph = Call_graph.make () in + let fnames = Hashtbl.create (List.length fcalls * 2) in + fcalls + |> List.iter (fun (sym, aliases, _) -> + Call_graph.add_proc call_graph sym; + Hashtbl.add fnames sym sym; + aliases |> List.iter (fun alias -> Hashtbl.add fnames alias sym)); + fcalls + |> List.iter (fun (caller, _, callees) -> + callees + |> List.iter (fun callee -> + match Hashtbl.find_opt fnames callee with + | Some callee -> + Call_graph.add_proc_call call_graph caller callee + | None -> ())); + call_graph diff --git a/GillianCore/command_line/act_console.ml b/GillianCore/command_line/act_console.ml index 19f60d6f..abf1c4f7 100644 --- a/GillianCore/command_line/act_console.ml +++ b/GillianCore/command_line/act_console.ml @@ -23,6 +23,10 @@ struct let doc = "Emit specs to stdout, useful for testing." in Arg.(value & flag & info [ "specs-to-stdout" ] ~doc) + let ignored_procs = + let doc = "Procs to ignore" in + Arg.(value & opt_all string [] & info [ "ignore" ] ~doc) + let parse_eprog file files already_compiled = if not already_compiled then let () = @@ -64,30 +68,6 @@ struct let out_path = Filename.concat dirname (fname ^ "_bi.gil") in Io_utils.save_file_pp out_path (Prog.pp_labeled ~pp_annot) e_prog - let make_callgraph (prog : ('a, 'b) Prog.t) = - let fcalls = - Hashtbl.fold - (fun _ proc acc -> - Proc.(proc.proc_name, proc.proc_aliases, proc.proc_calls) :: acc) - prog.procs [] - in - let call_graph = Call_graph.make () in - let fnames = Hashtbl.create (List.length fcalls * 2) in - fcalls - |> List.iter (fun (sym, aliases, _) -> - Call_graph.add_proc call_graph sym; - Hashtbl.add fnames sym sym; - aliases |> List.iter (fun alias -> Hashtbl.add fnames alias sym)); - fcalls - |> List.iter (fun (caller, _, callees) -> - callees - |> List.iter (fun callee -> - match Hashtbl.find_opt fnames callee with - | Some callee -> - Call_graph.add_proc_call call_graph caller callee - | None -> ())); - call_graph - let process_files files already_compiled @@ -109,7 +89,7 @@ struct let+ prog = Gil_parsing.eprog_to_prog ~other_imports:PC.other_imports e_prog in - let call_graph = make_callgraph prog in + let call_graph = Prog.make_callgraph prog in let () = L.normal (fun m -> m "@\n*** Stage 2: DONE transforming the program.@\n") in @@ -134,6 +114,7 @@ struct incremental bi_unroll_depth bi_no_spec_depth + ignored_specs () = let () = Config.current_exec_mode := BiAbduction in let () = PC.initialize BiAbduction in @@ -143,6 +124,7 @@ struct let () = Config.bi_no_spec_depth := bi_no_spec_depth in let () = Config.specs_to_stdout := specs_to_stdout in let () = Config.max_branching := bi_unroll_depth in + let () = Config.bi_ignore_procs := ignored_specs in let () = Config.under_approximation := true in let r = process_files files already_compiled outfile_opt should_emit_specs @@ -156,7 +138,7 @@ struct Term.( const act $ files $ already_compiled $ output_gil $ no_heap $ stats $ should_emit_specs $ specs_to_stdout $ incremental $ bi_unroll_depth - $ bi_no_spec_depth) + $ bi_no_spec_depth $ ignored_procs) let act_info = let doc = diff --git a/GillianCore/command_line/command_line.ml b/GillianCore/command_line/command_line.ml index 268a5ac0..0603f12b 100644 --- a/GillianCore/command_line/command_line.ml +++ b/GillianCore/command_line/command_line.ml @@ -1,5 +1,6 @@ open Cmdliner module ParserAndCompiler = ParserAndCompiler +module Act_console = Act_console module Make (ID : Init_data.S) diff --git a/GillianCore/command_line/command_line.mli b/GillianCore/command_line/command_line.mli index 45eccc43..8e08a165 100644 --- a/GillianCore/command_line/command_line.mli +++ b/GillianCore/command_line/command_line.mli @@ -2,6 +2,15 @@ module ParserAndCompiler = ParserAndCompiler +module Act_console : sig + module Make + (ID : Init_data.S) + (PC : ParserAndCompiler.S with type init_data = ID.t) + (Abductor : + Abductor.S with type init_data = ID.t and type annot = PC.Annot.t) + (Gil_parsing : Gil_parsing.S with type annot = PC.Annot.t) : Console.S +end + module Make (ID : Init_data.S) (CMemory : CMemory.S with type init_data = ID.t) diff --git a/GillianCore/engine/Abstraction/Matcher.ml b/GillianCore/engine/Abstraction/Matcher.ml index 4036171c..75e255a5 100644 --- a/GillianCore/engine/Abstraction/Matcher.ml +++ b/GillianCore/engine/Abstraction/Matcher.ml @@ -1508,8 +1508,6 @@ module Make (State : SState.S) : let successes, errors = Res_list.split res_list in match (!Config.under_approximation, successes, errors) with (* We start by handling the crash cases that should never happen *) - | true, _, _ :: _ -> - L.fail "ERROR: IMPOSSIBLE! MATCHING ERRORS IN UX MODE!!!!" | true, [], _ -> (* Vanished in UX *) match_mp' (rest_search_states, errs_so_far) @@ -1556,7 +1554,7 @@ module Make (State : SState.S) : | Ok res -> Ok res | Error errs -> match_mp' (rest_search_states, errs @ errs_so_far)) - | true, first :: rem, [] -> + | true, first :: rem, _ -> let rem = List.map (fun state -> diff --git a/GillianCore/engine/Abstraction/PState.ml b/GillianCore/engine/Abstraction/PState.ml index 22dce031..b97a4062 100644 --- a/GillianCore/engine/Abstraction/PState.ml +++ b/GillianCore/engine/Abstraction/PState.ml @@ -1,12 +1,19 @@ (** Interface for GIL Predicate States. They are considered to be mutable. *) module type S = sig - include SState.S - type state_t - type abs_t = string * vt list + type abs_t = string * SVal.M.t list module SMatcher : Matcher.S with type state_t = state_t + type t = SMatcher.t = { + state : state_t; + preds : Preds.t; + wands : Wands.t; + pred_defs : MP.preds_tbl_t; + } + + include SState.S with type t := t + val make_p : preds:MP.preds_tbl_t -> init_data:init_data -> @@ -17,6 +24,17 @@ module type S = sig unit -> t + val make_p_from_heap : + pred_defs:MP.preds_tbl_t -> + store:store_t -> + heap:heap_t -> + spec_vars:SS.t -> + wands:Wands.t -> + preds:Preds.t -> + pfs:PFS.t -> + gamma:Type_env.t -> + t + val init_with_pred_table : MP.preds_tbl_t -> init_data -> t (** Get preds of given symbolic state *) @@ -25,6 +43,8 @@ module type S = sig (** Set preds of given symbolic state *) val set_preds : t -> Preds.t -> t + val get_wands : t -> Wands.t + (** Set preds of given symbolic state *) val set_wands : t -> Wands.t -> t @@ -115,6 +135,21 @@ module Make (State : SState.S) : let state = State.make_s ~init_data ~store ~pfs ~gamma ~spec_vars in { state; preds = Preds.init []; wands = Wands.init []; pred_defs = preds } + let make_s_from_heap ~heap:_ ~store:_ ~pfs:_ ~gamma:_ ~spec_vars:_ = + failwith "Calling make_s_from_heap on SState" + + let make_p_from_heap + ~pred_defs + ~store + ~heap + ~spec_vars + ~wands + ~preds + ~pfs + ~gamma = + let sstate = State.make_s_from_heap ~store ~heap ~spec_vars ~pfs ~gamma in + { state = sstate; preds; wands; pred_defs } + let make_s ~init_data:_ ~store:_ ~pfs:_ ~gamma:_ ~spec_vars:_ : t = failwith "Calling make_s on a PState" @@ -146,6 +181,7 @@ module Make (State : SState.S) : let get_preds (astate : t) : Preds.t = astate.preds let set_preds (astate : t) (preds : Preds.t) : t = { astate with preds } let set_wands astate wands = { astate with wands } + let get_wands (astate : t) : Wands.t = astate.wands let assume ?(unfold = false) (astate : t) (v : Expr.t) : t list = let open Syntaxes.List in diff --git a/GillianCore/engine/Abstraction/PState.mli b/GillianCore/engine/Abstraction/PState.mli index 9d9e3e35..16c7f04e 100644 --- a/GillianCore/engine/Abstraction/PState.mli +++ b/GillianCore/engine/Abstraction/PState.mli @@ -1,12 +1,19 @@ (** Interface for GIL General States. They are considered to be mutable. *) module type S = sig - include SState.S - type state_t - type abs_t = string * vt list + type abs_t = string * SVal.M.t list module SMatcher : Matcher.S with type state_t = state_t + type t = SMatcher.t = { + state : state_t; + preds : Preds.t; + wands : Wands.t; + pred_defs : MP.preds_tbl_t; + } + + include SState.S with type t := t + val make_p : preds:MP.preds_tbl_t -> init_data:init_data -> @@ -17,6 +24,17 @@ module type S = sig unit -> t + val make_p_from_heap : + pred_defs:MP.preds_tbl_t -> + store:store_t -> + heap:heap_t -> + spec_vars:SS.t -> + wands:Wands.t -> + preds:Preds.t -> + pfs:PFS.t -> + gamma:Type_env.t -> + t + val init_with_pred_table : MP.preds_tbl_t -> init_data -> t (** Get preds of given symbolic state *) @@ -25,6 +43,8 @@ module type S = sig (** Set preds of given symbolic state *) val set_preds : t -> Preds.t -> t + val get_wands : t -> Wands.t + (** Set wands of given symbolic state *) val set_wands : t -> Wands.t -> t diff --git a/GillianCore/engine/Abstraction/Verifier.ml b/GillianCore/engine/Abstraction/Verifier.ml index aa403e46..44cfc6fa 100644 --- a/GillianCore/engine/Abstraction/Verifier.ml +++ b/GillianCore/engine/Abstraction/Verifier.ml @@ -4,15 +4,12 @@ module DL = Debugger_log module type S = sig type heap_t - type state type m_err type annot - module SPState : - PState.S - with type t = state - and type heap_t = heap_t - and type m_err_t = m_err + module SPState : PState.S with type heap_t = heap_t and type m_err_t = m_err + + type state = SPState.t module SState : SState.S with type t = SPState.state_t and type heap_t = heap_t diff --git a/GillianCore/engine/Abstraction/Verifier.mli b/GillianCore/engine/Abstraction/Verifier.mli index b16073d0..06375d53 100644 --- a/GillianCore/engine/Abstraction/Verifier.mli +++ b/GillianCore/engine/Abstraction/Verifier.mli @@ -1,14 +1,11 @@ module type S = sig type heap_t - type state type m_err type annot - module SPState : - PState.S - with type t = state - and type heap_t = heap_t - and type m_err_t = m_err + module SPState : PState.S with type heap_t = heap_t and type m_err_t = m_err + + type state = SPState.t module SState : SState.S with type t = SPState.state_t and type heap_t = heap_t @@ -71,7 +68,6 @@ module Make S with type heap_t = SPState.heap_t and type m_err = SPState.m_err_t - and type state = SPState.t and module SPState = SPState and module SState = SState and type annot = PC.Annot.t diff --git a/GillianCore/engine/BiAbduction/Abductor.ml b/GillianCore/engine/BiAbduction/Abductor.ml index 6c66424f..f5cf384d 100644 --- a/GillianCore/engine/BiAbduction/Abductor.ml +++ b/GillianCore/engine/BiAbduction/Abductor.ml @@ -13,23 +13,53 @@ module type S = sig unit end -module Make - (SPState : PState.S) - (PC : ParserAndCompiler.S with type init_data = SPState.init_data) - (External : External.T(PC.Annot).S) : - S with type annot = PC.Annot.t and type init_data = PC.init_data = struct +module type SimplifiedSState = + State.S + with type vt = SVal.M.t + and type st = SVal.SESubst.t + and type store_t = SStore.t + +module type BiProcessingS = sig + module NonBiPState : PState.S + + type annot + type init_data + type state_t + + (** Similar to Normaliser.normalise_assertion but all failed normalisations + are discarded, and it produces something of the adapted state type *) + val normalise_assertion : + init_data:init_data -> + prog:'a MP.prog -> + pvars:SS.t -> + Asrt.t -> + state_t list + + val bistate_to_pstate_and_af : state_t -> NonBiPState.t * Asrt.t +end + +(* A bit of hack around as the legacy hardcoded BiState and the new, + simpler, BiAbd combinator approach expose different state types. + We try to aggregate the logic of creating specs and running tests in a single module. *) +module Make_raw + (PC : ParserAndCompiler.S) + (State : SimplifiedSState with type init_data = PC.init_data) + (BiProcess : + BiProcessingS + with type state_t = State.t + and type init_data = State.init_data) + (External : External.T(PC.Annot).S) = +struct module L = Logging module SSubst = SVal.SESubst - module Normaliser = Normaliser.Make (SPState) - module SBAState = BiState.Make (SPState) - module SBAInterpreter = - G_interpreter.Make (SVal.M) (SVal.SESubst) (SStore) (SBAState) (PC) - (External) + module Interp = + G_interpreter.Make (SVal.M) (SVal.SESubst) (SStore) (State) (PC) (External) + (* module Normaliser = Normaliser.Make (SPState) *) - type bi_state_t = SBAState.t - type result_t = SBAInterpreter.result_t - type t = { name : string; params : string list; state : bi_state_t } + type state_t = Interp.state_t + type result_t = Interp.result_t + type t = { name : string; params : string list; state : state_t } type annot = PC.Annot.t type init_data = PC.init_data @@ -40,7 +70,7 @@ module Make List.map (fun x -> (Expr.LVar x, Expr.LVar x)) (SS.elements lvars) in let aloc_bindings = - List.map (fun x -> (Expr.LVar x, Expr.ALoc x)) (SS.elements alocs) + List.map (fun x -> (Expr.ALoc x, Expr.ALoc x)) (SS.elements alocs) in let bindings = lvar_bindings @ aloc_bindings in let bindings' = @@ -54,11 +84,10 @@ module Make SSubst.init bindings' let make_spec - (_ : annot MP.prog) (name : string) (params : string list) - (bi_state_i : bi_state_t) - (bi_state_f : bi_state_t) + (bi_state_i : state_t) + (bi_state_f : state_t) (fl : Flag.t) : Spec.t option = let open Syntaxes.List in let sspecs = @@ -66,46 +95,44 @@ module Make (* HMMMMM *) (* let _ = SBAState.simplify ~kill_new_lvars:true bi_state_f in *) - let state_i, _ = SBAState.get_components bi_state_i in - let state_f, state_af = SBAState.get_components bi_state_f in + let state_i, _ = BiProcess.bistate_to_pstate_and_af bi_state_i in + let state_f, af_asrt = BiProcess.bistate_to_pstate_and_af bi_state_f in let pvars = SS.of_list (Names.return_variable :: params) in L.verbose (fun m -> m - "Going to create a spec for @[%s(%a)@]\n\ - @[AF:@\n\ - %a@]@\n\ - @[Final STATE:@\n\ - %a@]" + "Going to create a spec for @[%s(%a)@]@\n\ + @[@[AF:@ %a@] @[Final STATE: %a@]@]" name Fmt.(list ~sep:comma string) - params SPState.pp state_af SPState.pp state_f); + params Asrt.pp af_asrt BiProcess.NonBiPState.pp state_f); (* Drop all pvars except ret/err from the state *) let () = - SStore.filter_map_inplace (SPState.get_store state_f) (fun x v -> - if x = Names.return_variable then Some v else None) + SStore.filter_map_inplace (BiProcess.NonBiPState.get_store state_f) + (fun x v -> if x = Names.return_variable then Some v else None) in let* post = let _, finals_simplified = - SPState.simplify ~kill_new_lvars:true state_f + BiProcess.NonBiPState.simplify ~kill_new_lvars:true state_f in let+ final_simplified = finals_simplified in List.sort Asrt.compare - (SPState.to_assertions ~to_keep:pvars final_simplified) + (BiProcess.NonBiPState.to_assertions ~to_keep:pvars final_simplified) in let+ pre = - let af_asrt = SPState.to_assertions state_af in let af_subst = make_id_subst af_asrt in - let* af_produce_res = SPState.produce state_i af_subst af_asrt in + let* af_produce_res = + BiProcess.NonBiPState.produce state_i af_subst af_asrt + in match af_produce_res with | Ok state_i' -> let _, simplifieds = - SPState.simplify ~kill_new_lvars:true state_i' + BiProcess.NonBiPState.simplify ~kill_new_lvars:true state_i' in let+ simplified = simplifieds in List.sort Asrt.compare - (SPState.to_assertions ~to_keep:pvars simplified) + (BiProcess.NonBiPState.to_assertions ~to_keep:pvars simplified) | Error _ -> L.verbose (fun m -> m "Failed to produce anti-frame"); [] @@ -159,39 +186,25 @@ module Make Some spec let testify ~init_data ~(prog : annot MP.prog) (bi_spec : BiSpec.t) : t list = + let open Syntaxes.List in L.verbose (fun m -> m "Bi-testifying: %s" bi_spec.bispec_name); - let proc_names = Prog.get_proc_names prog.prog in let params = SS.of_list bi_spec.bispec_params in - let normalise = - Normaliser.normalise_assertion ~init_data ~pred_defs:prog.preds - ~pvars:params - in - let make_test asrt = - match normalise asrt with - | Error _ -> [] - | Ok l -> - List.map - (fun (ss_pre, _) -> - { - name = bi_spec.bispec_name; - params = bi_spec.bispec_params; - state = - SBAState.make ~procs:(SS.of_list proc_names) ~state:ss_pre - ~init_data; - }) - l + (* For each pre in the bispec *) + let* pre, _ = bi_spec.bispec_pres in + let+ state = + BiProcess.normalise_assertion ~init_data ~pvars:params ~prog pre in - List.concat_map (fun (pre, _) -> make_test pre) bi_spec.bispec_pres + { name = bi_spec.bispec_name; params = bi_spec.bispec_params; state } let run_test (ret_fun : result_t -> (Spec.t * Flag.t) option) (prog : annot MP.prog) (test : t) : (Spec.t * Flag.t) list = - let state = SBAState.copy test.state in - let state = SBAState.add_spec_vars state (SBAState.get_lvars state) in + let state = State.copy test.state in + let state = State.add_spec_vars state (State.get_lvars state) in try let opt_results = - SBAInterpreter.evaluate_proc ret_fun prog test.name test.params state + Interp.evaluate_proc ret_fun prog test.name test.params state in let count = ref 0 in let result = @@ -216,11 +229,11 @@ module Make (prog : annot MP.prog) (name : string) (params : string list) - (state_i : bi_state_t) + (state_i : state_t) (result : result_t) : (Spec.t * Flag.t) option = let open Syntaxes.Option in - let process_spec = make_spec prog in - let state_i = SBAState.copy state_i in + let process_spec = make_spec in + let state_i = State.copy state_i in let add_spec spec = try MP.add_spec prog spec with _ -> @@ -228,13 +241,8 @@ module Make (Format.asprintf "When trying to build an MP for %s, I died!" name) in match result with - | RFail { error_state; errors; _ } -> - (* Because of fixes, the state may have changed since between the start of execution - and the failure: the anti-frame might have been modified before immediately erroring. - BiState thus returns, with every error, the state immeditaly before the error happens - with any applied fixes - this is the state that should be used to ensure fixes - don't get lost. *) - let rec find_error_state (aux : SBAInterpreter.err_t list) = + | RFail { error_state; _ } -> + (* let rec find_error_state (aux : Interp.err_t list) = match aux with | [] -> error_state | e :: errs -> ( @@ -242,7 +250,7 @@ module Make | EState (EMem (s, _)) -> s | _ -> find_error_state errs) in - let error_state = find_error_state errors in + let error_state = find_error_state errors in *) let+ spec = process_spec name params state_i error_state Flag.Bug in add_spec spec; (spec, Flag.Bug) @@ -280,6 +288,9 @@ module Make let rec run_tests_aux tests succ_specs err_specs bug_specs i = match tests with | [] -> (succ_specs, err_specs, bug_specs) + | test :: rest when List.mem test.name !Config.bi_ignore_procs -> + Fmt.pr "Skipping %s... (%d/%d)\n@?" test.name i num_tests; + run_tests_aux rest succ_specs err_specs bug_specs (i + 1) | test :: rest -> let rec part3 = function | [] -> ([], [], []) @@ -340,30 +351,41 @@ module Make (fun Spec.{ spec_name = name1; _ } Spec.{ spec_name = name2; _ } -> String.compare name1 name2) in - let bug_specs_txt = - Format.asprintf "@[BUG SPECS:@\n%a@]@\n" - Fmt.(list ~sep:(any "@\n") (MP.pp_spec ~preds:prog.preds)) - (sort_specs bug_specs) - in - let error_specs_txt = - Format.asprintf "@[ERROR SPECS:@\n%a@]@\n" - Fmt.(list ~sep:(any "@\n") (MP.pp_spec ~preds:prog.preds)) - (sort_specs error_specs) - in - let normal_specs_txt = - Format.asprintf "@[SUCCESSFUL SPECS:@\n%a@]@\n" - Fmt.(list ~sep:(any "@\n") (MP.pp_spec ~preds:prog.preds)) - (sort_specs succ_specs) - in + Fmt.pr "Ok 3 - %f@." (Sys.time ()); if !Config.specs_to_stdout then ( + let bug_specs_txt = + Format.asprintf "@[BUG SPECS:@\n%a@]@\n" + Fmt.(list ~sep:(any "@\n") (MP.pp_spec ~preds:prog.preds)) + (sort_specs bug_specs) + in + let error_specs_txt = + Format.asprintf "@[ERROR SPECS:@\n%a@]@\n" + Fmt.(list ~sep:(any "@\n") (MP.pp_spec ~preds:prog.preds)) + (sort_specs error_specs) + in + let normal_specs_txt = + Format.asprintf "@[SUCCESSFUL SPECS:@\n%a@]@\n" + Fmt.(list ~sep:(any "@\n") (MP.pp_spec ~preds:prog.preds)) + (sort_specs succ_specs) + in L.print_to_all bug_specs_txt; L.print_to_all error_specs_txt; L.print_to_all normal_specs_txt) else ( - L.normal (fun m -> m "%s" bug_specs_txt); - L.normal (fun m -> m "%s" error_specs_txt); - L.normal (fun m -> m "%s" normal_specs_txt)); + L.normal (fun m -> + m "@[BUG SPECS:@\n%a@]@\n" + Fmt.(list ~sep:(any "@\n") (MP.pp_spec ~preds:prog.preds)) + (sort_specs bug_specs)); + L.normal (fun m -> + m "@[SUCCESSFUL SPECS:@\n%a@]@\n" + Fmt.(list ~sep:(any "@\n") (MP.pp_spec ~preds:prog.preds)) + (sort_specs succ_specs)); + L.normal (fun m -> + m "@[SUCCESSFUL SPECS:@\n%a@]@\n" + Fmt.(list ~sep:(any "@\n") (MP.pp_spec ~preds:prog.preds)) + (sort_specs succ_specs))); + (* This is a hack to not count auxiliary functions that are bi-abduced *) let len_succ = List.length succ_specs in @@ -427,7 +449,7 @@ module Make let test_procs_incrementally (prog : annot MP.prog) - ~(init_data : SPState.init_data) + ~(init_data : State.init_data) ~(prev_results : BiAbductionResults.t) ~(reverse_graph : Call_graph.t) ~(changed_procs : string list) @@ -522,7 +544,7 @@ module Make test_procs_incrementally prog ~init_data ~prev_results ~reverse_graph ~changed_procs:proc_changes.changed_procs ~to_test in - let cur_call_graph = SBAInterpreter.call_graph in + let cur_call_graph = Interp.call_graph in let () = Call_graph.prune_procs prev_call_graph to_prune in let call_graph = Call_graph.merge prev_call_graph cur_call_graph in let results = BiAbductionResults.merge prev_results cur_results in @@ -533,11 +555,56 @@ module Make let cur_source_files = Option.value ~default:(SourceFiles.make ()) source_files in - let dyn_call_graph = SBAInterpreter.call_graph in + let dyn_call_graph = Interp.call_graph in let results = test_procs ~init_data ~call_graph prog in write_biabduction_results cur_source_files dyn_call_graph ~diff:"" results end +module Make + (SPState : PState.S) + (PC : ParserAndCompiler.S with type init_data = SPState.init_data) + (External : External.T(PC.Annot).S) : + S with type annot = PC.Annot.t and type init_data = PC.init_data = struct + module Pre_constructions = struct + module Normaliser = Normaliser.Make (SPState) + module SBAState = BiState.Make (SPState) + module SSubst = SVal.SESubst + module L = Logging + + module BiProcess = struct + type state_t = SBAState.t + type init_data = SBAState.init_data + type annot = PC.Annot.t + + module NonBiPState = SPState + + let normalise_assertion + ~(init_data : init_data) + ~(prog : 'a MP.prog) + ~(pvars : SS.t) + assertion = + let open Syntaxes.List in + let+ ss_pre, _ = + match + Normaliser.normalise_assertion ~pred_defs:prog.preds ~init_data + ~pvars assertion + with + | Ok l -> l + | Error _ -> [] + in + SBAState.make ~state:ss_pre ~init_data + + let bistate_to_pstate_and_af bistate = + let post, af = SBAState.get_components bistate in + (post, NonBiPState.to_assertions af) + end + end + + include + Make_raw (PC) (Pre_constructions.SBAState) (Pre_constructions.BiProcess) + (External) +end + module From_scratch (SMemory : SMemory.S) (PC : ParserAndCompiler.S with type init_data = SMemory.init_data) diff --git a/GillianCore/engine/BiAbduction/BiState.ml b/GillianCore/engine/BiAbduction/BiState.ml index d6d3b24f..72febf4b 100644 --- a/GillianCore/engine/BiAbduction/BiState.ml +++ b/GillianCore/engine/BiAbduction/BiState.ml @@ -2,7 +2,7 @@ open Containers open Literal module L = Logging -type 'a _t = { procs : SS.t; state : 'a; af_state : 'a } [@@deriving yojson] +type 'a _t = { state : 'a; af_state : 'a } [@@deriving yojson] module Make (State : SState.S) = struct type heap_t = State.heap_t @@ -19,9 +19,8 @@ module Make (State : SState.S) = struct type action_ret = (t * Expr.t list, err_t) result list - let make ~(procs : SS.t) ~(state : State.t) ~(init_data : State.init_data) : t - = - { procs; state; af_state = State.init init_data } + let make ~(state : State.t) ~(init_data : State.init_data) : t = + { state; af_state = State.init init_data } let lift_error st : State.err_t -> err_t = function | StateErr.EMem e -> StateErr.EMem (st, e) @@ -54,8 +53,7 @@ module Make (State : SState.S) = struct let state' = State.set_store state store in { bi_state with state = state' } - let assume ?(unfold = false) ({ procs; state; af_state } : t) (v : Expr.t) : - t list = + let assume ?(unfold = false) ({ state; af_state } : t) (v : Expr.t) : t list = let new_states = State.assume ~unfold state v in match new_states with | [] -> [] @@ -63,11 +61,10 @@ module Make (State : SState.S) = struct (* Slight optim, we don't copy the anti_frame if we have only one state. *) let rest = List.map - (fun state' -> - { procs; state = state'; af_state = State.copy af_state }) + (fun state' -> { state = state'; af_state = State.copy af_state }) rest in - { procs; state = first_state; af_state } :: rest + { state = first_state; af_state } :: rest let assume_a ?(matching = false) @@ -99,17 +96,12 @@ module Make (State : SState.S) = struct let get_type ({ state; _ } : t) (v : Expr.t) : Type.t option = State.get_type state v - let copy ({ procs; state; af_state } : t) : t = - { procs; state = State.copy state; af_state = State.copy af_state } - - let simplify - ?(save = false) - ?(kill_new_lvars : bool option) - ?matching:_ - ({ procs; state; af_state } : t) : SVal.SESubst.t * t list = - let kill_new_lvars = Option.value ~default:true kill_new_lvars in - let subst, states = State.simplify ~save ~kill_new_lvars state in + let copy ({ state; af_state } : t) : t = + { state = State.copy state; af_state = State.copy af_state } + let simplify ?save ?kill_new_lvars ?matching:_ ({ state; af_state } : t) : + SVal.SESubst.t * t list = + let subst, states = State.simplify ?save ?kill_new_lvars state in let states = List.concat_map (fun state -> @@ -120,7 +112,7 @@ module Make (State : SState.S) = struct | LVar x -> if SS.mem x svars then None else Some x_v | _ -> Some x_v); List.map - (fun af_state -> { procs; state; af_state }) + (fun af_state -> { state; af_state }) (State.substitution_in_place af_subst af_state)) states in @@ -130,10 +122,9 @@ module Make (State : SState.S) = struct let simplify_val ({ state; _ } : t) (v : Expr.t) : Expr.t = State.simplify_val state v - let pp fmt { procs; state; af_state } = - Fmt.pf fmt "PROCS:@\n@[%a@]@\nMAIN STATE:@\n%a@\nANTI FRAME:@\n%a@\n" - Fmt.(iter ~sep:comma SS.iter string) - procs State.pp state State.pp af_state + let pp fmt { state; af_state } = + Fmt.pf fmt "MAIN STATE:@\n%a@\nANTI FRAME:@\n%a@\n" State.pp state State.pp + af_state (* TODO: By-need formatter *) let pp_by_need _ _ _ fmt state = pp fmt state @@ -219,7 +210,6 @@ module Make (State : SState.S) = struct type post_res = (Flag.t * Asrt.t list) option let match_ - (_ : SS.t) (state : State.t) (af_state : State.t) (subst : SVal.SESubst.t) @@ -350,7 +340,7 @@ module Make (State : SState.S) = struct Fmt.(list ~sep:comma Expr.pp) args SVal.SESubst.pp subst_i)); - let { procs; state; af_state } = bi_state in + let { state; af_state } = bi_state in let old_store = State.get_store state in @@ -369,7 +359,7 @@ module Make (State : SState.S) = struct BI-ABDUCTION:@\n\ %a@]@\n" spec.data.spec_name MP.pp spec.mp)); - let ret_states = match_ procs state' af_state subst spec.mp in + let ret_states = match_ state' af_state subst spec.mp in L.( verbose (fun m -> m "Concluding matching With %d results" (List.length ret_states))); @@ -409,7 +399,7 @@ module Make (State : SState.S) = struct let final_state' : State.t = update_store final_state' (Some x) v_ret in (* FIXME: NOT WORKING DUE TO SIMPLIFICATION TYPE CHANGING *) let _ = State.simplify ~matching:true final_state' in - let bi_state : t = { procs; state = final_state'; af_state = af_state' } in + let bi_state : t = { state = final_state'; af_state = af_state' } in L.( verbose (fun m -> @@ -471,26 +461,25 @@ module Make (State : SState.S) = struct let rec execute_action (action : string) - ({ procs; state; af_state } : t) + ({ state; af_state } : t) (args : Expr.t list) : action_ret = let open Syntaxes.List in let* ret = State.execute_action action state args in match ret with - | Ok (state', outs) -> [ Ok ({ procs; state = state'; af_state }, outs) ] + | Ok (state', outs) -> [ Ok ({ state = state'; af_state }, outs) ] | Error err when not (State.can_fix err) -> - [ Error (lift_error { procs; state; af_state } err) ] - | Error err -> ( - match State.get_fixes err with - | [] -> [] (* No fix, we stop *) - | fixes -> - let* fix = fixes in - let state' = State.copy state in - let af_state' = State.copy af_state in - let* state' = fix_list_apply state' fix in - let* af_state' = fix_list_apply af_state' fix in - execute_action action - { procs; state = state'; af_state = af_state' } - args) + [ Error (lift_error { state; af_state } err) ] + | Error err -> + let fixes = State.get_fixes err in + Logging.verbose (fun m -> + m "Attempting to fix %a with candidates: %a" State.pp_err_t err + (Fmt.Dump.list Asrt.pp) fixes); + let* fix = fixes in + let state' = State.copy state in + let af_state' = State.copy af_state in + let* state' = fix_list_apply state' fix in + let* af_state' = fix_list_apply af_state' fix in + execute_action action { state = state'; af_state = af_state' } args let get_equal_values { state; _ } = State.get_equal_values state let get_heap { state; _ } = State.get_heap state diff --git a/GillianCore/engine/BiAbduction/BiState.mli b/GillianCore/engine/BiAbduction/BiState.mli index cc8c081d..12871b11 100644 --- a/GillianCore/engine/BiAbduction/BiState.mli +++ b/GillianCore/engine/BiAbduction/BiState.mli @@ -10,6 +10,6 @@ module Make (BaseState : PState.S) : sig and type init_data = BaseState.init_data and type m_err_t = BaseState.t _t * BaseState.m_err_t - val make : procs:SS.t -> state:BaseState.t -> init_data:init_data -> t + val make : state:BaseState.t -> init_data:init_data -> t val get_components : t -> BaseState.t * BaseState.t end diff --git a/GillianCore/engine/FOLogic/FOSolver.ml b/GillianCore/engine/FOLogic/FOSolver.ml index cc121d66..ac0df42e 100644 --- a/GillianCore/engine/FOLogic/FOSolver.ml +++ b/GillianCore/engine/FOLogic/FOSolver.ml @@ -86,7 +86,11 @@ let check_satisfiability if Expr.Set.is_empty fs then true else if Expr.Set.mem Expr.false_ fs then false else - let result = Smt.is_sat fs (Type_env.as_hashtbl gamma) in + let result = + try Smt.is_sat fs (Type_env.as_hashtbl gamma) + with Smt.SMT_error _ | Smt.SMT_unknown -> + if !Config.under_approximation then false else raise Smt.SMT_unknown + in (* if time <> "" then Utils.Statistics.update_statistics ("FOS: CheckSat: " ^ time) (Sys.time () -. t); *) diff --git a/GillianCore/engine/general_semantics/eSubst.ml b/GillianCore/engine/general_semantics/eSubst.ml index 3c573f15..add2aa03 100644 --- a/GillianCore/engine/general_semantics/eSubst.ml +++ b/GillianCore/engine/general_semantics/eSubst.ml @@ -287,7 +287,7 @@ module Make (Val : Val.S) : S with type vt = Val.t = struct @return unit *) let full_pp fmt (subst : t) = let pp_pair fmt (e, e_val) = - Fmt.pf fmt "@[(%a: %a)@]" Expr.pp e Val.full_pp e_val + Fmt.pf fmt "@[(%a: %a)@]" Expr.full_pp e Val.full_pp e_val in Fmt.pf fmt "[ @[%a@] ]" (Fmt.hashtbl ~sep:Fmt.comma pp_pair) subst diff --git a/GillianCore/engine/general_semantics/general/g_interpreter.ml b/GillianCore/engine/general_semantics/general/g_interpreter.ml index f9bd1fc5..6bfce972 100644 --- a/GillianCore/engine/general_semantics/general/g_interpreter.ml +++ b/GillianCore/engine/general_semantics/general/g_interpreter.ml @@ -453,12 +453,13 @@ struct raise (Interpreter_error (List.map (fun x -> Exec_err.EState x) errs, s)) let check_loop_ids actual expected = - match actual = expected with - | false -> - Fmt.failwith - "Malformed loop structure: current loops: %a; expected loops: %a" - pp_str_list actual pp_str_list expected - | true -> () + if Exec_mode.is_verification_exec !Config.current_exec_mode then + match actual = expected with + | false -> + Fmt.failwith + "Malformed loop structure: current loops: %a; expected loops: %a" + pp_str_list actual pp_str_list expected + | true -> () let rec loop_ids_to_frame_on_at_the_end end_ids start_ids = if end_ids = start_ids then [] diff --git a/GillianCore/engine/symbolic_semantics/SState.ml b/GillianCore/engine/symbolic_semantics/SState.ml index f06375b0..e4c69ad7 100644 --- a/GillianCore/engine/symbolic_semantics/SState.ml +++ b/GillianCore/engine/symbolic_semantics/SState.ml @@ -18,6 +18,14 @@ module type S = sig spec_vars:SS.t -> t + val make_s_from_heap : + heap:heap_t -> + store:store_t -> + pfs:PFS.t -> + gamma:Type_env.t -> + spec_vars:SS.t -> + t + val init : init_data -> t val get_init_data : t -> init_data val clear_resource : t -> t @@ -56,6 +64,14 @@ module Make (SMemory : SMemory.S) : type err_t = (m_err_t, vt) StateErr.t [@@deriving yojson, show] type action_ret = (t * vt list, err_t) result list + let make_s_from_heap + ~(heap : heap_t) + ~(store : store_t) + ~(pfs : PFS.t) + ~(gamma : Type_env.t) + ~(spec_vars : SS.t) : t = + { heap; store; pfs; gamma; spec_vars } + exception Internal_State_Error of err_t list * t module ES = Expr.Set diff --git a/GillianCore/engine/symbolic_semantics/SState.mli b/GillianCore/engine/symbolic_semantics/SState.mli index bbfbc6e8..0b7b1fa8 100644 --- a/GillianCore/engine/symbolic_semantics/SState.mli +++ b/GillianCore/engine/symbolic_semantics/SState.mli @@ -13,6 +13,14 @@ module type S = sig spec_vars:SS.t -> t + val make_s_from_heap : + heap:heap_t -> + store:store_t -> + pfs:PFS.t -> + gamma:Type_env.t -> + spec_vars:SS.t -> + t + val init : init_data -> t val get_init_data : t -> init_data val clear_resource : t -> t diff --git a/GillianCore/engine/symbolic_semantics/Symbolic.ml b/GillianCore/engine/symbolic_semantics/Symbolic.ml index cd5f3a74..0492488f 100644 --- a/GillianCore/engine/symbolic_semantics/Symbolic.ml +++ b/GillianCore/engine/symbolic_semantics/Symbolic.ml @@ -6,6 +6,8 @@ module Values = struct (** @inline *) include SVal.M + + module Subst = SVal.SESubst end (** @canonical Gillian.Symbolic.Subst *) @@ -56,3 +58,9 @@ module Dummy_memory = SMemory.Dummy (** @canonical Gillian.Symbolic.Legacy_s_memory *) module Legacy_s_memory = Legacy_s_memory + +(** @canonical Gillian.Symbolic.Store *) +module Store = SStore + +module SState = SState +module PState = PState diff --git a/GillianCore/lib/gillian.ml b/GillianCore/lib/gillian.ml index 57eec9e6..42ab1b17 100644 --- a/GillianCore/lib/gillian.ml +++ b/GillianCore/lib/gillian.ml @@ -57,8 +57,11 @@ end module Abstraction = struct module MP = Engine.MP module Verifier = Engine.Verifier + module Normaliser = Engine.Normaliser end +module Abductor = Engine.Abductor + (* module Test262 = Test262_main *) (** Modules for logging (to the file log and the report database) *) diff --git a/GillianCore/monadic/delayed.ml b/GillianCore/monadic/delayed.ml index deae9e9a..c1b77bb4 100644 --- a/GillianCore/monadic/delayed.ml +++ b/GillianCore/monadic/delayed.ml @@ -95,6 +95,15 @@ let delayed_eval2 f x y ~curr_pc = let reduce = delayed_eval FOSolver.reduce_expr let resolve_loc = delayed_eval FOSolver.resolve_loc_name +let assume_types e_tys ~curr_pc = + let new_tys = Engine.Typing.reverse_type_lexpr false curr_pc.Pc.gamma e_tys in + match new_tys with + | None -> [] (* type inconsistency, vanish *) + | Some new_tys -> + let new_tys = Engine.Type_env.to_list new_tys in + let new_pc = Pc.extend_types curr_pc new_tys in + [ Branch.make ~pc:new_pc ~value:() ] + let entails = let entails ~pc lhs rhs = let temp_pc = Pc.extend pc lhs in diff --git a/GillianCore/monadic/delayed.mli b/GillianCore/monadic/delayed.mli index dc0413bf..b8c87eca 100644 --- a/GillianCore/monadic/delayed.mli +++ b/GillianCore/monadic/delayed.mli @@ -20,6 +20,7 @@ val if_sure : Expr.t -> then_:(unit -> 'a t) -> else_:(unit -> 'a t) -> 'a t val branch_entailment : (Expr.t * (unit -> 'a t)) list -> 'a t val leak_pc_copy : unit -> Engine.Gpc.t t val branch_on : Expr.t -> then_:(unit -> 'a t) -> else_:(unit -> 'a t) -> 'a t +val assume_types : (Expr.t * Type.t) list -> unit t module Syntax : sig val ( let* ) : 'a t -> ('a -> 'b t) -> 'b t diff --git a/GillianCore/smt/smt.ml b/GillianCore/smt/smt.ml index 9a3e5962..9f408cfb 100644 --- a/GillianCore/smt/smt.ml +++ b/GillianCore/smt/smt.ml @@ -6,6 +6,10 @@ open Syntaxes.Option (* open Ctx *) module L = Logging +exception SMT_error of string + +let exceptf fmt = Fmt.kstr (fun s -> raise (SMT_error s)) fmt + let z3_config = [ ("model", "true"); @@ -350,7 +354,7 @@ let encode_type (t : Type.t) = | ListType -> Type_operations.List.construct | TypeType -> Type_operations.Type.construct | SetType -> Type_operations.Set.construct - with _ -> Fmt.failwith "DEATH: encode_type with arg: %a" Type.pp t + with _ -> exceptf "DEATH: encode_type with arg: %a" Type.pp t module Encoding = struct type kind = @@ -449,7 +453,7 @@ module Encoding = struct | BooleanType -> Bool.construct | ListType -> List.construct | UndefinedType | NullType | EmptyType | NoneType | SetType -> - Fmt.failwith "Cannot simple-wrap value of type %s" + exceptf "Cannot simple-wrap value of type %s" (Gil_syntax.Type.str typ) in construct expr @@ -470,7 +474,7 @@ module Encoding = struct match kind with | Native SetType -> expr | Extended_wrapped -> Ext_lit_operations.Gil_set.access expr - | _ -> failwith "wrong encoding of set" + | _ -> exceptf "wrong encoding of set" let get_string = get_native ~accessor:Lit_operations.String.access end @@ -561,8 +565,7 @@ let rec encode_lit (lit : Literal.t) : Encoding.t = let args = List.map (fun lit -> simple_wrap (encode_lit lit)) lits in list args >- ListType | Constant _ -> raise (Exceptions.Unsupported "Z3 encoding: constants") - with Failure msg -> - Fmt.failwith "DEATH: encode_lit %a. %s" Literal.pp lit msg + with Failure msg -> exceptf "DEATH: encode_lit %a. %s" Literal.pp lit msg let encode_equality (p1 : Encoding.t) (p2 : Encoding.t) : Encoding.t = let open Encoding in @@ -578,7 +581,7 @@ let encode_equality (p1 : Encoding.t) (p2 : Encoding.t) : Encoding.t = else eq p1.expr p2.expr | Simple_wrapped, Simple_wrapped | Extended_wrapped, Extended_wrapped -> eq p1.expr p2.expr - | Native _, Native _ -> failwith "incompatible equality, type error!" + | Native _, Native _ -> exceptf "incompatible equality, type error!" | Simple_wrapped, Native _ | Native _, Simple_wrapped -> eq (simple_wrap p1) (simple_wrap p2) | Extended_wrapped, _ | _, Extended_wrapped -> @@ -652,7 +655,7 @@ let encode_binop (op : BinOp.t) (p1 : Encoding.t) (p2 : Encoding.t) : Encoding.t | M_atan2 | M_pow | StrCat -> - Fmt.failwith "SMT encoding: Costruct not supported yet - binop: %s" + exceptf "SMT encoding: Costruct not supported yet - binop: %s" (BinOp.str op) let encode_unop ~llen_lvars ~e (op : UnOp.t) le = @@ -747,7 +750,7 @@ let encode_quantified_expr match encode_expr ~gamma ~llen_lvars ~list_elem_vars assertion with | { kind = Native BooleanType; expr; consts; extra_asrts } -> (expr, consts, extra_asrts) - | _ -> failwith "the thing inside forall is not boolean!" + | _ -> exceptf "the thing inside forall is not boolean!" in let quantified_vars = quantified_vars @@ -788,7 +791,7 @@ let rec encode_logical_expression in make_const ~typ kind var | ALoc var -> native_const ObjectType var - | PVar _ -> failwith "HORROR: Program variable in pure formula" + | PVar _ -> exceptf "HORROR: Program variable in pure formula" | UnOp (op, le) -> encode_unop ~llen_lvars ~e:le op (f le) | BinOp (le1, op, le2) -> encode_binop op (f le1) (f le2) | NOp (SetUnion, les) -> @@ -1093,7 +1096,7 @@ let lift_model match x with | LVar x -> x | _ -> - failwith "INTERNAL ERROR: SMT lifting of a non-logical variable" + exceptf "INTERNAL ERROR: SMT lifting of a non-logical variable" in let v = lift_val x in let () = diff --git a/GillianCore/smt/smt.mli b/GillianCore/smt/smt.mli index 18cebade..7f3e092d 100644 --- a/GillianCore/smt/smt.mli +++ b/GillianCore/smt/smt.mli @@ -1,6 +1,7 @@ open Gil_syntax exception SMT_unknown +exception SMT_error of string val exec_sat : Expr.Set.t -> (string, Type.t) Hashtbl.t -> Sexplib.Sexp.t option val is_sat : Expr.Set.t -> (string, Type.t) Hashtbl.t -> bool diff --git a/GillianCore/utils/config.ml b/GillianCore/utils/config.ml index fb71dfd9..5070cae6 100644 --- a/GillianCore/utils/config.ml +++ b/GillianCore/utils/config.ml @@ -64,6 +64,7 @@ let bi_dflt = ref true let bi_unfold_depth = ref 1 let bi_unroll_depth = ref 1 let bi_no_spec_depth = ref 0 +let bi_ignore_procs : string list ref = ref [] let delay_entailment = ref true (* If true, will dump a folder containing all smt queries made to the solver *) diff --git a/GillianCore/utils/gillian_result.ml b/GillianCore/utils/gillian_result.ml index 8ba05571..8bed1985 100644 --- a/GillianCore/utils/gillian_result.ml +++ b/GillianCore/utils/gillian_result.ml @@ -53,7 +53,10 @@ module Error = struct msgs | true, AnalysisFailures es -> let len = List.length es in - Fmt.pf fmt "%d analysis failure%s!" len (if len > 1 then "s" else "") + Fmt.pf fmt "%d analysis failure%s!\n%a" len + (if len > 1 then "s" else "") + (Fmt.Dump.list Yojson.Safe.pp) + (List.map analysis_failure_to_yojson es) | false, CompilationError { msg; loc; _ } -> Fmt.pf fmt "Error during compilation, at%a.\n%s" Location.pp_full loc msg diff --git a/transformers/bin/c_bi_abd.ml b/transformers/bin/c_bi_abd.ml new file mode 100644 index 00000000..ffb3df36 --- /dev/null +++ b/transformers/bin/c_bi_abd.ml @@ -0,0 +1,13 @@ +open Prebuilt.Lib.C_ALoc +module SMemory = MonadicSMemory + +module Bi_cli = + Transformers_abductor.Abductor.Cli (MyInitData) (SMemory) (ParserAndCompiler) + (ExternalSemantics) + +let act_cmd = + match Bi_cli.cmds with + | [ Normal cmd ] -> cmd + | _ -> failwith "Unexpected command structure in bi-abduction CLI" + +let () = exit (Cmdliner.Cmd.eval act_cmd) diff --git a/transformers/bin/dune b/transformers/bin/dune index bd74a711..7034e7c4 100644 --- a/transformers/bin/dune +++ b/transformers/bin/dune @@ -13,6 +13,7 @@ t_wisl_s t_wislf t_wislf_a - t_wislf_s) + t_wislf_s + c_bi_abd) (package transformers) - (libraries prebuilt states gillian)) + (libraries prebuilt states gillian transformers_abductor)) diff --git a/transformers/lib/bi_abduction/abductor.ml b/transformers/lib/bi_abduction/abductor.ml new file mode 100644 index 00000000..d79206bb --- /dev/null +++ b/transformers/lib/bi_abduction/abductor.ml @@ -0,0 +1,100 @@ +open Gillian +open Gillian.Symbolic +open Gillian.General +open Gil_syntax +module MP = Gillian.Abstraction.MP +module L = Gillian.Logging +module SSubst = Symbolic.Subst + +(** This functor expects to receive a symbolic memory that was *not* transformed + through the Bi_abd combinator. *) +module Make + (Init_data : States.MyMonadicSMemory.ID) + (SMemory : States.MyMonadicSMemory.S) + (PC : ParserAndCompiler.S with type init_data = Init_data.t) + (External : External.T(PC.Annot).S) : + Abductor.S with type init_data = PC.init_data and type annot = PC.Annot.t = +struct + (* We first construct memory that performs bi-abduction *) + module BiMemory = States.Bi_abd.Make (SMemory) + + (* We lift to legacy memory signature *) + module BiMemoryMonadicLegacy = + States.MyMonadicSMemory.Make (BiMemory) (Init_data) + + module BiMemoryLegacy = Monadic.MonadicSMemory.Lift (BiMemoryMonadicLegacy) + + (* We lift it to Gillian states *) + module BiSState = SState.Make (BiMemoryLegacy) + module SPState = PState.Make (BiSState) + module NonBiMemory = States.MyMonadicSMemory.Make (SMemory) (Init_data) + module NonBiMemoryLegacy = Monadic.MonadicSMemory.Lift (NonBiMemory) + module NonBiSState = SState.Make (NonBiMemoryLegacy) + + (* We define a helper to run functions under bi-abduction *) + + module Normaliser = Abstraction.Normaliser.Make (SPState) + + (* We can now use the standard Abductor loop + (which iterates over the functions of the program to generate specifications). + *) + + module BiProcess = struct + type annot = PC.Annot.t + type state_t = SPState.t + type init_data = Init_data.t + + module NonBiPState = PState.Make (NonBiSState) + + let normalise_assertion ~init_data ~prog ~pvars assertion = + match + Normaliser.normalise_assertion ~init_data ~pred_defs:prog.MP.preds + ~pvars assertion + with + | Ok l -> List.map fst l + | Error _ -> [] + + let bistate_to_pstate_and_af (bi_state : state_t) = + let States.Bi_abd.{ anti_frame; state } = SPState.get_heap bi_state in + let current = + NonBiPState.make_p_from_heap ~pred_defs:bi_state.pred_defs + ~store:(SPState.get_store bi_state) + ~heap:state ~pfs:(SPState.get_pfs bi_state) + ~gamma:(SPState.get_typ_env bi_state) + ~spec_vars:(SPState.get_spec_vars bi_state) + ~wands:(SPState.get_wands bi_state) + ~preds:(SPState.get_preds bi_state) + in + (* To avoid unfeasible matching plans, we bring up equalities that avoid variable disconnection. *) + let anti_frame = + let spatial = + States.Fix.to_asrt ~pred_to_str:SMemory.pred_to_str anti_frame + in + let equalities = + SPState.get_pfs bi_state |> Pure_context.to_list + |> List.filter (function + | Expr.BinOp (_, Equal, _) -> true + | _ -> false) + |> List.map (fun e -> Asrt.Pure e) + in + spatial @ equalities + in + (current, anti_frame) + end + + include Abductor.Make_raw (PC) (SPState) (BiProcess) (External) +end + +module Cli + (Init_data : States.MyMonadicSMemory.ID) + (SMemory : States.MyMonadicSMemory.S) + (PC : ParserAndCompiler.S with type init_data = Init_data.t) + (External : External.T(PC.Annot).S) = +struct + module Gil_parsing = Gil_parsing.Make (PC.Annot) + module Abductor = Make (Init_data) (SMemory) (PC) (External) + + include + Gillian.Command_line.Act_console.Make (Init_data) (PC) (Abductor) + (Gil_parsing) +end diff --git a/transformers/lib/bi_abduction/dune b/transformers/lib/bi_abduction/dune new file mode 100644 index 00000000..0e23e1e5 --- /dev/null +++ b/transformers/lib/bi_abduction/dune @@ -0,0 +1,4 @@ +(library + (name transformers_abductor) + (public_name transformers.abductor) + (libraries gillian states)) diff --git a/transformers/lib/dune b/transformers/lib/dune deleted file mode 100644 index ed98c29b..00000000 --- a/transformers/lib/dune +++ /dev/null @@ -1,2 +0,0 @@ -(library - (name transformers_lib)) diff --git a/transformers/lib/prebuilt/C.ml b/transformers/lib/prebuilt/C.ml index dd84b9d6..2606b930 100644 --- a/transformers/lib/prebuilt/C.ml +++ b/transformers/lib/prebuilt/C.ml @@ -89,8 +89,7 @@ module ExtendMemory (S : C_PMapType) = struct | _ -> false let map_fixes mapper = - States.MyUtils.deep_map - (States.MyAsrt.map_cp (fun (p, i, o) -> (mapper p, i, o))) + States.MyUtils.deep_map (fun (p, i, o) -> (mapper p, i, o)) let get_fixes = function | BaseError e -> S.get_fixes e |> map_fixes S.pred_to_str @@ -150,7 +149,7 @@ module ExternalSemantics = module InitData = Cgil_lib.Global_env module MyInitData = struct - type t = InitData.t + type t = InitData.t [@@deriving yojson] let init = C_states.CGEnv.set_init_data end diff --git a/transformers/lib/prebuilt/c_states/BlockTree.ml b/transformers/lib/prebuilt/c_states/BlockTree.ml index 531dbc91..10ac9b51 100644 --- a/transformers/lib/prebuilt/c_states/BlockTree.ml +++ b/transformers/lib/prebuilt/c_states/BlockTree.ml @@ -5,7 +5,6 @@ module DR = Delayed_result module DO = Delayed_option module SS = Gillian.Utils.Containers.SS module CoreP = Constr.Core -module MyAsrt = States.MyAsrt (* Import from Cgil lib: *) module CConstants = Cgil_lib.CConstants @@ -486,20 +485,24 @@ module Node = struct DR.ok (SVArr.AllUndef, exact_perm) let encode ~(perm : Perm.t) ~(chunk : Chunk.t) (sval : SVal.t) = - let mem_val = + let open Delayed.Syntax in + let+ mem_val = match (sval, chunk) with | ( SVint _, (Mint8signed | Mint8unsigned | Mint16signed | Mint16unsigned | Mint32) ) | SVlong _, Mint64 | SVsingle _, Mfloat32 - | SVfloat _, Mfloat64 -> Single { chunk; value = sval } + | SVfloat _, Mfloat64 -> Delayed.return (Single { chunk; value = sval }) | SVlong _, Mptr when Compcert.Archi.ptr64 -> - Single { chunk; value = sval } + Delayed.return (Single { chunk; value = sval }) | SVint _, Mptr when not Compcert.Archi.ptr64 -> - Single { chunk; value = sval } - | Sptr _, c when Chunk.could_be_ptr c -> Single { chunk; value = sval } - | _ -> Single { chunk; value = SUndefined } + Delayed.return (Single { chunk; value = sval }) + | Sptr _, c when Chunk.could_be_ptr c -> + Delayed.return (Single { chunk; value = sval }) + | _ -> + if !Gillian.Utils.Config.under_approximation then Delayed.vanish () + else Delayed.return (Single { chunk; value = SUndefined }) in MemVal { exact_perm = Some perm; min_perm = perm; mem_val } @@ -640,17 +643,18 @@ module Tree = struct in Delayed.return { node = new_node; span; children = Some (left, right) } - let remove_node x = Ok (make ~node:(NotOwned Totally) ~span:x.span ()) + let remove_node x = DR.ok (make ~node:(NotOwned Totally) ~span:x.span ()) let sval_leaf ~low ~perm ~value ~chunk = - let node = Node.encode ~perm ~chunk value in + let open Delayed.Syntax in + let+ node = Node.encode ~perm ~chunk value in let span = Range.of_low_and_chunk low chunk in - make ~node ~span () + Ok (make ~node ~span ()) let sarr_leaf ~low ~perm ~size ~array ~chunk = let node = Node.encode_arr ~perm ~chunk array in let span = Range.of_low_chunk_and_size low chunk size in - make ~node ~span () + DR.ok (make ~node ~span ()) let undefined ?(perm = Perm.Freeable) span = make ~node:(Node.undefined ~perm) ~span () @@ -780,9 +784,8 @@ module Tree = struct Range.is_equal range t.span then ( log_string "Range does equal span, replacing."; - match replace_node t with - | Ok new_tree -> DR.ok (t, new_tree) - | Error err -> DR.error err) + let++ new_tree = replace_node t in + (t, new_tree)) else match t.children with | Some (left, right) -> @@ -793,7 +796,7 @@ module Tree = struct then let l, h = range in let upper_range = (mid, h) in - let dont_replace_node = Result.ok in + let dont_replace_node = DR.ok in if%sat (* High-range already good *) Range.is_equal upper_range right.span @@ -871,7 +874,7 @@ module Tree = struct let prod_node (t : t) range node : (t, err) DR.t = let open DR.Syntax in - let replace_node _ = Ok (make ~node ~span:range ()) in + let replace_node _ = DR.ok (make ~node ~span:range ()) in let rebuild_parent = of_children in let++ _, t = frame_range t ~replace_node ~rebuild_parent range in t @@ -897,7 +900,7 @@ module Tree = struct (perm : Perm.t) : (t, err) DR.t = let open DR.Syntax in let open Delayed.Syntax in - let replace_node _ = Ok (sarr_leaf ~low ~chunk ~array ~size ~perm) in + let replace_node _ = sarr_leaf ~low ~chunk ~array ~size ~perm in let rebuild_parent = of_children in let range = Range.of_low_chunk_and_size low chunk size in let** _, t = frame_range t ~replace_node ~rebuild_parent range in @@ -922,7 +925,7 @@ module Tree = struct (sval : SVal.t) (perm : Perm.t) : (t, err) DR.t = let open DR.Syntax in - let replace_node _ = Ok (sval_leaf ~low ~chunk ~value:sval ~perm) in + let replace_node _ = sval_leaf ~low ~chunk ~value:sval ~perm in let rebuild_parent = of_children in let range = Range.of_low_and_chunk low chunk in let++ _, t = frame_range t ~replace_node ~rebuild_parent range in @@ -935,17 +938,17 @@ module Tree = struct let replace_node node = match node.node with | Node.NotOwned Totally -> - Error (MissingResource (Fixable { is_store = false; low; chunk })) + DR.error (MissingResource (Fixable { is_store = false; low; chunk })) | Node.NotOwned Partially -> Logging.verbose (fun fmt -> fmt "SHeapTree Load Error: Memory Partially Not Owned (Currently \ Unsupported)"); - Error (MissingResource Unfixable) + DR.error (MissingResource Unfixable) | MemVal { min_perm; _ } -> - if min_perm >=% Readable then Ok node + if min_perm >=% Readable then DR.ok node else - Error + DR.error (InsufficientPermission { required = Readable; actual = min_perm }) in let rebuild_parent = with_children in @@ -961,18 +964,18 @@ module Tree = struct let replace_node node = match node.node with | NotOwned Totally -> - Error (MissingResource (Fixable { is_store = true; low; chunk })) + DR.error (MissingResource (Fixable { is_store = true; low; chunk })) | NotOwned Partially -> Logging.verbose (fun fmt -> fmt "SHeapTree Store Error: Memory Partially Not Owned (Currently \ Unsupported)"); - Error (MissingResource Unfixable) + DR.error (MissingResource Unfixable) | MemVal { min_perm; _ } -> if min_perm >=% Writable then - Ok (sval_leaf ~low ~chunk ~value:sval ~perm:min_perm) + sval_leaf ~low ~chunk ~value:sval ~perm:min_perm else - Error + DR.error (InsufficientPermission { required = Writable; actual = min_perm }) in let rebuild_parent = of_children in @@ -1021,16 +1024,16 @@ module Tree = struct let replace_node node = match node.node with | NotOwned Totally -> - Error (MissingResource Unfixable) (* No chunk available to fix *) + DR.error (MissingResource Unfixable) (* No chunk available to fix *) | NotOwned Partially -> Logging.verbose (fun fmt -> fmt "SHeapTree Drop Permission Error: Memory Partially Not Owned \ (Currently Unsupported)"); - Error (MissingResource Unfixable) - | MemVal { min_perm = Freeable; _ } -> Ok (rec_set_perm node) + DR.error (MissingResource Unfixable) + | MemVal { min_perm = Freeable; _ } -> DR.ok (rec_set_perm node) | MemVal { min_perm; _ } -> - Error + DR.error (InsufficientPermission { required = Freeable; actual = min_perm }) in let rebuild_parent = update_parent_perm in @@ -1145,7 +1148,7 @@ module M = struct [@@deriving show, yojson] type action = ac - type pred = ga + type pred = ga [@@deriving yojson] let action_to_str = str_ac let action_from_str s = try Some (ac_from_str s) with _ -> None @@ -1404,8 +1407,7 @@ module M = struct | None -> DR.error (MissingResource Unfixable) | Some src_root -> let** framed, _ = - Tree.frame_range src_root - ~replace_node:(fun x -> Ok x) + Tree.frame_range src_root ~replace_node:DR.ok ~rebuild_parent:(fun t ~left:_ ~right:_ -> Delayed.return t) src_range in @@ -1422,8 +1424,8 @@ module M = struct Tree.frame_range dst_root ~replace_node:(fun current -> match current.node with - | NotOwned _ -> Error (MissingResource Unfixable) - | _ -> Ok (Tree.realign framed dst_ofs)) + | NotOwned _ -> DR.error (MissingResource Unfixable) + | _ -> DR.ok (Tree.realign framed dst_ofs)) ~rebuild_parent:Tree.of_children dst_range in DR.of_result (with_root dst_tree new_dst_root) @@ -1482,7 +1484,7 @@ module M = struct List.fold_left (fun acc (tree_node : Tree.t) -> let** acc = acc in - let replace_node _ = Ok tree_node in + let replace_node _ = DR.ok tree_node in let rebuild_parent = Tree.of_children in let++ _, tree = Tree.frame_range acc ~replace_node ~rebuild_parent @@ -1596,7 +1598,7 @@ module M = struct ] ) -> let perm = ValueTranslation.permission_of_string perm_string in let chunk = ValueTranslation.chunk_of_string chunk_string in - let* sval = SVal.of_gil_expr_exn sval_e in + let* sval = SVal.of_gil_expr_vanish sval_e in prod_single s ofs chunk sval perm |> filter_errors | ( Array, [ @@ -1679,7 +1681,7 @@ module M = struct let fixes = match chunk with | Mptr -> - let new_var1 = Expr.LVar (LVar.alloc ()) in + let new_var1 = Expr.ALoc (ALoc.alloc ()) in let new_var2 = Expr.LVar (LVar.alloc ()) in let value = Expr.EList [ new_var1; new_var2 ] in let null_typ = @@ -1688,34 +1690,22 @@ module M = struct in let null_ptr = Expr.EList [ null_typ; Expr.int 0 ] in [ + [ (Single, [ ofs; chunk_as_expr ], [ value; freeable_perm ]) ]; [ - MyAsrt.CorePred - (Single, [ ofs; chunk_as_expr ], [ value; freeable_perm ]); - MyAsrt.Types - [ (new_var1, Type.ObjectType); (new_var2, Type.IntType) ]; - ]; - [ - MyAsrt.CorePred - (Single, [ ofs; chunk_as_expr ], [ null_ptr; freeable_perm ]); + (Single, [ ofs; chunk_as_expr ], [ null_ptr; freeable_perm ]); ]; ] | _ -> - let type_str, type_gil = + let type_str = match chunk with - | Chunk.Mfloat32 -> (single_type, Type.NumberType) - | Chunk.Mfloat64 -> (float_type, Type.NumberType) - | Chunk.Mint64 -> (long_type, Type.IntType) - | _ -> (int_type, Type.IntType) + | Chunk.Mfloat32 -> single_type + | Chunk.Mfloat64 -> float_type + | Chunk.Mint64 -> long_type + | _ -> int_type in let new_var = Expr.LVar (LVar.alloc ()) in let value = Expr.EList [ Expr.string type_str; new_var ] in - [ - [ - MyAsrt.CorePred - (Single, [ ofs; chunk_as_expr ], [ value; freeable_perm ]); - MyAsrt.Types [ (new_var, type_gil) ]; - ]; - ] + [ [ (Single, [ ofs; chunk_as_expr ], [ value; freeable_perm ]) ] ] in (* Additional fix for store operation to handle case of unitialized memory *) if is_store then @@ -1726,10 +1716,7 @@ module M = struct in let uninit = [ - [ - MyAsrt.CorePred - (Hole, [ ofs; offset_by_chunk ofs chunk ], [ freeable_perm ]); - ]; + [ (Hole, [ ofs; offset_by_chunk ofs chunk ], [ freeable_perm ]) ]; ] in uninit @ fixes diff --git a/transformers/lib/prebuilt/c_states/CGEnv.ml b/transformers/lib/prebuilt/c_states/CGEnv.ml index 44d53350..309e05ba 100644 --- a/transformers/lib/prebuilt/c_states/CGEnv.ml +++ b/transformers/lib/prebuilt/c_states/CGEnv.ml @@ -1,62 +1,40 @@ -open Gil_syntax +open Utils open Gillian.Monadic -module DR = Delayed_result +open Gil_syntax module Global_env = Cgil_lib.Global_env let init_data = ref Global_env.empty let set_init_data d = init_data := d -module M : States.MyMonadicSMemory.S with type t = Global_env.t = struct - type t = Global_env.t [@@deriving yojson] - type err_t = unit [@@deriving show, yojson] - type action = GetDef - type pred = unit - - let pp = Global_env.pp - - let action_from_str = function - | "getdef" -> Some GetDef - | _ -> None +module EnvAg = struct + include Agreement - let action_to_str GetDef = "getdef" - let pred_from_str _ = None - let pred_to_str () = failwith "No pred in GEnv" - let empty () = !init_data + let execute_action a ins s = + let open Delayed.Syntax in + let* res = execute_action a ins s in + match (a, res) with + | Load, Error e when can_fix e && !Gillian.Utils.Config.under_approximation + -> Delayed.vanish () + | _ -> Delayed.return res - (* Execute action *) - let execute_action GetDef s args = - match args with - | [ (Expr.Lit (Loc loc) | Expr.ALoc loc | Expr.LVar loc) ] -> ( - match Global_env.find_def_opt s loc with - | Some def -> - let v = Global_env.serialize_def def in - DR.ok (s, [ Expr.Lit (Loc loc); Expr.Lit v ]) - | None -> - (* If we can't find a function, in UX mode we give up, while in OX mode we - signal. *) - if !Gillian.Utils.Config.under_approximation then Delayed.vanish () - else - Fmt.failwith "execute_genvgetdef: couldn't find %s\nGENV:\n%a" loc - Global_env.pp s) - | _ -> failwith "Invalid arguments for GetDef" - - let consume () _ _ = failwith "Invalid C GEnv consume" - let produce () _ _ = failwith "Invalid C GEnv produce" - let compose _ _ = Delayed.vanish () (* TODO *) - let is_exclusively_owned _ _ = Delayed.return false - let is_empty _ = false - let is_concrete _ = false - let instantiate _ = (Global_env.empty, []) - - (* Core predicates: pred * ins * outs, converted to Asrt.CorePred *) + let get_fixes _ = [] let assertions _ = [] - let assertions_others _ = [] - let can_fix () = false - let get_fixes () = [] - let lvars _ = Gillian.Utils.Containers.SS.empty - let alocs _ = Gillian.Utils.Containers.SS.empty - let substitution_in_place _ s = Delayed.return s - let get_recovery_tactic _ = Gillian.General.Recovery_tactic.none - let list_actions () = [ (GetDef, [], []) ] - let list_preds () = [] end + +module M : MyMonadicSMemory = + Mapper + (struct + let action_substitutions = [ ("getdef", "load") ] + let pred_substitutions = [ ("def", "value") ] + end) + (struct + include OpenALocPMap (EnvAg) + + let empty () : t = + Cgil_lib.String_map.fold + (fun k v acc -> + States.MyUtils.SMap.add k + (Some (Expr.Lit (Global_env.serialize_def v))) + acc) + !init_data States.MyUtils.SMap.empty + end) diff --git a/transformers/lib/prebuilt/c_states/LActions.ml b/transformers/lib/prebuilt/c_states/LActions.ml index 1cb77ed5..7ebaf374 100644 --- a/transformers/lib/prebuilt/c_states/LActions.ml +++ b/transformers/lib/prebuilt/c_states/LActions.ml @@ -1,5 +1,5 @@ type ac = DropPerm | GetCurPerm | WeakValidPointer | Store | Load -type ga = Single | Array | Hole | Zeros | Bounds +type ga = Single | Array | Hole | Zeros | Bounds [@@deriving yojson] let str_ac = function | DropPerm -> "dropperm" diff --git a/transformers/lib/states/ActionAdder.ml b/transformers/lib/states/ActionAdder.ml index 91235673..8de5730b 100644 --- a/transformers/lib/states/ActionAdder.ml +++ b/transformers/lib/states/ActionAdder.ml @@ -14,7 +14,7 @@ module type ActionAddition = sig action -> t -> Expr.t list -> (t * Expr.t list, err_t) result Delayed.t val can_fix : err_t -> bool - val get_fixes : err_t -> string MyAsrt.t list list + val get_fixes : err_t -> string Fix.t list val get_recovery_tactic : err_t -> Expr.t Gillian.General.Recovery_tactic.t end @@ -65,9 +65,8 @@ struct | BaseErr e -> S.get_fixes e | AddedErr e -> A.get_fixes e - |> MyUtils.deep_map - @@ MyAsrt.map_cp (fun (p, i, o) -> - (S.pred_from_str p |> Option.get, i, o)) + |> MyUtils.deep_map @@ fun (p, i, o) -> + (S.pred_from_str p |> Option.get, i, o) let get_recovery_tactic = function | BaseErr e -> S.get_recovery_tactic e diff --git a/transformers/lib/states/Agreement.ml b/transformers/lib/states/Agreement.ml index 68233b48..3ca2c728 100644 --- a/transformers/lib/states/Agreement.ml +++ b/transformers/lib/states/Agreement.ml @@ -8,7 +8,7 @@ module Recovery_tactic = Gillian.General.Recovery_tactic type t = Expr.t option [@@deriving yojson] type err_t = MissingState [@@deriving show, yojson] type action = Load -type pred = Ag +type pred = Ag [@@deriving yojson] let pp = Fmt.(option ~none:(any "None") Expr.pp) @@ -103,5 +103,4 @@ let can_fix = function | MissingState -> true let get_fixes = function - | MissingState -> - [ [ MyAsrt.CorePred (Ag, [], [ LVar (Generators.fresh_svar ()) ]) ] ] + | MissingState -> [ [ (Ag, [], [ Expr.LVar (Generators.fresh_svar ()) ]) ] ] diff --git a/transformers/lib/states/Exclusive.ml b/transformers/lib/states/Exclusive.ml index 8bd28fff..3cbbced1 100644 --- a/transformers/lib/states/Exclusive.ml +++ b/transformers/lib/states/Exclusive.ml @@ -8,7 +8,7 @@ module Recovery_tactic = Gillian.General.Recovery_tactic type t = Expr.t option [@@deriving show, yojson] type err_t = MissingState [@@deriving show, yojson] type action = Load | Store -type pred = Ex +type pred = Ex [@@deriving yojson] let pp = Fmt.(option ~none:(any "None") Expr.pp) @@ -95,4 +95,4 @@ let get_recovery_tactic _ = Recovery_tactic.none let can_fix MissingState = true let get_fixes MissingState = - [ [ MyAsrt.CorePred (Ex, [], [ LVar (Generators.fresh_svar ()) ]) ] ] + [ [ (Ex, [], [ Expr.LVar (Generators.fresh_svar ()) ]) ] ] diff --git a/transformers/lib/states/Fix.ml b/transformers/lib/states/Fix.ml new file mode 100644 index 00000000..54a25da8 --- /dev/null +++ b/transformers/lib/states/Fix.ml @@ -0,0 +1,35 @@ +open Gillian.Gil_syntax + +type 'cp atom = 'cp * Expr.t list * Expr.t list [@@deriving yojson, show] +type 'cp t = 'cp atom list [@@deriving yojson, show] + +let lvars (fix : 'cp t) = + let open Gillian.Utils.Containers in + List.fold_left + (fun acc (_, ins, outs) -> + let acc = + List.fold_left (fun acc e -> SS.union acc (Expr.lvars e)) acc ins + in + List.fold_left (fun acc e -> SS.union acc (Expr.lvars e)) acc outs) + SS.empty fix + +let alocs (fix : 'cp t) = + let open Gillian.Utils.Containers in + List.fold_left + (fun acc (_, ins, outs) -> + let acc = + List.fold_left (fun acc e -> SS.union acc (Expr.alocs e)) acc ins + in + List.fold_left (fun acc e -> SS.union acc (Expr.alocs e)) acc outs) + SS.empty fix + +let subst (subst : Gillian.Symbolic.Subst.t) (fix : 'a t) : 'a t = + let le_subst = Gillian.Symbolic.Subst.subst_in_expr subst ~partial:true in + let subst_atom (cp, ins, outs) = + (cp, List.map le_subst ins, List.map le_subst outs) + in + List.map subst_atom fix + +let to_asrt ~pred_to_str fix : Asrt.t = + ListLabels.map fix ~f:(fun (cp, ins, outs) -> + Asrt.CorePred (pred_to_str cp, ins, outs)) diff --git a/transformers/lib/states/Fractional.ml b/transformers/lib/states/Fractional.ml index db0a02ae..43800a2f 100644 --- a/transformers/lib/states/Fractional.ml +++ b/transformers/lib/states/Fractional.ml @@ -13,7 +13,7 @@ type t = (Expr.t * Expr.t) option [@@deriving show, yojson] type err_t = MissingState | NotEnoughPermission [@@deriving show, yojson] type action = Load | Store -type pred = Frac +type pred = Frac [@@deriving yojson] let action_from_str = function | "load" -> Some Load diff --git a/transformers/lib/states/Freeable.ml b/transformers/lib/states/Freeable.ml index f6027b42..4ebcb153 100644 --- a/transformers/lib/states/Freeable.ml +++ b/transformers/lib/states/Freeable.ml @@ -38,7 +38,7 @@ module Make (S : MyMonadicSMemory.S) : (fun (a, arg, ret) -> (SubAction a, arg, ret)) (S.list_actions ()) - type pred = FreedPred | SubPred of S.pred + type pred = FreedPred | SubPred of S.pred [@@deriving yojson] let pred_from_str = function | "freed" -> Some FreedPred @@ -177,11 +177,11 @@ module Make (S : MyMonadicSMemory.S) : let get_fixes = function | SubError e -> - S.get_fixes e |> MyUtils.deep_map (MyAsrt.map_cp lift_corepred) + S.get_fixes e |> MyUtils.deep_map lift_corepred (* Fix can either be inner fix, or if empty the memory is freed! But Gillian C/WISL doesn't implement this so we comment it out to have comparable performance *) - (* @ [ [ MyAsrt.CorePred (FreedPred, [], []) ] ]*) - | MissingFreed -> [ [ MyAsrt.CorePred (FreedPred, [], []) ] ] + (* @ [ [ (FreedPred, [], []) ] ]*) + | MissingFreed -> [ [ (FreedPred, [], []) ] ] | _ -> failwith "Invalid fix call" end diff --git a/transformers/lib/states/MList.ml b/transformers/lib/states/MList.ml index d585ec23..b8041d10 100644 --- a/transformers/lib/states/MList.ml +++ b/transformers/lib/states/MList.ml @@ -37,7 +37,7 @@ module Make (S : MyMonadicSMemory.S) : (fun (a, args, ret) -> (SubAction a, "offset" :: args, ret)) (S.list_actions ()) - type pred = Length | SubPred of S.pred + type pred = Length | SubPred of S.pred [@@deriving yojson] let pred_from_str = function | "length" -> Some Length @@ -112,7 +112,9 @@ module Make (S : MyMonadicSMemory.S) : | Length, [ n' ] -> ( match n with | Some _ -> Delayed.vanish () - | None -> Delayed.return (b, Some n')) + | None -> + let+ () = Delayed.assume_types [ (n', Type.IntType) ] in + (b, Some n')) | Length, _ -> failwith "Invalid arguments for length produce" let compose s1 s2 = @@ -228,15 +230,9 @@ module Make (S : MyMonadicSMemory.S) : | OutOfBounds _ -> false let get_fixes = function - | SubError (idx, e) -> - S.get_fixes e |> MyUtils.deep_map (MyAsrt.map_cp (lift_corepred idx)) + | SubError (idx, e) -> S.get_fixes e |> MyUtils.deep_map (lift_corepred idx) | MissingLength -> let lvar = Expr.LVar (LVar.alloc ()) in - [ - [ - MyAsrt.CorePred (Length, [], [ lvar ]); - MyAsrt.Types [ (lvar, Type.IntType) ]; - ]; - ] + [ [ (Length, [], [ lvar ]) ] ] | _ -> failwith "Called get_fixes on unfixable error" end diff --git a/transformers/lib/states/MyAsrt.ml b/transformers/lib/states/MyAsrt.ml deleted file mode 100644 index 5524979e..00000000 --- a/transformers/lib/states/MyAsrt.ml +++ /dev/null @@ -1,20 +0,0 @@ -open Gil_syntax - -(* Similar to Gil_syntax.Asrt.t, but made to be simpler and nicer to use: - - typed core predicate names - - removed wands + predicates as using them from within a state model seems complicated+uneeded *) -type 'cp t = - | Emp (** Empty heap *) - | Pure of Expr.t (** Pure formula *) - | Types of (Expr.t * Type.t) list (** Typing assertion *) - | CorePred of 'cp * Expr.t list * Expr.t list (** Core predicate *) - -let map_cp - (f : 'cp1 * Expr.t list * Expr.t list -> 'cp2 * Expr.t list * Expr.t list) : - 'cp1 t -> 'cp2 t = function - | Emp -> Emp - | Pure f -> Pure f - | Types tys -> Types tys - | CorePred (cp, i, o) -> - let cp', i', o' = f (cp, i, o) in - CorePred (cp', i', o') diff --git a/transformers/lib/states/MyMonadicSMemory.ml b/transformers/lib/states/MyMonadicSMemory.ml index a4e48b0f..4745706b 100644 --- a/transformers/lib/states/MyMonadicSMemory.ml +++ b/transformers/lib/states/MyMonadicSMemory.ml @@ -14,7 +14,7 @@ module type S = sig (* Type of predicates and actions *) type action - type pred + type pred [@@deriving yojson] val action_from_str : string -> action option val action_to_str : action -> string @@ -66,7 +66,7 @@ module type S = sig (** Get the fixes for an error, as a list of fixes -- a fix is a list of core predicates to produce onto the state. *) - val get_fixes : err_t -> pred MyAsrt.t list list + val get_fixes : err_t -> pred Fix.t list (** The recovery tactic to attempt to resolve an error, by eg. unfolding predicates *) @@ -116,21 +116,21 @@ end callback, that is called whenever memory is initialised with some init data. *) module type ID = sig - type t + type t [@@deriving yojson] val init : t -> unit end module DummyID : ID with type t = unit = struct - type t = unit + type t = unit [@@deriving yojson] let init () = () end (** Functor to convert composable, typed state models into Gillian monadic state models *) -module Make (Mem : S) (ID : ID) : MonadicSMemory.S with type init_data = ID.t = -struct +module Make (Mem : S) (ID : ID) : + MonadicSMemory.S with type init_data = ID.t and type t = Mem.t = struct include Mem include Defaults @@ -174,14 +174,11 @@ struct let mapping (p, ins, outs) = Asrt.CorePred (pred_to_str p, ins, outs) in List.map mapping core_preds @ formulas - let get_fixes e = - get_fixes e - |> MyUtils.deep_map @@ function - | MyAsrt.Emp -> Asrt.Emp - | MyAsrt.Pure f -> Asrt.Pure f - | MyAsrt.Types ts -> Asrt.Types ts - | MyAsrt.CorePred (p, ins, outs) -> - Asrt.CorePred (pred_to_str p, ins, outs) + let get_fixes (e : err_t) = + let fixes = get_fixes e in + MyUtils.deep_map + (fun (p, ins, outs) -> Asrt.CorePred (pred_to_str p, ins, outs)) + fixes (* Override methods to keep implementations light *) let clear _ = empty () diff --git a/transformers/lib/states/PMap.ml b/transformers/lib/states/PMap.ml index 4a450a46..80a7100e 100644 --- a/transformers/lib/states/PMap.ml +++ b/transformers/lib/states/PMap.ml @@ -156,7 +156,7 @@ struct (fun (a, args, ret) -> (SubAction a, "index" :: args, ret)) (S.list_actions ()) - type pred = DomainSet | SubPred of S.pred + type pred = DomainSet | SubPred of S.pred [@@deriving yojson] let pred_from_str = function | "domainset" -> Some DomainSet @@ -287,6 +287,7 @@ struct match s with | _, Some _ -> Delayed.vanish () | h, None -> + let* () = Delayed.assume_types [ (d', Type.SetType) ] in (* This would be the correct implementation, but the handling of sets is bad so it creates all sorts of issues (eg. in matching plans)... let dom = ExpMap.bindings h |> List.map fst in @@ -389,18 +390,11 @@ struct | NotAllocated _ -> false let get_fixes = function - | SubError (idx, idx', e) -> - S.get_fixes e - |> MyUtils.deep_map @@ MyAsrt.map_cp @@ lift_corepred idx' - |> List.map @@ List.cons @@ MyAsrt.Pure Expr.Infix.(idx == idx') + | SubError (_idx, idx', e) -> + S.get_fixes e |> MyUtils.deep_map @@ lift_corepred idx' | MissingDomainSet -> let lvar = Expr.LVar (LVar.alloc ()) in - [ - [ - MyAsrt.CorePred (DomainSet, [], [ lvar ]); - MyAsrt.Types [ (lvar, Type.SetType) ]; - ]; - ] + [ [ (DomainSet, [], [ lvar ]) ] ] | _ -> failwith "Called get_fixes on unfixable error" end @@ -444,7 +438,7 @@ struct (fun (a, args, ret) -> (SubAction a, "index" :: args, ret)) (S.list_actions ()) - type pred = S.pred + type pred = S.pred [@@deriving yojson] let pred_from_str = S.pred_from_str let pred_to_str = S.pred_to_str @@ -552,10 +546,8 @@ struct | InvalidIndexValue _ -> false let get_fixes = function - | SubError (idx, idx', e) -> - S.get_fixes e - |> MyUtils.deep_map @@ MyAsrt.map_cp @@ lift_corepred idx' - |> List.map @@ List.cons @@ MyAsrt.Pure Expr.Infix.(idx == idx') + | SubError (_idx, idx', e) -> + S.get_fixes e |> MyUtils.deep_map @@ lift_corepred idx' | _ -> failwith "Called get_fixes on unfixable error" end diff --git a/transformers/lib/states/Product.ml b/transformers/lib/states/Product.ml index eca0bf7a..38d28610 100644 --- a/transformers/lib/states/Product.ml +++ b/transformers/lib/states/Product.ml @@ -27,7 +27,7 @@ module Make (IDs : IDs) (S1 : MyMonadicSMemory.S) (S2 : MyMonadicSMemory.S) : List.map (fun (a, args, ret) -> (A1 a, args, ret)) (S1.list_actions ()) @ List.map (fun (a, args, ret) -> (A2 a, args, ret)) (S2.list_actions ()) - type pred = P1 of S1.pred | P2 of S2.pred + type pred = P1 of S1.pred | P2 of S2.pred [@@deriving yojson] let pred_from_str s = match IDer.get_ided s with @@ -133,6 +133,6 @@ module Make (IDs : IDs) (S1 : MyMonadicSMemory.S) (S2 : MyMonadicSMemory.S) : | E2 e -> S2.can_fix e let get_fixes = function - | E1 e -> S1.get_fixes e |> MyUtils.deep_map (MyAsrt.map_cp lift_corepred_1) - | E2 e -> S2.get_fixes e |> MyUtils.deep_map (MyAsrt.map_cp lift_corepred_2) + | E1 e -> S1.get_fixes e |> MyUtils.deep_map lift_corepred_1 + | E2 e -> S2.get_fixes e |> MyUtils.deep_map lift_corepred_2 end diff --git a/transformers/lib/states/Sum.ml b/transformers/lib/states/Sum.ml index c0ce1112..d7a24983 100644 --- a/transformers/lib/states/Sum.ml +++ b/transformers/lib/states/Sum.ml @@ -27,7 +27,7 @@ module Make (IDs : IDs) (S1 : MyMonadicSMemory.S) (S2 : MyMonadicSMemory.S) : List.map (fun (a, args, ret) -> (A1 a, args, ret)) (S1.list_actions ()) @ List.map (fun (a, args, ret) -> (A2 a, args, ret)) (S2.list_actions ()) - type pred = P1 of S1.pred | P2 of S2.pred + type pred = P1 of S1.pred | P2 of S2.pred [@@deriving yojson] let pred_from_str s = match IDer.get_ided s with @@ -192,9 +192,7 @@ module Make (IDs : IDs) (S1 : MyMonadicSMemory.S) (S2 : MyMonadicSMemory.S) : let get_fixes e = match e with - | E1 e1 -> - S1.get_fixes e1 |> MyUtils.deep_map (MyAsrt.map_cp lift_corepred_1) - | E2 e2 -> - S2.get_fixes e2 |> MyUtils.deep_map (MyAsrt.map_cp lift_corepred_2) + | E1 e1 -> S1.get_fixes e1 |> MyUtils.deep_map lift_corepred_1 + | E2 e2 -> S2.get_fixes e2 |> MyUtils.deep_map lift_corepred_2 | _ -> failwith "get_fixes: invalid error" end diff --git a/transformers/lib/states/bi_abd.ml b/transformers/lib/states/bi_abd.ml new file mode 100644 index 00000000..e13e54e2 --- /dev/null +++ b/transformers/lib/states/bi_abd.ml @@ -0,0 +1,123 @@ +open Gillian.Monadic +module DR = Delayed_result + +type ('a, 'pred) bi_state = { state : 'a; anti_frame : 'pred Fix.t } +[@@deriving show, yojson] + +module Make (Mem : MyMonadicSMemory.S) : + MyMonadicSMemory.S with type t = (Mem.t, Mem.pred) bi_state = struct + type pred = Mem.pred [@@deriving yojson] + + let pred_from_str = Mem.pred_from_str + let pred_to_str = Mem.pred_to_str + let pp_pred = Fmt.of_to_string pred_to_str + let list_preds = Mem.list_preds + + type t = (Mem.t, pred) bi_state [@@deriving show, yojson] + type err_t = Mem.err_t [@@deriving show, yojson] + type action = Mem.action + + let action_from_str = Mem.action_from_str + let action_to_str = Mem.action_to_str + let list_actions = Mem.list_actions + let empty () : t = { state = Mem.empty (); anti_frame = [] } + + let with_bi_abduction ~f state args = + let open Delayed.Syntax in + let rec aux ~fuel state = + (* If fuel is exhausted we give up *) + let* () = if fuel <= 0 then Delayed.vanish () else Delayed.return () in + let* r = f state.state args in + match r with + | Ok (state', v) -> DR.ok ({ state with state = state' }, v) + | Error e when not (Mem.can_fix e) -> + (* can_fix is true when the error is a `miss` *) + DR.error e + | Error err -> + (* This is the missing error case *) + (* We take each fix one by one *) + let* cp_list = + let fixes = Mem.get_fixes err in + Logging.verbose (fun m -> + m "Attempting to fix %a with candidates: %a" Mem.pp_err_t err + (Fmt.Dump.list (Fix.pp (Fmt.of_to_string Mem.pred_to_str))) + fixes); + List.map Delayed.return fixes |> Delayed.branches + in + let* state' = + List.fold_left + (fun state (pred, ins, outs) -> + let* state = state in + Mem.produce pred state (ins @ outs)) + (Delayed.return state.state) + cp_list + in + let anti_frame = cp_list @ state.anti_frame in + (* We produce that fix in our current state *) + let new_state = { state = state'; anti_frame } in + aux ~fuel:(fuel - 1) new_state + in + (* We try to fix twice *) + aux ~fuel:2 state + + let execute_action action = with_bi_abduction ~f:(Mem.execute_action action) + + let produce pred { state; anti_frame } args = + let open Delayed.Syntax in + let+ state = Mem.produce pred state args in + { state; anti_frame } + + let consume pred state args = + with_bi_abduction ~f:(Mem.consume pred) state args + + let is_empty s = Mem.is_empty s.state + + (* Variables *) + + let lvars s = + let open Gillian.Utils.Containers in + Mem.lvars s.state |> SS.union (Fix.lvars s.anti_frame) + + let alocs s = + let open Gillian.Utils.Containers in + Mem.alocs s.state |> SS.union (Fix.alocs s.anti_frame) + + let substitution_in_place subst s = + let open Monadic.Delayed.Syntax in + let+ state = Mem.substitution_in_place subst s.state in + let anti_frame = Fix.subst subst s.anti_frame in + { state; anti_frame } + + (* Error handling *) + + let get_recovery_tactic = Mem.get_recovery_tactic + let can_fix e = Mem.can_fix e + + (* The rest of the functions remain unimplemented as Bi_abd makes no sense being an input to other transformers. *) + + let get_fixes _ = + failwith + "Bi_abd state should not be used as an input to the bi-abduction state \ + module. That one is legacy." + + let assertions_others _ = + failwith + "Should not be transforming bi-abd state to assertions, only its first \ + component" + + let assertions _ = + failwith + "Should not be transforming bi-abd state to assertions, only its first \ + component" + + let instantiate _ = + failwith "Bi_abd state should not be used as an input state" + + let is_exclusively_owned _ = + failwith "Bi_abd state should not be used as an input state" + + let is_concrete _ = + failwith "Bi_abd state should not be used as an input state" + + let compose _ _ = failwith "Bi_abd state should not be used as an input state" +end