diff --git a/.gitignore b/.gitignore index cf12abfaf..8d9a65762 100644 --- a/.gitignore +++ b/.gitignore @@ -87,4 +87,4 @@ see_deps.py javert-test262 # Temporary databases for logs -*.db \ No newline at end of file +*.db diff --git a/Gillian-C/bin/gillian_c.ml b/Gillian-C/bin/gillian_c.ml index c31f92d6c..e226e1ff6 100644 --- a/Gillian-C/bin/gillian_c.ml +++ b/Gillian-C/bin/gillian_c.ml @@ -7,5 +7,6 @@ module CLI = let runners : Gillian.Bulk.Runner.t list = [ (module CRunner); (module SRunner) ] end) + (Debugger.Gil_to_tl_lifter.Default (SMemory) (ParserAndCompiler)) let () = CLI.main () diff --git a/Gillian-JS/bin/dune b/Gillian-JS/bin/dune index 516c94886..cd5133ff1 100644 --- a/Gillian-JS/bin/dune +++ b/Gillian-JS/bin/dune @@ -2,7 +2,7 @@ (name gillian_js) (public_name gillian-js) (package gillian-js) - (libraries gillian js2jsil_lib semantics test262 cosetteRunner)) + (libraries gillian js2jsil_lib semantics test262 cosetteRunner debugging)) ; (executable ; (name test262) diff --git a/Gillian-JS/bin/gillian_js.ml b/Gillian-JS/bin/gillian_js.ml index 6fb739f2a..625ee4260 100644 --- a/Gillian-JS/bin/gillian_js.ml +++ b/Gillian-JS/bin/gillian_js.ml @@ -6,5 +6,6 @@ module CLI = let runners : Gillian.Bulk.Runner.t list = [ (module Test262.Test262_runner); (module CosetteRunner) ] end) + (Debugging.JSLifter) let () = CLI.main () diff --git a/Gillian-JS/lib/Debugging/JSLifter.ml b/Gillian-JS/lib/Debugging/JSLifter.ml new file mode 100644 index 000000000..181cb4f4f --- /dev/null +++ b/Gillian-JS/lib/Debugging/JSLifter.ml @@ -0,0 +1,288 @@ +open Gil_syntax +open Semantics +open Debugger.DebuggerTypes +include + Debugger.Gil_to_tl_lifter.Default + (Semantics.Symbolic) + (Js2jsil_lib.JS2GIL_ParserAndCompiler) + +let to_str pp = Fmt.to_to_string (Fmt.hbox pp) + +(* TODO: All of this node stuff should be refactored to hide the scope id *) +let create_node_var name nodes get_new_scope_id (variables : variables) = + let id = get_new_scope_id () in + let () = Hashtbl.replace variables id nodes in + (id, create_node_variable name id ()) + +let get_store_vars store = + store + |> List.map (fun (var, value) : variable -> + let value = Fmt.to_to_string (Fmt.hbox Expr.pp) value in + create_leaf_variable var value ()) + |> List.sort (fun v w -> Stdlib.compare v.name w.name) + +let add_properties_vars properties get_new_scope_id (variables : variables) = + let add_lst_vars name to_string lst get_new_scope_id (variables : variables) = + let list_nodes = + List.mapi + (fun index element -> + create_leaf_variable (string_of_int index) (to_string element) ()) + lst + in + let _, node = create_node_var name list_nodes get_new_scope_id variables in + node + in + let property_nodes = + properties |> Expr.Map.to_seq + |> Seq.map (fun (name, value) -> + let name = to_str Expr.pp name in + match value with + | Expr.EList lst -> + add_lst_vars name (to_str Expr.pp) lst get_new_scope_id variables + | Expr.Lit (Literal.LList lst) -> + add_lst_vars name (to_str Literal.pp) lst get_new_scope_id + variables + | _ -> create_leaf_variable name (to_str Expr.pp value) ()) + |> List.of_seq + in + let _, node = + create_node_var "properties" property_nodes get_new_scope_id variables + in + node + +let add_memory_vars smemory get_new_scope_id (variables : variables) = + let sorted_locs_with_vals = Symbolic.sorted_locs_with_vals smemory in + let value_nodes (loc, ((properties, domain), metadata)) : variable = + let () = ignore properties in + let properties = + add_properties_vars properties get_new_scope_id variables + in + let domain = + create_leaf_variable "domain" (to_str (Fmt.option Expr.pp) domain) () + in + let metadata = + create_leaf_variable "metadata" + (to_str (Fmt.option ~none:(Fmt.any "unknown") Expr.pp) metadata) + () + in + let loc_id = get_new_scope_id () in + let () = + Hashtbl.replace variables loc_id [ properties; domain; metadata ] + in + create_node_variable loc loc_id () + in + List.map value_nodes sorted_locs_with_vals + +let rec add_loc_vars + (loc : string) + smemory + get_new_scope_id + (variables : variables) + (loc_to_scope_id : (string, int) Hashtbl.t) : unit = + let rec add_lit_vars name lit : variable = + match lit with + | Literal.Loc loc -> + let () = + add_loc_vars loc smemory get_new_scope_id variables loc_to_scope_id + in + let id = Hashtbl.find loc_to_scope_id loc in + create_node_variable name id () + | LList lst -> + let nodes = + List.mapi + (fun index element -> + let name = string_of_int index in + add_lit_vars name element) + lst + in + let _, node = create_node_var name nodes get_new_scope_id variables in + node + | _ -> create_leaf_variable name (to_str Literal.pp lit) () + in + let add_expr_vars name expr = + match expr with + | Expr.ALoc loc -> + let () = + add_loc_vars loc smemory get_new_scope_id variables loc_to_scope_id + in + let id = Hashtbl.find loc_to_scope_id loc in + create_node_variable name id () + (* TODO: The below causes a stack overflow error in large pieces of + code, so they is probably a more efficient way to write this algorithm + or something else is just incorrect*) + (* | Expr.EList lst -> + let nodes = + List.mapi + (fun index element -> + let name = string_of_int index in + add_expr_vars name element) + lst + in + let _, node = create_node_var name nodes get_new_scope_id variables in + node + | Expr.Lit lit -> add_lit_vars name lit *) + | _ -> create_leaf_variable name (to_str Expr.pp expr) () + in + let add_properties_vars properties = + let property_nodes = + properties |> Expr.Map.to_seq + |> Seq.map (fun (name, value) -> + let name = to_str Expr.pp name in + let field_names = + [ + "descriptor_type"; + "value"; + "enumerable"; + "writable"; + "configurable"; + ] + in + match value with + | Expr.EList lst -> + let nodes = + if List.length lst == 5 then + (* TODO: Not sure if this is always the case *) + List.map2 + (fun name element -> add_expr_vars name element) + field_names lst + else + List.mapi + (fun index element -> + let name = string_of_int index in + add_expr_vars name element) + lst + in + let _, node = + create_node_var name nodes get_new_scope_id variables + in + node + | Expr.Lit (Literal.LList lst) -> + let nodes = + if List.length lst == 5 then + List.map2 + (fun name element -> add_lit_vars name element) + field_names lst + else + List.mapi + (fun index element -> + let name = string_of_int index in + add_lit_vars name element) + lst + in + + let _, node = + create_node_var name nodes get_new_scope_id variables + in + node + | _ -> add_expr_vars name value) + |> List.of_seq + in + let _, node = + create_node_var "properties" property_nodes get_new_scope_id variables + in + node + in + match Hashtbl.find_opt loc_to_scope_id loc with + | None -> + let loc_id = get_new_scope_id () in + let vars = + match SHeap.get smemory loc with + | None -> [] + | Some ((properties, domain), metadata_opt) -> + let metadata_node metadata_opt : variable = + let name = "metadata" in + match metadata_opt with + | None -> create_leaf_variable name "unknown" () + | Some metadata -> ( + match metadata with + | Expr.ALoc child_loc -> + let () = + add_loc_vars child_loc smemory get_new_scope_id + variables loc_to_scope_id + in + let id = Hashtbl.find loc_to_scope_id child_loc in + create_node_variable name id () + | _ -> create_leaf_variable name + (to_str Expr.pp metadata) ()) + in + let properties = add_properties_vars properties in + (* let properties = + add_properties_vars properties get_new_scope_id variables + in *) + let domain = + create_leaf_variable "domain" + (to_str (Fmt.option Expr.pp) domain) + () + in + [ properties; domain; metadata_node metadata_opt ] + in + + let () = Hashtbl.replace variables loc_id vars in + Hashtbl.replace loc_to_scope_id loc loc_id + | Some _ -> () + +let add_variables + ~store ~memory ~is_gil_file ~get_new_scope_id (variables : variables) = + if is_gil_file then + let store_id = get_new_scope_id () in + let memory_id = get_new_scope_id () in + let scopes : scope list = + [ { id = store_id; name = "Store" }; { id = memory_id; name = "Memory" } ] + in + let store_vars = get_store_vars store in + let memory_vars = add_memory_vars memory get_new_scope_id variables in + let vars = [ store_vars; memory_vars ] in + let () = + List.iter2 + (fun (scope : scope) vars -> Hashtbl.replace variables scope.id vars) + scopes vars + in + scopes + else + let sorted_locs_with_vals = Symbolic.sorted_locs_with_vals memory in + let loc_to_scope_id = Hashtbl.create 0 in + let () = + List.iter + (fun (loc, _) -> + add_loc_vars loc memory get_new_scope_id variables loc_to_scope_id) + sorted_locs_with_vals + in + (* TODO: probably better if we got a hash map of the store *) + let local_scope = + List.filter_map + (fun (var, value) -> + if var = Js2jsil_lib.JS2JSIL_Helpers.var_sc_first then + Some (var, value) + else None) + store + in + let local_scope_loc = + if List.length local_scope == 0 then "" + else + match List.hd local_scope with + | _, Expr.EList [ _; ALoc loc ] -> loc + | _ -> "" + in + let local_id : int = + match Hashtbl.find_opt loc_to_scope_id local_scope_loc with + | None -> + let local_id = get_new_scope_id () in + let () = Hashtbl.replace variables local_id [] in + local_id + | Some local_id -> local_id + in + let global_id : int = + match Hashtbl.find_opt loc_to_scope_id "$lg" with + | None -> + let global_id = get_new_scope_id () in + let () = Hashtbl.replace variables global_id [] in + global_id + | Some global_id -> global_id + in + let scopes : scope list = + [ + { id = local_id; name = "Local Scope" }; + { id = global_id; name = "Global Scope" }; + ] + in + scopes diff --git a/Gillian-JS/lib/Debugging/JSLifter.mli b/Gillian-JS/lib/Debugging/JSLifter.mli new file mode 100644 index 000000000..fd8de6509 --- /dev/null +++ b/Gillian-JS/lib/Debugging/JSLifter.mli @@ -0,0 +1,5 @@ +include + Gillian.Debugger.Gil_to_tl_lifter.S + with type memory = Semantics.Symbolic.t + and type memory_error = Semantics.Symbolic.err_t + and type tl_ast = Js2jsil_lib.JS2GIL_ParserAndCompiler.tl_ast diff --git a/Gillian-JS/lib/Debugging/dune b/Gillian-JS/lib/Debugging/dune new file mode 100644 index 000000000..2f1552404 --- /dev/null +++ b/Gillian-JS/lib/Debugging/dune @@ -0,0 +1,3 @@ +(library + (name debugging) + (libraries gillian semantics js2jsil_lib)) diff --git a/Gillian-JS/lib/Semantics/JSILSMemory.ml b/Gillian-JS/lib/Semantics/JSILSMemory.ml index 50fcaccd5..19008905e 100644 --- a/Gillian-JS/lib/Semantics/JSILSMemory.ml +++ b/Gillian-JS/lib/Semantics/JSILSMemory.ml @@ -10,7 +10,7 @@ module PFS = Gillian.Symbolic.PureContext module TypEnv = Gillian.Symbolic.TypEnv open Gillian.Logic -module M : Gillian.Symbolic.Memory_S = struct +module M = struct type vt = SVal.t [@@deriving yojson] (** Type of JSIL general states *) @@ -831,4 +831,8 @@ module M : Gillian.Symbolic.Memory_S = struct List.iter (fun f -> PFS.extend pfs f) new_pfs; mem | _ -> raise (Failure "Bi-abduction: cannot fix cell.")) + + let sorted_locs_with_vals (smemory : t) = + let sorted_locs = Containers.SS.elements (SHeap.domain smemory) in + List.map (fun loc -> (loc, Option.get (SHeap.get smemory loc))) sorted_locs end diff --git a/Gillian-JS/lib/Semantics/SFVL.mli b/Gillian-JS/lib/Semantics/SFVL.mli index a9dc3f052..5487405c9 100644 --- a/Gillian-JS/lib/Semantics/SFVL.mli +++ b/Gillian-JS/lib/Semantics/SFVL.mli @@ -2,12 +2,12 @@ * Interface for JSIL Symbolic FV-lists * *****************************************) -type t [@@deriving yojson] - type field_name = Gillian.Gil_syntax.Expr.t type field_value = Gillian.Gil_syntax.Expr.t +type t = field_value Gillian.Gil_syntax.Expr.Map.t [@@deriving yojson] + val add : field_name -> field_value -> t -> t val empty : t diff --git a/Gillian-JS/lib/Semantics/SHeap.ml b/Gillian-JS/lib/Semantics/SHeap.ml index 8c5f043e7..a79816435 100644 --- a/Gillian-JS/lib/Semantics/SHeap.ml +++ b/Gillian-JS/lib/Semantics/SHeap.ml @@ -14,8 +14,8 @@ type t = { sfvl : (string, SFVL.t) Hashtbl.t; sdom : (string, Expr.t option) Hashtbl.t; smet : (string, Expr.t option) Hashtbl.t; - cdmn : Var.Set.t ref; - sdmn : Var.Set.t ref; + cdmn : SS.t ref; + sdmn : SS.t ref; } [@@deriving yojson] diff --git a/Gillian-JS/lib/Semantics/dune b/Gillian-JS/lib/Semantics/dune index cf173375d..35f73311c 100644 --- a/Gillian-JS/lib/Semantics/dune +++ b/Gillian-JS/lib/Semantics/dune @@ -1,6 +1,6 @@ (library (name semantics) (libraries gillian jsil_syntax javert_utils js2jsil_lib str) - (flags :standard -open Utils -open Gillian.Utils -open Gillian.Utils.Prelude) (preprocess - (pps ppx_deriving_yojson))) + (pps ppx_deriving_yojson)) + (flags :standard -open Utils -open Gillian.Utils -open Utils.Prelude)) diff --git a/Gillian-JS/lib/Semantics/semantics.ml b/Gillian-JS/lib/Semantics/semantics.ml index 93d02afd5..562a596a1 100644 --- a/Gillian-JS/lib/Semantics/semantics.ml +++ b/Gillian-JS/lib/Semantics/semantics.ml @@ -1,3 +1,4 @@ module Symbolic = JSILSMemory.M module Concrete = JSILCMemory.M module External = External.M +module SHeap = SHeap diff --git a/GillianCore/CommandLine/CommandLine.ml b/GillianCore/CommandLine/CommandLine.ml index 119f2cdd5..3f1f51ba9 100644 --- a/GillianCore/CommandLine/CommandLine.ml +++ b/GillianCore/CommandLine/CommandLine.ml @@ -16,7 +16,11 @@ module Make (External : External.S) (PC : ParserAndCompiler.S) (Runners : sig val runners : Bulk.Runner.t list - end) = + end) + (Gil_to_tl_lifter : Debugger.Gil_to_tl_lifter.S + with type memory = SMemory.t + and type memory_error = SMemory.err_t + and type tl_ast = PC.tl_ast) = struct module CState = CState.Make (CMemory) module CInterpreter = @@ -28,6 +32,8 @@ struct PState.Make (SVal.M) (SVal.SESubst) (SStore) (SState) (Preds.SPreds) module Verification = Verifier.Make (SState) (SPState) (External) module Abductor = Abductor.Make (SState) (SPState) (External) + module Debugger = Debugger.Make (PC) (Verification) (Gil_to_tl_lifter) + module DebugAdapter = DebugAdapter.Make (Debugger) let files = let doc = "Input file." in @@ -62,18 +68,14 @@ struct in Arg.(value & opt c default & info [ "l"; "logging" ] ~docv:"SETTING" ~doc) - type reporter_info = { name : string; reporter : (module L.Reporter.S) } + type reporter_info = { name : string; reporter : L.Reporter.t } let reporters = let parse : string -> (reporter_info, [> `Msg of string ]) Result.t = function - | "file" -> Ok - { - name = "file"; - reporter = (module L.FileReporter); - } + | "file" -> Ok { name = "file"; reporter = L.file_reporter } | "database" | "db" -> - Ok { name = "database"; reporter = (module L.DatabaseReporter) } + Ok { name = "database"; reporter = L.database_reporter } | other -> Error (`Msg ("unknown value \"" ^ other ^ "\"")) in let print fmt (reporter_info : reporter_info) = @@ -81,12 +83,13 @@ struct in let c = Arg.(list & conv (parse, print)) in let default : reporter_info list = - [ { name = "file"; reporter = (module L.FileReporter) } ] + [ { name = "file"; reporter = L.file_reporter } ] in let doc = "Controls which reporters are used when logging. The value REPORTERS \ - must be a comma separated list of REPORTER values. A REPORTER value \ - must be one of `file`, `database`, `db`." + must be a comma separated list (with no spaces) of REPORTER values. A \ + REPORTER value must be one of `file`, `database`, `db` (short for \ + `database`)." in Arg.( value & opt c default & info [ "r"; "reporters" ] ~docv:"REPORTERS" ~doc) @@ -697,6 +700,27 @@ struct let bulk_cmds = List.map make_bulk_console Runners.runners end + module DebugVerificationConsole = struct + let debug_verify_info = + let doc = "Starts Gillian in debugging mode for verification" in + let man = + [ + `S Manpage.s_description; + `P + "Starts Gillian in debugging mode for verification, which \ + communicates via the Debug Adapter Protocol"; + ] + in + Term.info "debugverify" ~doc ~exits:Term.default_exits ~man + + let start_debug_adapter () = + Lwt_main.run (DebugAdapter.start Lwt_io.stdin Lwt_io.stdout) + + let debug_verify_t = with_common Term.(const start_debug_adapter) + + let debug_verify_cmd = (debug_verify_t, debug_verify_info) + end + let default_cmd = let doc = "An analysis toolchain" in let sdocs = Manpage.s_common_options in @@ -718,6 +742,7 @@ struct SInterpreterConsole.wpst_cmd; VerificationConsole.verify_cmd; ACTConsole.act_cmd; + DebugVerificationConsole.debug_verify_cmd; ] @ BulkConsole.bulk_cmds diff --git a/GillianCore/CommandLine/dune b/GillianCore/CommandLine/dune index e0a8160a3..caf8975bc 100644 --- a/GillianCore/CommandLine/dune +++ b/GillianCore/CommandLine/dune @@ -2,6 +2,6 @@ (name commandLine) (public_name gillian.commandLine) (libraries cmdliner fmt.tty gil_syntax utils engine bulk logging - incrementalAnalysis) + incrementalAnalysis debugAdapter) (flags :standard -open Gil_syntax -open Utils -open Engine -open Bulk -open IncrementalAnalysis)) diff --git a/GillianCore/GIL_Parser/GIL_Parser.mly b/GillianCore/GIL_Parser/GIL_Parser.mly index 7155173a1..eb6c2950e 100644 --- a/GillianCore/GIL_Parser/GIL_Parser.mly +++ b/GillianCore/GIL_Parser/GIL_Parser.mly @@ -1018,7 +1018,7 @@ lit_target: | TRUE { Bool true } | FALSE { Bool false } | FLOAT { Num $1 } - | n = INTEGER { Int n } + | n = INTEGER { Int n } | NAN { Num nan } | INFINITY { Num infinity } | STRING { String $1 } diff --git a/GillianCore/GIL_Syntax/Gil_syntax.mli b/GillianCore/GIL_Syntax/Gil_syntax.mli index 1dc02c352..226ee27c6 100644 --- a/GillianCore/GIL_Syntax/Gil_syntax.mli +++ b/GillianCore/GIL_Syntax/Gil_syntax.mli @@ -910,8 +910,11 @@ module Annot : sig (** Set the loop info *) val set_loop_info : t -> string list -> t - (** get the line offset *) + (** Get the origin location *) val get_origin_loc : t -> Location.t option + + (* Get the origin id *) + val get_origin_id : t -> int end module Proc : sig diff --git a/GillianCore/debugging/debugger/Gil_to_tl_lifter.ml b/GillianCore/debugging/debugger/Gil_to_tl_lifter.ml new file mode 100644 index 000000000..305f0d0f0 --- /dev/null +++ b/GillianCore/debugging/debugger/Gil_to_tl_lifter.ml @@ -0,0 +1,68 @@ +type ('err, 'ast) memory_error_info = { + error : 'err; (** The memory error that needs to be lifted *) + command : (int Cmd.t * Annot.t) option; (** The command where it happened *) + tl_ast : 'ast option; +} + +module type S = sig + type memory_error + + type tl_ast + + type memory + + val memory_error_to_exception_info : + (memory_error, tl_ast) memory_error_info -> DebuggerTypes.exception_info + + val add_variables : + store:(string * Expr.t) list -> + memory:memory -> + is_gil_file:bool -> + get_new_scope_id:(unit -> int) -> + DebuggerTypes.variables -> + DebuggerTypes.scope list +end + +module Default (SMemory : SMemory.S) (PC : ParserAndCompiler.S) : + S + with type memory = SMemory.t + and type tl_ast = PC.tl_ast + and type memory_error = SMemory.err_t = struct + type memory = SMemory.t + + type tl_ast = PC.tl_ast + + type memory_error = SMemory.err_t + + let memory_error_to_exception_info { error; _ } : DebuggerTypes.exception_info + = + { id = Fmt.to_to_string SMemory.pp_err error; description = None } + + let add_variables ~store ~memory ~is_gil_file ~get_new_scope_id variables : + DebuggerTypes.scope list = + let open DebuggerTypes in + let () = ignore is_gil_file in + let store_id = get_new_scope_id () in + let memory_id = get_new_scope_id () in + let scopes : scope list = + [ { id = store_id; name = "Store" }; { id = memory_id; name = "Memory" } ] + in + let store_vars = + store + |> List.map (fun (var, value) : variable -> + let value = Fmt.to_to_string (Fmt.hbox Expr.pp) value in + create_leaf_variable var value ()) + |> List.sort (fun (v : DebuggerTypes.variable) w -> + Stdlib.compare v.name w.name) + in + let memory_vars = + [ + create_leaf_variable "" + (Fmt.to_to_string (Fmt.hbox SMemory.pp) memory) + (); + ] + in + let () = Hashtbl.replace variables store_id store_vars in + let () = Hashtbl.replace variables memory_id memory_vars in + scopes +end diff --git a/GillianCore/debugging/debugger/Gil_to_tl_lifter.mli b/GillianCore/debugging/debugger/Gil_to_tl_lifter.mli new file mode 100644 index 000000000..8de78fe48 --- /dev/null +++ b/GillianCore/debugging/debugger/Gil_to_tl_lifter.mli @@ -0,0 +1,31 @@ +type ('err, 'ast) memory_error_info = { + error : 'err; (** The memory error that needs to be lifted *) + command : (int Cmd.t * Annot.t) option; (** The command where it happened *) + tl_ast : 'ast option; + (** If the program was compiled from the target language, we keep the tl ast around *) +} + +module type S = sig + type memory_error + + type tl_ast + + type memory + + val memory_error_to_exception_info : + (memory_error, tl_ast) memory_error_info -> DebuggerTypes.exception_info + + val add_variables : + store:(string * Expr.t) list -> + memory:memory -> + is_gil_file:bool -> + get_new_scope_id:(unit -> int) -> + DebuggerTypes.variables -> + DebuggerTypes.scope list +end + +module Default (SMemory : SMemory.S) (PC : ParserAndCompiler.S) : + S + with type memory = SMemory.t + and type tl_ast = PC.tl_ast + and type memory_error = SMemory.err_t diff --git a/GillianCore/debugging/debugger/debugger.ml b/GillianCore/debugging/debugger/debugger.ml index ecf058656..162391576 100644 --- a/GillianCore/debugging/debugger/debugger.ml +++ b/GillianCore/debugging/debugger/debugger.ml @@ -1,4 +1,7 @@ +module L = Logging +module Gil_to_tl_lifter = Gil_to_tl_lifter module DebuggerTypes = DebuggerTypes +module DebuggerUtils = DebuggerUtils open DebuggerTypes module type S = sig @@ -28,3 +31,468 @@ module type S = sig val set_breakpoints : string option -> int list -> debugger_state -> unit end + +module Make + (PC : ParserAndCompiler.S) + (Verification : Verifier.S) + (Lifter : Gil_to_tl_lifter.S + with type memory = Verification.SAInterpreter.heap_t + and type memory_error = Verification.SPState.m_err_t + and type tl_ast = PC.tl_ast) = +struct + open Verification.SAInterpreter + module Breakpoints = Set.Make (Int) + + type breakpoints = (string, Breakpoints.t) Hashtbl.t + + type tl_ast = PC.tl_ast + + type debugger_state = { + source_file : string; + source_files : SourceFiles.t option; + prog : (Annot.t, int) Prog.t; + tl_ast : tl_ast option; + mutable cont_func : + (unit -> Verification.SAInterpreter.result_t cont_func) option; + mutable breakpoints : breakpoints; + mutable cur_report_id : L.ReportId.t; + (* TODO: The below fields only depend on the + cur_report_id and could be refactored to use this *) + mutable top_level_scopes : scope list; + mutable frames : frame list; + mutable variables : variables; + mutable errors : err_t list; + mutable cur_cmd : (int Cmd.t * Annot.t) option; + } + + let top_level_scopes : scope list = + let top_level_scope_names = + (* [ "Store"; "Heap"; "Pure Formulae"; "Typing Environment"; "Predicates" ] *) + [ "Pure Formulae"; "Typing Environment"; "Predicates" ] + in + List.mapi (fun i name -> { name; id = i + 1 }) top_level_scope_names + + let is_gil_file file_name = Filename.check_suffix file_name "gil" + + let get_pure_formulae_vars (state : state_t) : variable list = + Verification.SPState.get_pfs state + |> PFS.to_list + |> List.map (fun formula -> + let value = Fmt.to_to_string (Fmt.hbox Formula.pp) formula in + { name = ""; value; type_ = None; var_ref = 0 }) + |> List.sort (fun v w -> Stdlib.compare v.value w.value) + + let get_typ_env_vars (state : state_t) : variable list = + let typ_env = Verification.SPState.get_typ_env state in + TypEnv.to_list typ_env + |> List.sort (fun (v, _) (w, _) -> Stdlib.compare v w) + |> List.map (fun (name, value) -> + let value = Type.str value in + { name; value; type_ = None; var_ref = 0 }) + |> List.sort (fun v w -> Stdlib.compare v.name w.name) + + let get_pred_vars (state : state_t) : variable list = + Verification.SPState.get_preds state + |> Preds.SPreds.to_list + |> List.map (fun pred -> + let value = Fmt.to_to_string (Fmt.hbox Preds.SPreds.pp_pabs) pred in + { name = ""; value; type_ = None; var_ref = 0 }) + |> List.sort (fun v w -> Stdlib.compare v.value w.value) + + let create_variables (state : state_t option) (is_gil_file : bool) : + scope list * variables = + let variables = Hashtbl.create 0 in + (* New scope ids must be higher than last top level scope id to prevent + duplicate scope ids *) + let scope_id = ref (List.length top_level_scopes) in + let get_new_scope_id () = + let () = scope_id := !scope_id + 1 in + !scope_id + in + let lifted_scopes = + match state with + | None -> [] + | Some state -> + let store = Verification.SPState.get_store state |> Store.bindings in + let memory = Verification.SPState.get_heap state in + let lifted_scopes = + Lifter.add_variables ~store ~memory ~is_gil_file ~get_new_scope_id + variables + in + let pure_formulae_vars = get_pure_formulae_vars state in + let typ_env_vars = get_typ_env_vars state in + let pred_vars = get_pred_vars state in + let vars_list = [ pure_formulae_vars; typ_env_vars; pred_vars ] in + let () = + List.iter2 + (fun (scope : scope) vars -> + Hashtbl.replace variables scope.id vars) + top_level_scopes vars_list + in + lifted_scopes + in + (lifted_scopes, variables) + + (* TODO: Find a common place to put the below three functions which are + duplicated in CommandLine.ml *) + let convert_other_imports oi = + List.map + (fun (ext, f) -> + let fun_with_exn s = Stdlib.Result.get_ok (f s) in + (ext, fun_with_exn)) + oi + + let get_progs_or_fail = function + | Ok progs -> ( + match progs.ParserAndCompiler.gil_progs with + | [] -> + Fmt.pr "Error: expected at least one GIL program\n"; + exit 1 + | _ -> progs) + | Error err -> + Fmt.pr "Error during compilation to GIL:\n%a" PC.pp_err err; + exit 1 + + let burn_gil prog outfile_opt = + match outfile_opt with + | Some outfile -> + let outc = open_out outfile in + let fmt = Format.formatter_of_out_channel outc in + let () = Prog.pp_labeled fmt prog in + close_out outc + | None -> () + + let preprocess_files files already_compiled outfile_opt no_unfold = + let e_prog, source_files_opt, tl_ast = + if not already_compiled then + let progs = get_progs_or_fail (PC.parse_and_compile_files files) in + let e_progs = progs.gil_progs in + let () = Gil_parsing.cache_labelled_progs (List.tl e_progs) in + let e_prog = snd (List.hd e_progs) in + let source_files = progs.source_files in + (e_prog, Some source_files, Some progs.tl_ast) + else + let e_prog = Gil_parsing.parse_eprog_from_file (List.hd files) in + (e_prog, None, None) + in + let () = burn_gil e_prog outfile_opt in + (* Prog.perform_syntax_checks e_prog; *) + let prog = + Gil_parsing.eprog_to_prog + ~other_imports:(convert_other_imports PC.other_imports) + e_prog + in + let () = + L.verbose (fun m -> + m "@\nProgram as parsed:@\n%a@\n" Prog.pp_indexed prog) + in + let prog = LogicPreprocessing.preprocess prog (not no_unfold) in + let () = + L.verbose (fun m -> + m "@\nProgram after logic preprocessing:@\n%a@\n" Prog.pp_indexed prog) + in + (prog, source_files_opt, tl_ast) + + let has_hit_breakpoint dbg = + match dbg.frames with + | [] -> false + | frame :: _ -> + if Hashtbl.mem dbg.breakpoints frame.source_path then + let breakpoints = Hashtbl.find dbg.breakpoints frame.source_path in + (* Currently only one breakpoint per line is supported *) + Breakpoints.mem frame.start_line breakpoints + else false + + let rec call_stack_to_frames call_stack next_proc_body_idx prog = + match call_stack with + | [] -> [] + | (se : CallStack.stack_element) :: rest -> + let defaults = (0, 0, 0, 0, "") in + let proc = Prog.get_proc prog se.pid in + let start_line, start_column, end_line, end_column, source_path = + match proc with + | None -> defaults + | Some proc -> ( + let annot, _, _ = proc.proc_body.(next_proc_body_idx) in + let loc_opt = Annot.get_origin_loc annot in + match loc_opt with + | None -> defaults + | Some loc -> + let loc = DebuggerUtils.location_to_display_location loc in + ( loc.loc_start.pos_line, + loc.loc_start.pos_column, + loc.loc_end.pos_line, + loc.loc_end.pos_column, + loc.loc_source )) + in + let frame = + { + (* TODO: make this a guaranteed unique index*) + index = se.call_index; + name = se.pid; + source_path; + start_line; + start_column; + end_line; + end_column; + } + in + frame :: call_stack_to_frames rest se.call_index prog + + let update_report_id_and_inspection_fields report_id dbg = + dbg.cur_report_id <- report_id; + match Logging.LogQueryer.get_report report_id with + | None -> + Fmt.failwith + "Unable to find report id '%a'. Check the logging level is set \ + correctly" + L.ReportId.pp report_id + | Some (content, type_) -> ( + match type_ with + | t when t = Logging.LoggingConstants.ContentType.cmd_step -> ( + let cmd_step = + content |> Yojson.Safe.from_string |> cmd_step_of_yojson + in + match cmd_step with + | Ok cmd_step -> + let () = + dbg.frames <- + call_stack_to_frames cmd_step.callstack + cmd_step.proc_body_index dbg.prog + in + let lifted_scopes, variables = + create_variables cmd_step.state (is_gil_file dbg.source_file) + in + let () = dbg.variables <- variables in + let () = + dbg.top_level_scopes <- + List.concat [ lifted_scopes; top_level_scopes ] + in + let () = dbg.errors <- cmd_step.errors in + let cur_cmd = + match cmd_step.callstack with + | [] -> None + | (se : CallStack.stack_element) :: _ -> ( + let proc = Prog.get_proc dbg.prog se.pid in + match proc with + | None -> None + | Some proc -> + let annot, _, cmd = + proc.proc_body.(cmd_step.proc_body_index) + in + Some (cmd, annot)) + in + dbg.cur_cmd <- cur_cmd + | Error err -> failwith err) + | _ as t -> + raise + (Failure + (Printf.sprintf + "Cannot deserialize: type '%s' does not match cmd_step" t))) + + let launch file_name proc_name = + let () = Fmt_tty.setup_std_outputs () in + let () = Config.current_exec_mode := Verification in + let () = PC.initialize Verification in + let () = Config.stats := false in + let () = Config.lemma_proof := true in + let () = Config.manual_proof := false in + let () = + match proc_name with + | None -> () + | Some proc_name -> Config.Verification.set_procs_to_verify [ proc_name ] + in + (* If the file is a GIL file, assume it is already compiled *) + let already_compiled = is_gil_file file_name in + let outfile_opt = None in + let no_unfold = false in + (* TODO: Support debugging incremental mode *) + (* let incremental = false in *) + let prog, source_files_opt, tl_ast = + preprocess_files [ file_name ] already_compiled outfile_opt no_unfold + in + let cont_func = Verification.verify_up_to_procs prog in + match cont_func with + | Verification.SAInterpreter.Finished _ -> Error "Nothing to run" + | Verification.SAInterpreter.Continue (cur_report_id, cont_func) -> ( + match cur_report_id with + | None -> + raise + (Failure + "Did not log report. Check the logging level is set correctly") + | Some cur_report_id -> + let dbg = + ({ + source_file = file_name; + source_files = source_files_opt; + top_level_scopes; + cont_func = Some cont_func; + prog; + tl_ast; + frames = []; + cur_report_id; + breakpoints = Hashtbl.create 0; + variables = Hashtbl.create 0; + errors = []; + cur_cmd = None; + } + : debugger_state) + in + let _ = update_report_id_and_inspection_fields cur_report_id dbg in + Ok dbg) + + let execute_step dbg = + let open Verification.SAInterpreter in + match dbg.cont_func with + | None -> ReachedEnd + | Some cont_func -> ( + let cont_func = cont_func () in + match cont_func with + | Finished _ -> + let () = dbg.cont_func <- None in + ReachedEnd + | Continue (cur_report_id, cont_func) -> ( + match cur_report_id with + | None -> + raise + (Failure + "Did not log report. Check the logging level is set \ + correctly") + | Some cur_report_id -> + let () = dbg.cont_func <- Some cont_func in + let () = + update_report_id_and_inspection_fields cur_report_id dbg + in + Step)) + + let step_in ?(reverse = false) dbg = + let stop_reason = + if reverse then + let prev_report_id = + Logging.LogQueryer.get_previous_report_id dbg.cur_report_id + in + match prev_report_id with + | None -> ReachedStart + | Some prev_report_id -> + let () = + update_report_id_and_inspection_fields prev_report_id dbg + in + Step + else + let next_report_id = + Logging.LogQueryer.get_next_report_id dbg.cur_report_id + in + match next_report_id with + | None -> execute_step dbg + | Some next_report_id -> + let () = + update_report_id_and_inspection_fields next_report_id dbg + in + Step + in + if has_hit_breakpoint dbg then Breakpoint + else if List.length dbg.errors > 0 then + let () = dbg.cont_func <- None in + ExecutionError + else stop_reason + + let rec step_until_cond + (prev_frame : frame) + (prev_stack_depth : int) + (cond : frame -> frame -> int -> int -> bool) + (dbg : debugger_state) : stop_reason = + let stop_reason = step_in dbg in + match stop_reason with + | Step -> ( + match dbg.frames with + | [] -> failwith "Nothing in call stack, cannot step" + | cur_frame :: _ -> + let cur_stack_depth = List.length dbg.frames in + if cond prev_frame cur_frame prev_stack_depth cur_stack_depth then + stop_reason + else step_until_cond prev_frame prev_stack_depth cond dbg) + | other_stop_reason -> other_stop_reason + + let step dbg = + match dbg.frames with + | [] -> failwith "Nothing in call stack, cannot step" + | frame :: _ -> + if is_gil_file dbg.source_file then + (* If GIL file, step until next cmd in the same frame (like in regular + debuggers) *) + step_until_cond frame (List.length dbg.frames) + (fun prev_frame cur_frame prev_stack_depth cur_stack_depth -> + cur_frame.source_path = prev_frame.source_path + && cur_frame.name = prev_frame.name + || cur_stack_depth < prev_stack_depth) + dbg + else + (* If target language file, step until the code origin location is + different, indicating an actual step in the target language*) + step_until_cond frame (List.length dbg.frames) + (fun prev_frame cur_frame _ _ -> + cur_frame.source_path = prev_frame.source_path + && (cur_frame.start_line <> prev_frame.start_line + || cur_frame.start_column <> prev_frame.start_column + || cur_frame.end_line <> prev_frame.end_line + || cur_frame.end_column <> prev_frame.end_column)) + dbg + + let step_out dbg = + let rec step_out stack_depth dbg = + let stop_reason = step_in dbg in + match stop_reason with + | Step -> + if List.length dbg.frames < stack_depth then stop_reason + else step_out stack_depth dbg + | other_stop_reason -> other_stop_reason + in + step_out (List.length dbg.frames) dbg + + let rec run ?(reverse = false) ?(launch = false) dbg = + (* We need to check if a breakpoint has been hit if run is called + immediately after launching to prevent missing a breakpoint on the first + line *) + if launch && has_hit_breakpoint dbg then Breakpoint + else + let stop_reason = step_in ~reverse dbg in + match stop_reason with + | Step -> run ~reverse dbg + | other_stop_reason -> other_stop_reason + + let terminate dbg = + let () = Verification.postprocess_files dbg.source_files in + let () = if !Config.stats then Statistics.print_statistics () in + Logging.wrap_up () + + let get_frames dbg = dbg.frames + + let get_scopes dbg = dbg.top_level_scopes + + let get_variables (var_ref : int) (dbg : debugger_state) : variable list = + match Hashtbl.find_opt dbg.variables var_ref with + | None -> [] + | Some vars -> vars + + let get_exception_info (dbg : debugger_state) = + let error = List.hd dbg.errors in + let non_mem_exception_info = + { id = Fmt.to_to_string pp_err error; description = None } + in + match error with + | ExecErr.ESt state_error -> ( + match state_error with + | StateErr.EMem merr -> + Lifter.memory_error_to_exception_info + { error = merr; command = dbg.cur_cmd; tl_ast = dbg.tl_ast } + | _ -> non_mem_exception_info) + | _ -> non_mem_exception_info + + let set_breakpoints source bp_list dbg = + match source with + (* We can't set the breakpoints if we do not know the source file *) + | None -> () + | Some source -> + let bp_set = Breakpoints.of_list bp_list in + Hashtbl.replace dbg.breakpoints source bp_set +end diff --git a/GillianCore/debugging/debugger/debugger.mli b/GillianCore/debugging/debugger/debugger.mli index ecf058656..d3f8aa1bb 100644 --- a/GillianCore/debugging/debugger/debugger.mli +++ b/GillianCore/debugging/debugger/debugger.mli @@ -1,4 +1,6 @@ module DebuggerTypes = DebuggerTypes +module DebuggerUtils = DebuggerUtils +module Gil_to_tl_lifter = Gil_to_tl_lifter open DebuggerTypes module type S = sig @@ -28,3 +30,11 @@ module type S = sig val set_breakpoints : string option -> int list -> debugger_state -> unit end + +module Make + (PC : ParserAndCompiler.S) + (Verification : Verifier.S) + (Lifter : Gil_to_tl_lifter.S + with type memory = Verification.SAInterpreter.heap_t + and type memory_error = Verification.SPState.m_err_t + and type tl_ast = PC.tl_ast) : S diff --git a/GillianCore/debugging/debugger/debuggerUtils.ml b/GillianCore/debugging/debugger/debuggerUtils.ml new file mode 100644 index 000000000..7cd55b589 --- /dev/null +++ b/GillianCore/debugging/debugger/debuggerUtils.ml @@ -0,0 +1,13 @@ +(* VSCode column numbers start from 1 while GIL location columns start from 0 *) +let location_to_display_location (loc : Location.t) : Location.t = + let loc_source = loc.loc_source in + let loc_start : Location.position = + { + pos_line = loc.loc_start.pos_line; + pos_column = loc.loc_start.pos_column + 1; + } + in + let loc_end : Location.position = + { pos_line = loc.loc_end.pos_line; pos_column = loc.loc_end.pos_column + 1 } + in + { loc_start; loc_end; loc_source } diff --git a/GillianCore/engine/Abstraction/PState.ml b/GillianCore/engine/Abstraction/PState.ml index bafa3dc8f..b3bc7555c 100644 --- a/GillianCore/engine/Abstraction/PState.ml +++ b/GillianCore/engine/Abstraction/PState.ml @@ -3,7 +3,7 @@ They are considered to be mutable. *) module type S = sig - include State.S + include SState.S type state_t @@ -36,7 +36,7 @@ module Make (Val : Val.S) (ESubst : ESubst.S with type vt = Val.t and type t = Val.et) (Store : Store.S with type vt = Val.t) - (State : State.S + (State : SState.S with type vt = Val.t and type st = ESubst.t and type store_t = Store.t) @@ -46,7 +46,9 @@ module Make and type st = ESubst.t and type store_t = Store.t and type state_t = State.t - and type preds_t = Preds.t = struct + and type preds_t = Preds.t + and type heap_t = State.heap_t + and type m_err_t = State.m_err_t = struct open Containers open Literal module L = Logging @@ -59,13 +61,15 @@ module Make type store_t = Store.t + type heap_t = State.heap_t + type abs_t = Preds.abs_t type state_t = State.t type preds_t = Preds.t - type err_t = State.err_t + type err_t = State.err_t [@@deriving yojson] type fix_t = State.fix_t @@ -1252,4 +1256,32 @@ module Make let get_equal_values astate = let state, _, _ = astate in State.get_equal_values state + + let get_heap pstate = + let state, _, _ = pstate in + State.get_heap state + + let get_typ_env pstate = + let state, _, _ = pstate in + State.get_typ_env state + + let get_pfs pstate = + let state, _, _ = pstate in + State.get_pfs state + + let of_yojson (yojson : Yojson.Safe.t) : (t, string) result = + (* TODO: Deserialize other components of pstate *) + match yojson with + | `Assoc [ ("state", state_yojson); ("preds", preds_yojson) ] -> + Result.bind (State.of_yojson state_yojson) (fun state -> + Preds.of_yojson preds_yojson + |> Result.map (fun (preds : Preds.t) : t -> + (state, preds, UP.init_pred_defs ()))) + | _ -> Error "Cannot parse yojson into PState" + + let to_yojson pstate = + (* TODO: Serialize other components of pstate *) + let state, preds, _ = pstate in + `Assoc + [ ("state", State.to_yojson state); ("preds", Preds.to_yojson preds) ] end diff --git a/GillianCore/engine/Abstraction/PState.mli b/GillianCore/engine/Abstraction/PState.mli index 370b40393..6d4927234 100644 --- a/GillianCore/engine/Abstraction/PState.mli +++ b/GillianCore/engine/Abstraction/PState.mli @@ -3,7 +3,7 @@ They are considered to be mutable. *) module type S = sig - include State.S + include SState.S type state_t @@ -36,7 +36,7 @@ module Make (Val : Val.S) (ESubst : ESubst.S with type vt = Val.t and type t = Val.et) (Store : Store.S with type vt = Val.t) - (State : State.S + (State : SState.S with type vt = Val.t and type st = ESubst.t and type store_t = Store.t) @@ -47,3 +47,5 @@ module Make and type store_t = Store.t and type state_t = State.t and type preds_t = Preds.t + and type heap_t = State.heap_t + and type m_err_t = State.m_err_t diff --git a/GillianCore/engine/Abstraction/Preds.ml b/GillianCore/engine/Abstraction/Preds.ml index 571a75c6e..384214575 100644 --- a/GillianCore/engine/Abstraction/Preds.ml +++ b/GillianCore/engine/Abstraction/Preds.ml @@ -1,12 +1,12 @@ module type S = sig (* value type *) - type vt + type vt [@@deriving yojson] (* substitution type for the value type *) type st (* preds *) - type t + type t [@@deriving yojson] type abs_t = string * vt list @@ -59,13 +59,13 @@ module Make S with type vt = Val.t and type st = ESubst.t = struct module L = Logging - type vt = Val.t + type vt = Val.t [@@deriving yojson] type st = ESubst.t type abs_t = string * vt list - type t = (string * vt list) list ref + type t = (string * vt list) list ref [@@deriving yojson] (** Returns the number of predicate assertions *) let length x = List.length !x diff --git a/GillianCore/engine/Abstraction/Preds.mli b/GillianCore/engine/Abstraction/Preds.mli index 288fcd2a2..40a710c6d 100644 --- a/GillianCore/engine/Abstraction/Preds.mli +++ b/GillianCore/engine/Abstraction/Preds.mli @@ -1,12 +1,12 @@ module type S = sig (* value type *) - type vt + type vt [@@deriving yojson] (* substitution type for the value type *) type st (* preds *) - type t + type t [@@deriving yojson] type abs_t = string * vt list diff --git a/GillianCore/engine/Abstraction/StateCleanUp.mli_ b/GillianCore/engine/Abstraction/StateCleanUp.mli_ deleted file mode 100644 index de0c23112..000000000 --- a/GillianCore/engine/Abstraction/StateCleanUp.mli_ +++ /dev/null @@ -1,13 +0,0 @@ -module type M = sig - type vt - - type st - - type store_t - - type error_t - - type state_t - - val exec : Prog.t -> state_t -> string -> bool -> state_t -end diff --git a/GillianCore/engine/Abstraction/Verifier.ml b/GillianCore/engine/Abstraction/Verifier.ml index 547384049..1e537c532 100644 --- a/GillianCore/engine/Abstraction/Verifier.ml +++ b/GillianCore/engine/Abstraction/Verifier.ml @@ -1,5 +1,48 @@ open Containers +module type S = sig + type st + + type heap_t + + type state + + type m_err + + module SPState : + PState.S + with type t = state + and type vt = SVal.M.t + and type st = st + and type store_t = SStore.t + and type heap_t = heap_t + and type m_err_t = m_err + and type preds_t = Preds.SPreds.t + + module SAInterpreter : + GInterpreter.S + with type vt = SVal.M.t + and type st = st + and type store_t = SStore.t + and type state_t = state + and type heap_t = heap_t + and type state_err_t = SPState.err_t + + type t + + val start_time : float ref + + val reset : unit -> unit + + val verify_prog : + (Annot.t, int) Prog.t -> bool -> SourceFiles.t option -> unit + + val verify_up_to_procs : + (Annot.t, int) Prog.t -> SAInterpreter.result_t SAInterpreter.cont_func + + val postprocess_files : SourceFiles.t option -> unit +end + module Make (SState : State.S with type vt = SVal.M.t @@ -17,6 +60,15 @@ struct module SAInterpreter = GInterpreter.Make (SVal.M) (SVal.SESubst) (SStore) (SPState) (External) module Normaliser = Normaliser.Make (SPState) + module SPState = SPState + + type st = SPState.st + + type state = SPState.t + + type heap_t = SPState.heap_t + + type m_err = SPState.m_err_t let print_success_or_failure success = if success then Fmt.pr "%a" (Fmt.styled `Green Fmt.string) "Success\n" @@ -450,18 +502,24 @@ struct print_success_or_failure success; success - let verify (prog : UP.prog) (test : t) : bool = - let state = test.pre_state in - + let verify_up_to_procs (prog : UP.prog) (test : t) : UP.prog = (* Printf.printf "Inside verify with a test for %s\n" test.name; *) match test.flag with - | Some flag -> + | Some _ -> let msg = "Verifying one spec of procedure " ^ test.name ^ "... " in L.tmi (fun fmt -> fmt "%s" msg); Fmt.pr "%s@?" msg; (* Reset coverage for every procedure in verification *) - let prog = { prog with coverage = Hashtbl.create 1 } in - (* TEST for procedure *) + { prog with coverage = Hashtbl.create 1 } + | None -> raise (Failure "Debugging lemmas unsupported!") + + let verify (prog : UP.prog) (test : t) : bool = + let state = test.pre_state in + + (* Printf.printf "Inside verify with a test for %s\n" test.name; *) + match test.flag with + | Some flag -> + let prog = verify_up_to_procs prog test in let rets = SAInterpreter.evaluate_proc (fun x -> x) @@ -571,11 +629,10 @@ struct ~printer:print_success_or_failure res cur_verified) prev_results - let verify_procs - ?(prev_results : VerificationResults.t option) + let get_tests_to_verify (prog : (Annot.t, int) Prog.t) (pnames_to_verify : SS.t) - (lnames_to_verify : SS.t) : unit = + (lnames_to_verify : SS.t) : UP.prog * t list * t list = let ipreds = UP.init_preds prog.preds in match ipreds with | Error e -> @@ -669,28 +726,71 @@ struct Hashtbl.iter (fun pred_name _ -> record_preds_used_by_pred pred_name prog') prog'.preds; + (prog', tests', tests)) - (* STEP 6: Run the symbolic tests *) - let cur_time = Sys.time () in - Fmt.pr "Running symbolic tests: %f\n@?" (cur_time -. !start_time); - let success : bool = - List.fold_left - (fun ac test -> if verify prog' test then ac else false) - true (tests' @ tests) - in - let end_time = Sys.time () in - let cur_verified = SS.union pnames_to_verify lnames_to_verify in - let success = - success && check_previously_verified prev_results cur_verified - in - let msg : string = - if success then "All specs succeeded:" else "There were failures:" - in - let msg : string = - Printf.sprintf "%s %f%!" msg (end_time -. !start_time) - in - Fmt.pr "%s\n@?" msg; - L.normal (fun m -> m "%s" msg)) + let verify_procs + ?(prev_results : VerificationResults.t option) + (prog : (Annot.t, int) Prog.t) + (pnames_to_verify : SS.t) + (lnames_to_verify : SS.t) : unit = + let prog', tests', tests = + get_tests_to_verify prog pnames_to_verify lnames_to_verify + in + (* STEP 6: Run the symbolic tests *) + let cur_time = Sys.time () in + Printf.printf "Running symbolic tests: %f\n" (cur_time -. !start_time); + let success : bool = + List.fold_left + (fun ac test -> if verify prog' test then ac else false) + true (tests' @ tests) + in + let end_time = Sys.time () in + let cur_verified = SS.union pnames_to_verify lnames_to_verify in + let success = + success && check_previously_verified prev_results cur_verified + in + let msg : string = + if success then "All specs succeeded:" else "There were failures:" + in + let msg : string = Printf.sprintf "%s %f%!" msg (end_time -. !start_time) in + Printf.printf "%s\n" msg; + L.normal (fun m -> m "%s" msg) + + let verify_up_to_procs (prog : (Annot.t, int) Prog.t) : + SAInterpreter.result_t SAInterpreter.cont_func = + L.with_normal_phase ~title:"Program verification" (fun () -> + (* Analyse all procedures and lemmas *) + let procs_to_verify = + SS.of_list (Prog.get_noninternal_proc_names prog) + in + let lemmas_to_verify = + SS.of_list (Prog.get_noninternal_lemma_names prog) + in + let procs_to_verify, lemmas_to_verify = + if !Config.Verification.verify_only_some_of_the_things then + ( SS.inter procs_to_verify + (SS.of_list !Config.Verification.procs_to_verify), + SS.inter lemmas_to_verify + (SS.of_list !Config.Verification.lemmas_to_verify) ) + else (procs_to_verify, lemmas_to_verify) + in + let prog, _, proc_tests = + get_tests_to_verify prog procs_to_verify lemmas_to_verify + in + (* TODO: Verify All procedures. Currently we only verify the first + procedure. Assume there is at least one procedure*) + let test = List.hd proc_tests in + SAInterpreter.init_evaluate_proc + (fun x -> x) + prog test.name test.params test.pre_state) + + let postprocess_files source_files = + let cur_source_files = + Option.value ~default:(SourceFiles.make ()) source_files + in + let call_graph = SAInterpreter.call_graph in + ResultsDir.write_verif_results cur_source_files call_graph ~diff:"" + global_results let verify_prog (prog : (Annot.t, int) Prog.t) diff --git a/GillianCore/engine/Abstraction/Verifier.mli b/GillianCore/engine/Abstraction/Verifier.mli new file mode 100644 index 000000000..6426dda12 --- /dev/null +++ b/GillianCore/engine/Abstraction/Verifier.mli @@ -0,0 +1,55 @@ +module type S = sig + type st + + type heap_t + + type state + + type m_err + + module SPState : + PState.S + with type t = state + and type vt = SVal.M.t + and type st = st + and type store_t = SStore.t + and type heap_t = heap_t + and type m_err_t = m_err + and type preds_t = Preds.SPreds.t + + module SAInterpreter : + GInterpreter.S + with type vt = SVal.M.t + and type st = st + and type store_t = SStore.t + and type state_t = state + and type heap_t = heap_t + and type state_err_t = SPState.err_t + + type t + + val start_time : float ref + + val reset : unit -> unit + + val verify_prog : + (Annot.t, int) Prog.t -> bool -> SourceFiles.t option -> unit + + val verify_up_to_procs : + (Annot.t, int) Prog.t -> SAInterpreter.result_t SAInterpreter.cont_func + + val postprocess_files : SourceFiles.t option -> unit +end + +module Make + (SState : State.S + with type vt = SVal.M.t + and type st = SVal.SESubst.t + and type store_t = SStore.t) + (SPState : PState.S + with type vt = SVal.M.t + and type st = SVal.SESubst.t + and type store_t = SStore.t + and type preds_t = Preds.SPreds.t) + (External : External.S) : + S with type heap_t = SPState.heap_t and type m_err = SPState.m_err_t diff --git a/GillianCore/engine/BiAbduction/BiState.ml b/GillianCore/engine/BiAbduction/BiState.ml index 546b20b91..e39df4430 100644 --- a/GillianCore/engine/BiAbduction/BiState.ml +++ b/GillianCore/engine/BiAbduction/BiState.ml @@ -6,7 +6,7 @@ module Make (Val : Val.S) (ESubst : ESubst.S with type vt = Val.t and type t = Val.et) (Store : Store.S with type vt = Val.t) - (State : State.S + (State : SState.S with type vt = Val.t and type st = ESubst.t and type store_t = Store.t) = @@ -20,11 +20,13 @@ struct type store_t = Store.t + type heap_t = State.heap_t + type state_t = State.t type t = SS.t * state_t * state_t - type err_t = State.err_t + type err_t = State.err_t [@@deriving yojson] type fix_t = State.fix_t @@ -609,4 +611,16 @@ struct let get_equal_values bi_state = let _, state, _ = bi_state in State.get_equal_values state + + let get_heap bi_state = + let _, state, _ = bi_state in + State.get_heap state + + let of_yojson _ = + failwith + "Please implement of_yojson to enable logging this type to a database" + + let to_yojson _ = + failwith + "Please implement to_yojson to enable logging this type to a database" end diff --git a/GillianCore/engine/BiAbduction/BiState.mli b/GillianCore/engine/BiAbduction/BiState.mli index 8ebfb290b..fc091c728 100644 --- a/GillianCore/engine/BiAbduction/BiState.mli +++ b/GillianCore/engine/BiAbduction/BiState.mli @@ -2,7 +2,7 @@ module Make (Val : Val.S) (ESubst : ESubst.S with type vt = Val.t and type t = Val.et) (Store : Store.S with type vt = Val.t) - (BaseState : State.S + (BaseState : SState.S with type vt = Val.t and type st = ESubst.t and type store_t = Store.t) : sig diff --git a/GillianCore/engine/ConcreteSemantics/CState.ml b/GillianCore/engine/ConcreteSemantics/CState.ml index 794b5f8fe..c11520b59 100644 --- a/GillianCore/engine/ConcreteSemantics/CState.ml +++ b/GillianCore/engine/ConcreteSemantics/CState.ml @@ -19,6 +19,8 @@ module Make type store_t = CStore.t + type heap_t = CMemory.t + type t = CMemory.t * CStore.t * vt list type fix_t @@ -246,4 +248,26 @@ module Make raise (Failure "Concrete: apply_fixes not implemented in CState.Make") let get_equal_values _ vs = vs + + let get_heap state = + let heap, _, _ = state in + heap + + let of_yojson _ = + failwith + "Please implement of_yojson to enable logging this type to a database" + + let to_yojson _ = + failwith + "Please implement to_yojson to enable logging this type to a database" + + let err_t_of_yojson _ = + failwith + "Please implement err_t_of_yojson to enable logging this type to a \ + database" + + let err_t_to_yojson _ = + failwith + "Please implement err_t_to_yojson to enable logging this type to a \ + database" end diff --git a/GillianCore/engine/FOLogic/FOSolver.ml b/GillianCore/engine/FOLogic/FOSolver.ml index b4a559b53..be9af2753 100644 --- a/GillianCore/engine/FOLogic/FOSolver.ml +++ b/GillianCore/engine/FOLogic/FOSolver.ml @@ -1,5 +1,4 @@ open SVal -open Containers module L = Logging (** **************** diff --git a/GillianCore/engine/FOLogic/PFS.ml b/GillianCore/engine/FOLogic/PFS.ml index 647397eb5..a3bb6eee9 100644 --- a/GillianCore/engine/FOLogic/PFS.ml +++ b/GillianCore/engine/FOLogic/PFS.ml @@ -1,10 +1,9 @@ (** GIL Pure Formulae *) -open Containers open SVal module L = Logging -type t = Formula.t ExtList.t +type t = Formula.t ExtList.t [@@deriving yojson] (**************************************) (** Pure formulae functions **) diff --git a/GillianCore/engine/FOLogic/PFS.mli b/GillianCore/engine/FOLogic/PFS.mli index 8f7a2a07a..b981e92fa 100644 --- a/GillianCore/engine/FOLogic/PFS.mli +++ b/GillianCore/engine/FOLogic/PFS.mli @@ -1,5 +1,5 @@ (** Type of Gillian pure formulae *) -type t +type t [@@deriving yojson] (** [init ()] returns a fresh empty collection of pure formulae *) val init : unit -> t diff --git a/GillianCore/engine/FOLogic/Simplifications.ml b/GillianCore/engine/FOLogic/Simplifications.ml index 63cbec58a..c53e7bfc8 100644 --- a/GillianCore/engine/FOLogic/Simplifications.ml +++ b/GillianCore/engine/FOLogic/Simplifications.ml @@ -1,6 +1,6 @@ -open Containers open SVal module L = Logging +module SB = Containers.SB type simpl_key_type = { kill_new_lvars : bool option; diff --git a/GillianCore/engine/GeneralSemantics/CallStack.ml b/GillianCore/engine/GeneralSemantics/CallStack.ml index 0349a1933..3759f9d8c 100644 --- a/GillianCore/engine/GeneralSemantics/CallStack.ml +++ b/GillianCore/engine/GeneralSemantics/CallStack.ml @@ -26,8 +26,9 @@ module type S = sig continue_index : int; error_index : int option; } + [@@deriving yojson] - type t = stack_element list + type t = stack_element list [@@deriving yojson] val empty : t @@ -90,13 +91,22 @@ module type S = sig @return The number of times the pid been recursively called *) val recursive_depth : t -> string -> int + + (** + Call stack pretty printer + + @param fmt Formatter + @param cs Call stack to pretty print + @return unit + *) + val pp : Format.formatter -> t -> unit end module Make (Val : Val.S) (Store : Store.S with type vt = Val.t) : S with type vt = Val.t and type store_t = Store.t = struct - type vt = Val.t + type vt = Val.t [@@deriving yojson] - type store_t = Store.t + type store_t = Store.t [@@deriving yojson] (** Type of call stacks: a call stack is a list of tuples, each of which contains 1) identifier of the current procedure (string) @@ -117,8 +127,9 @@ module Make (Val : Val.S) (Store : Store.S with type vt = Val.t) : continue_index : int; error_index : int option; } + [@@deriving yojson] - type t = stack_element list + type t = stack_element list [@@deriving yojson] let empty = [] @@ -201,4 +212,6 @@ module Make (Val : Val.S) (Store : Store.S with type vt = Val.t) : let get_cur_procs (cs : t) : string list = List.rev (List.fold_left (fun ac { pid; _ } -> pid :: ac) [] cs) + + let pp fmt cs = Fmt.(brackets (list ~sep:comma string)) fmt (get_cur_procs cs) end diff --git a/GillianCore/engine/GeneralSemantics/General/ExecErr.ml b/GillianCore/engine/GeneralSemantics/General/ExecErr.ml index 00da3a344..f4dfe0e0b 100644 --- a/GillianCore/engine/GeneralSemantics/General/ExecErr.ml +++ b/GillianCore/engine/GeneralSemantics/General/ExecErr.ml @@ -1,11 +1,15 @@ type ('value, 'state_err) t = - | EProc of 'value (** Incorrect procedure identifier *) - | ESt of 'state_err (** Memory Error *) + | EProc of 'value (** Incorrect procedure identifier *) + | ESt of 'state_err (** Memory Error *) | ECleanUp + | EFailReached of { fail_code : string; fail_params : 'value list } +[@@deriving yojson] let pp pp_val pp_state_err ft err = let open Fmt in match err with | EProc pid -> pf ft "@[EProc(%a)@]" pp_val pid - | ESt err -> (hbox pp_state_err) ft err - | ECleanUp -> string ft "ECleanUp()" + | ESt err -> (hbox pp_state_err) ft err + | ECleanUp -> string ft "ECleanUp()" + | EFailReached { fail_code; fail_params } -> + pf ft "@[EFailReached(%s, %a)@]" fail_code (list pp_val) fail_params diff --git a/GillianCore/engine/GeneralSemantics/General/GInterpreter.ml b/GillianCore/engine/GeneralSemantics/General/GInterpreter.ml index e78711d75..b199dd052 100644 --- a/GillianCore/engine/GeneralSemantics/General/GInterpreter.ml +++ b/GillianCore/engine/GeneralSemantics/General/GInterpreter.ml @@ -1,6 +1,100 @@ open Literal module L = Logging +module type S = sig + module CallStack : CallStack.S + + type vt + + type st + + type store_t + + type state_t + + type state_err_t + + type state_vt + + type heap_t + + module Val : Val.S with type t = vt + + module Store : Store.S with type t = store_t and type vt = vt + + type invariant_frames = (string * state_t) list + + type err_t = (vt, state_err_t) ExecErr.t [@@deriving yojson] + + type cconf_t = + | ConfErr of { + callstack : CallStack.t; + proc_idx : int; + error_state : state_t; + errors : err_t list; + } + | ConfCont of { + state : state_t; + callstack : CallStack.t; + invariant_frames : invariant_frames; + prev_idx : int; + next_idx : int; + loop_ids : string list; + branch_count : int; + } + | ConfFinish of { flag : Flag.t; ret_val : state_vt; final_state : state_t } + (** Equal to Conf cont + the id of the required spec *) + | ConfSusp of { + spec_id : string; + state : state_t; + callstack : CallStack.t; + invariant_frames : invariant_frames; + prev_idx : int; + next_idx : int; + loop_ids : string list; + branch_count : int; + } + + type conf_t = BConfErr of err_t list | BConfCont of state_t + + type result_t = (state_t, state_vt, err_t) ExecRes.t + + type 'a cont_func = + | Finished of 'a list + | Continue of (Logging.ReportId.t option * (unit -> 'a cont_func)) + + type cmd_step = { + callstack : CallStack.t; + proc_body_index : int; + state : state_t option; + errors : err_t list; + } + [@@deriving yojson] + + val pp_err : Format.formatter -> (vt, state_err_t) ExecErr.t -> unit + + val pp_result : Format.formatter -> result_t list -> unit + + val call_graph : CallGraph.t + + val reset : unit -> unit + + val evaluate_lcmds : UP.prog -> LCmd.t list -> state_t -> state_t list + + val init_evaluate_proc : + (result_t -> 'a) -> + UP.prog -> + string -> + string list -> + state_t -> + 'a cont_func + + val evaluate_proc : + (result_t -> 'a) -> UP.prog -> string -> string list -> state_t -> 'a list + + val evaluate_prog : UP.prog -> result_t list +end + (** General GIL Interpreter *) module Make (Val : Val.S) @@ -18,12 +112,27 @@ struct module CallStack = CallStack.Make (Val) (Store) module External = External (Val) (ESubst) (Store) (State) (CallStack) + module Val = Val + module State = State + module Store = Store + + type vt = Val.t + + type st = ESubst.t + + type store_t = Store.t - type state = State.t + type state_t = State.t [@@deriving yojson] - type invariant_frames = (string * state) list + type state_err_t = State.err_t - type err_t = (Val.t, State.err_t) ExecErr.t + type state_vt = State.vt + + type heap_t = State.heap_t + + type invariant_frames = (string * State.t) list + + type err_t = (Val.t, State.err_t) ExecErr.t [@@deriving yojson] let pp_err = ExecErr.pp Val.pp State.pp_err @@ -31,25 +140,53 @@ struct (** Type of configurations: state, call stack, previous index, previous loop ids, current index, branching *) type cconf_t = - | ConfErr of string * int * State.t * err_t list - | ConfCont of - State.t * CallStack.t * invariant_frames * int * string list * int * int - | ConfFinish of Flag.t * State.vt * State.t + | ConfErr of { + callstack : CallStack.t; + proc_idx : int; + error_state : state_t; + errors : err_t list; + } + | ConfCont of { + state : State.t; + callstack : CallStack.t; + invariant_frames : invariant_frames; + prev_idx : int; + next_idx : int; + loop_ids : string list; + branch_count : int; + } + | ConfFinish of { flag : Flag.t; ret_val : State.vt; final_state : State.t } (** Equal to Conf cont + the id of the required spec *) - | ConfSusp of - string - * State.t - * CallStack.t - * invariant_frames - * int - * string list - * int - * int + | ConfSusp of { + spec_id : string; + state : state_t; + callstack : CallStack.t; + invariant_frames : invariant_frames; + prev_idx : int; + next_idx : int; + loop_ids : string list; + branch_count : int; + } type conf_t = BConfErr of err_t list | BConfCont of State.t type result_t = (State.t, State.vt, err_t) ExecRes.t + type 'a cont_func = + | Finished of 'a list + | Continue of (Logging.ReportId.t option * (unit -> 'a cont_func)) + + type cmd_step = { + callstack : CallStack.t; + proc_body_index : int; + state : state_t option; + errors : err_t list; + } + [@@deriving yojson] + + type annotated_action = { annot : Annot.t; action_name : string } + [@@deriving yojson] + let max_branching = 100 exception Interpreter_error of err_t list * State.t @@ -186,6 +323,17 @@ struct (CallStack.get_loop_ids cs) b_counter state_printer state) + let cmd_step_pp fmt cmd_step = + (* TODO: Cmd step should contain all things in a configuration + print the same contents as print_configuration *) + CallStack.pp fmt cmd_step.callstack + + let annotated_action_pp fmt annotated_action = + let origin_loc = Annot.get_origin_loc annotated_action.annot in + Fmt.pf fmt "Executing action '%s' at %a" annotated_action.action_name + (Fmt.option ~none:(Fmt.any "none") Location.pp) + origin_loc + let print_lconfiguration (lcmd : LCmd.t) (state : State.t) : unit = L.normal (fun m -> m @@ -524,7 +672,16 @@ struct raise (Syntax_error msg) in - ConfCont (ret_state, new_cs, iframes, i, loop_ids, new_j, b_counter) + ConfCont + { + state = ret_state; + callstack = new_cs; + invariant_frames = iframes; + prev_idx = i; + loop_ids; + next_idx = new_j; + branch_count = b_counter; + } in let is_internal_proc proc_name = @@ -540,7 +697,18 @@ struct CallStack.push cs ~pid ~arguments:v_args ~store:old_store ~loop_ids ~ret_var:x ~call_index:i ~continue_index:(i + 1) ?error_index:j () in - [ ConfCont (state', cs', iframes, -1, loop_ids, 0, b_counter) ] + [ + ConfCont + { + state = state'; + callstack = cs'; + invariant_frames = iframes; + prev_idx = -1; + loop_ids; + next_idx = 0; + branch_count = b_counter; + }; + ] in let spec_exec_proc () = @@ -586,7 +754,16 @@ struct if Hashtbl.mem prog.prog.bi_specs pid then [ ConfSusp - (pid, state, cs, iframes, prev, prev_loop_ids, i, b_counter); + { + spec_id = pid; + state; + callstack = cs; + invariant_frames = iframes; + prev_idx = prev; + loop_ids = prev_loop_ids; + next_idx = i; + branch_count = b_counter; + }; ] else symb_exec_proc () in @@ -613,14 +790,43 @@ struct match cmd with (* Skip *) - | Skip -> [ ConfCont (state, cs, iframes, i, loop_ids, i + 1, b_counter) ] + | Skip -> + [ + ConfCont + { + state; + callstack = cs; + invariant_frames = iframes; + prev_idx = i; + loop_ids; + next_idx = i + 1; + branch_count = b_counter; + }; + ] (* Assignment *) | Assignment (x, e) -> let v = eval_expr e in let state' = update_store state x v in - [ ConfCont (state', cs, iframes, i, loop_ids, i + 1, b_counter) ] + [ + ConfCont + { + state = state'; + callstack = cs; + invariant_frames = iframes; + prev_idx = i; + loop_ids; + next_idx = i + 1; + branch_count = b_counter; + }; + ] (* Action *) | LAction (x, a, es) -> ( + let _ = + L.normal_specific + (L.Loggable.make annotated_action_pp annotated_action_of_yojson + annotated_action_to_yojson { annot; action_name = a }) + L.LoggingConstants.ContentType.annotated_action + in let v_es = List.map eval_expr es in match State.execute_action a state v_es with | ASucc [] -> @@ -636,13 +842,15 @@ struct let r_v = eval_expr r_e in let r_state' = update_store r_state x r_v in ConfCont - ( r_state', - CallStack.copy cs, - iframes, - i, - loop_ids, - i + 1, - b_counter )) + { + state = r_state'; + callstack = CallStack.copy cs; + invariant_frames = iframes; + prev_idx = i; + loop_ids; + next_idx = i + 1; + branch_count = b_counter; + }) rest_rets in let ret_len = 1 + List.length rest_rets in @@ -663,7 +871,15 @@ struct | _ -> [ ConfCont - (state'', cs, iframes, i, loop_ids, i + 1, b_counter); + { + state = state''; + callstack = cs; + invariant_frames = iframes; + prev_idx = i; + loop_ids; + next_idx = i + 1; + branch_count = b_counter; + }; ]) | false, true -> ( (* Can split into two threads *) @@ -674,11 +890,28 @@ struct | 0 -> [ ConfCont - (state'', cs, iframes, i, loop_ids, i + 1, b_counter); + { + state = state''; + callstack = cs; + invariant_frames = iframes; + prev_idx = i; + loop_ids; + next_idx = i + 1; + branch_count = b_counter; + }; ] | _ -> rest_confs) | _ -> - ConfCont (state'', cs, iframes, i, loop_ids, i + 1, b_counter) + ConfCont + { + state = state''; + callstack = cs; + invariant_frames = iframes; + prev_idx = i; + loop_ids; + next_idx = i + 1; + branch_count = b_counter; + } :: rest_confs) | AFail errs -> if not (ExecMode.concrete_exec !Config.current_exec_mode) then ( @@ -703,22 +936,40 @@ struct List.map (fun state -> ConfCont - (state, cs, iframes, prev, prev_loop_ids, i, b_counter)) + { + state; + callstack = cs; + invariant_frames = iframes; + prev_idx = prev; + loop_ids = prev_loop_ids; + next_idx = i; + branch_count = b_counter; + }) recovery_states | _ -> L.normal ~title:"failure" ~severity:Error (fun m -> m "Action call failed with:@.%a" (Fmt.Dump.list State.pp_err) errs); - raise - (Fmt.failwith "Local Action Failed: %a" Cmd.pp_indexed cmd)) + raise (State.Internal_State_Error (errs, state))) else Fmt.failwith "Local Action Failed: %a" Cmd.pp_indexed cmd) (* Logic command *) | Logic lcmd -> ( match lcmd with | SL SymbExec -> symb_exec_next := true; - [ ConfCont (state, cs, iframes, i, loop_ids, i + 1, b_counter) ] + [ + ConfCont + { + state; + callstack = cs; + invariant_frames = iframes; + prev_idx = i; + loop_ids; + next_idx = i + 1; + branch_count = b_counter; + }; + ] (* Invariant being revisited *) | SL (Invariant (a, binders)) when prev_loop_ids = loop_ids -> (* let () = Fmt.pr "\nRe-establishing invariant... @?" in *) @@ -736,7 +987,16 @@ struct List.map (fun (frame, state) -> let iframes = (List.hd loop_ids, frame) :: iframes in - ConfCont (state, cs, iframes, i, loop_ids, i + 1, b_counter)) + ConfCont + { + state; + callstack = cs; + invariant_frames = iframes; + prev_idx = i; + loop_ids; + next_idx = i + 1; + branch_count = b_counter; + }) frames_and_states | _ -> let resulting_states : State.t list = @@ -748,10 +1008,31 @@ struct in List.map (fun state -> - ConfCont (state, cs, iframes, i, loop_ids, i + 1, b_counter)) + ConfCont + { + state; + callstack = cs; + invariant_frames = iframes; + prev_idx = i; + loop_ids; + next_idx = i + 1; + branch_count = b_counter; + }) resulting_states) (* Unconditional goto *) - | Goto j -> [ ConfCont (state, cs, iframes, i, loop_ids, j, b_counter) ] + | Goto j -> + [ + ConfCont + { + state; + callstack = cs; + invariant_frames = iframes; + prev_idx = i; + loop_ids; + next_idx = j; + branch_count = b_counter; + }; + ] (* Conditional goto *) | GuardedGoto (e, j, k) -> ( let vt = eval_expr e in @@ -810,13 +1091,15 @@ struct List.mapi (fun j (state, next) -> ConfCont - ( state, - (if j = 0 then cs else CallStack.copy cs), - iframes, - i, - loop_ids, - next, - b_counter )) + { + state; + callstack = (if j = 0 then cs else CallStack.copy cs); + invariant_frames = iframes; + prev_idx = i; + loop_ids; + next_idx = next; + branch_count = b_counter; + }) sp in match @@ -840,7 +1123,18 @@ struct update_store state x v) state lxarr in - [ ConfCont (state', cs, iframes, i, loop_ids, i + 1, b_counter) ] + [ + ConfCont + { + state = state'; + callstack = cs; + invariant_frames = iframes; + prev_idx = i; + loop_ids; + next_idx = i + 1; + branch_count = b_counter; + }; + ] (* Function call *) | Call (x, e, args, j, subst) -> let pid = eval_expr e in @@ -861,7 +1155,16 @@ struct let v_args = List.map eval_expr args in List.map (fun (state, cs, i, j) -> - ConfCont (state, cs, iframes, i, loop_ids, j, b_counter)) + ConfCont + { + state; + callstack = cs; + invariant_frames = iframes; + prev_idx = i; + loop_ids; + next_idx = j; + branch_count = b_counter; + }) (External.execute prog.prog state cs i x pid v_args j) (* Function application *) | Apply (x, pid_args, j) -> ( @@ -882,7 +1185,18 @@ struct let args = CallStack.get_cur_args cs in let args = Val.from_list args in let state' = update_store state x args in - [ ConfCont (state', cs, iframes, i, loop_ids, i + 1, b_counter) ] + [ + ConfCont + { + state = state'; + callstack = cs; + invariant_frames = iframes; + prev_idx = i; + loop_ids; + next_idx = i + 1; + branch_count = b_counter; + }; + ] (* Normal-mode return *) | ReturnNormal -> let v_ret = Store.get store Names.return_variable in @@ -891,8 +1205,15 @@ struct | None, _ -> raise (Failure "nm_ret_var not in store (normal return)") | Some v_ret, { store = None; loop_ids = start_loop_ids; _ } :: _ -> check_loop_ids loop_ids start_loop_ids; - Fmt.pr "n @?"; - [ ConfFinish (Normal, v_ret, state) ] + (* TODO: Redirect stdout to a file in debugging mode, as + the debug adapter communicates with VSCode via stdout. This + particular print statement currently causes issues, but + should be re-added once stdout has been redirected. *) + (* Fmt.pr "n @?"; *) + [ + ConfFinish + { flag = Normal; ret_val = v_ret; final_state = state }; + ] | ( Some v_ret, { store = Some old_store; @@ -915,7 +1236,15 @@ struct let state' = State.set_store state old_store in let state'' = update_store state' x v_ret in ConfCont - (state'', cs', iframes, prev', start_loop_ids, j, b_counter) + { + state = state''; + callstack = cs'; + invariant_frames = iframes; + prev_idx = prev'; + loop_ids = start_loop_ids; + next_idx = j; + branch_count = b_counter; + } | _ -> raise (Failure "Malformed callstack") in L.verbose (fun m -> m "Returning."); @@ -929,7 +1258,9 @@ struct | Some v_ret, { store = None; loop_ids = start_loop_ids; _ } :: _ -> check_loop_ids loop_ids start_loop_ids; Fmt.pr "e @?"; - [ ConfFinish (Error, v_ret, state) ] + [ + ConfFinish { flag = Error; ret_val = v_ret; final_state = state }; + ] | ( Some v_ret, { store = Some old_store; @@ -951,14 +1282,22 @@ struct in let state' = State.set_store state old_store in let state'' = update_store state' x v_ret in - ConfCont (state'', cs', iframes, prev', start_loop_ids, j, b_counter) + ConfCont + { + state = state''; + callstack = cs'; + invariant_frames = iframes; + prev_idx = prev'; + loop_ids = start_loop_ids; + next_idx = j; + branch_count = b_counter; + } | _ -> raise (Failure "Malformed callstack")) (* Explicit failure *) - | Fail (fname, exprs) -> - let message = - Fmt.(str "Fail : %s%a" fname (parens (list ~sep:comma Expr.pp)) exprs) - in - raise (Failure message) + | Fail (fail_code, fail_params) -> + let fail_params = List.map (State.eval_expr state) fail_params in + let err = ExecErr.EFailReached { fail_code; fail_params } in + raise (Interpreter_error ([ err ], state)) let simplify state = snd (State.simplify ~save:true ~kill_new_lvars:true state) @@ -982,38 +1321,70 @@ struct try evaluate_cmd prog state cs iframes prev prev_loop_ids i b_counter with - | Interpreter_error (errs, state) -> - let proc = CallStack.get_cur_proc_id cs in - [ ConfErr (proc, i, state, errs) ] - | State.Internal_State_Error (errs, state) -> + | Interpreter_error (errors, error_state) -> + [ ConfErr { callstack = cs; proc_idx = i; error_state; errors } ] + | State.Internal_State_Error (errs, error_state) -> (* Return: current procedure name, current command index, the state, and the associated errors *) - let proc = CallStack.get_cur_proc_id cs in - [ ConfErr (proc, i, state, List.map (fun x -> ExecErr.ESt x) errs) ]) + [ + ConfErr + { + callstack = cs; + proc_idx = i; + error_state; + errors = List.map (fun x -> ExecErr.ESt x) errs; + }; + ]) states (** - Iterative evaluation of commands + Evaluates one step of a program + @param ret_fun Function to transform the results @param prog GIL program - @param confs Current configurations - @param results Current evaluation outcomes - @return List of final configurations -*) - let rec evaluate_cmd_iter + @param name Identifier of the procedure to be evaluated + @param params Parameters of the procedure to be evaluated + @state state Current state + @preds preds Current predicate set + @return Continuation function specifying the next step of evaluation + *) + let rec evaluate_cmd_step (ret_fun : result_t -> 'a) (retry : bool) (prog : UP.prog) (hold_results : 'a list) (on_hold : (cconf_t * string) list) (confs : cconf_t list) - (results : result_t list) : 'a list = - let f = evaluate_cmd_iter ret_fun retry prog hold_results on_hold in + (results : result_t list) : 'a cont_func = + let f = evaluate_cmd_step ret_fun retry prog hold_results on_hold in + + let continue_or_pause rest_confs cont_func = + match rest_confs with + | ConfCont { state; callstack; next_idx = proc_body_index; _ } :: _ -> + let report_id = + L.normal_specific + (L.Loggable.make cmd_step_pp cmd_step_of_yojson cmd_step_to_yojson + { callstack; proc_body_index; state = Some state; errors = [] }) + L.LoggingConstants.ContentType.cmd_step + in + Continue (report_id, fun () -> L.with_normal_phase cont_func) + | ConfErr + { callstack; proc_idx = proc_body_index; error_state = state; errors } + :: _ -> + let report_id = + L.normal_specific + (L.Loggable.make cmd_step_pp cmd_step_of_yojson cmd_step_to_yojson + { callstack; proc_body_index; state = Some state; errors }) + L.LoggingConstants.ContentType.cmd_step + in + Continue (report_id, fun () -> L.with_normal_phase cont_func) + | _ -> cont_func () + in match confs with | [] -> let results = List.map ret_fun results in let results = hold_results @ results in - if not retry then results + if not retry then Finished results else ( L.(verbose (fun m -> m "Relaunching suspended confs")); let hold_confs = @@ -1022,16 +1393,29 @@ struct if Hashtbl.mem prog.specs pid then Some conf else None) on_hold in - evaluate_cmd_iter ret_fun false prog results [] hold_confs []) - | ConfCont (state, cs, iframes, prev, prev_loop_ids, i, b_counter) + continue_or_pause hold_confs (fun () -> + evaluate_cmd_step ret_fun false prog results [] hold_confs [])) + | ConfCont + { + state; + callstack = cs; + invariant_frames = iframes; + prev_idx = prev; + loop_ids = prev_loop_ids; + next_idx = i; + branch_count = b_counter; + } :: rest_confs when b_counter < max_branching -> let next_confs = protected_evaluate_cmd prog state cs iframes prev prev_loop_ids i b_counter in - f (next_confs @ rest_confs) results - | ConfCont (state, cs, _, _, _, i, b_counter) :: rest_confs -> + continue_or_pause (next_confs @ rest_confs) (fun () -> + f (next_confs @ rest_confs) results) + | ConfCont + { state; callstack = cs; next_idx = i; branch_count = b_counter; _ } + :: rest_confs -> let _, annot_cmd = get_cmd prog cs i in Printf.printf "WARNING: MAX BRANCHING STOP: %d.\n" b_counter; L.( @@ -1041,42 +1425,80 @@ struct STOPPING CONF:\n" b_counter)); print_configuration annot_cmd state cs i b_counter; - f rest_confs results - | ConfErr (proc, i, state, errs) :: rest_confs -> - let result = ExecRes.RFail (proc, i, state, errs) in - f rest_confs (result :: results) - | ConfFinish (fl, v, state) :: rest_confs -> + continue_or_pause rest_confs (fun () -> f rest_confs results) + | ConfErr { callstack; proc_idx; error_state; errors } :: rest_confs -> + let proc = CallStack.get_cur_proc_id callstack in + let result = ExecRes.RFail (proc, proc_idx, error_state, errors) in + continue_or_pause rest_confs (fun () -> + f rest_confs (result :: results)) + | ConfFinish { flag = fl; ret_val = v; final_state = state } :: rest_confs + -> let result = ExecRes.RSucc (fl, v, state) in - f rest_confs (result :: results) - | ConfSusp (fid, state, cs, iframes, prev, prev_loop_ids, i, b_counter) + continue_or_pause rest_confs (fun () -> + f rest_confs (result :: results)) + | ConfSusp + { + spec_id = fid; + state; + callstack; + invariant_frames; + prev_idx; + loop_ids; + next_idx; + branch_count; + } :: rest_confs when retry -> let conf = - ConfCont (state, cs, iframes, prev, prev_loop_ids, i, b_counter) + ConfCont + { + state; + callstack; + invariant_frames; + prev_idx; + loop_ids; + next_idx; + branch_count; + } in L.( verbose (fun m -> m "Suspending a computation that was trying to call %s" fid)); - evaluate_cmd_iter ret_fun retry prog hold_results - ((conf, fid) :: on_hold) rest_confs results - | _ :: rest_confs -> f rest_confs results + continue_or_pause rest_confs (fun () -> + evaluate_cmd_step ret_fun retry prog hold_results + ((conf, fid) :: on_hold) rest_confs results) + | _ :: rest_confs -> + continue_or_pause rest_confs (fun () -> f rest_confs results) (** - Evaluation of procedures + Evaluates commands iteratively + + @param init_func The initial continuation function which evaluates the first + step of the program +*) + let rec evaluate_cmd_iter (init_func : 'a cont_func) : 'a list = + match init_func with + | Finished results -> results + | Continue (_, cont_func) -> evaluate_cmd_iter (cont_func ()) + + (** + Sets the initial values for evaluating a program, and returns a continuation + function which evaluates the first step of the program + @param ret_fun Function to transform the results @param prog GIL program @param name Identifier of the procedure to be evaluated @param params Parameters of the procedure to be evaluated @state state Current state @preds preds Current predicate set - @return List of final configurations -*) - let evaluate_proc + @return Continuation function which evaluates the first step of the program + *) + let init_evaluate_proc (ret_fun : result_t -> 'a) (prog : UP.prog) (name : string) (params : string list) - (state : State.t) : 'a list = + (state : State.t) : 'a cont_func = let () = CallGraph.add_proc call_graph name in L.normal (fun m -> m @@ -1095,14 +1517,52 @@ struct raise (Failure "Symbolic State does NOT contain formal parameter")) params in - let cs : CallStack.t = CallStack.push CallStack.empty ~pid:name ~arguments ~loop_ids:[] ~ret_var:"out" ~call_index:(-1) ~continue_index:(-1) ~error_index:(-1) () in - let conf : cconf_t = ConfCont (state, cs, [], -1, [], 0, 0) in - evaluate_cmd_iter ret_fun true prog [] [] [ conf ] [] + let proc_body_index = 0 in + let conf : cconf_t = + ConfCont + { + state; + callstack = cs; + invariant_frames = []; + prev_idx = -1; + loop_ids = []; + next_idx = proc_body_index; + branch_count = 0; + } + in + let report_id = + L.normal_specific + (L.Loggable.make cmd_step_pp cmd_step_of_yojson cmd_step_to_yojson + { callstack = cs; proc_body_index; state = Some state; errors = [] }) + L.LoggingConstants.ContentType.cmd_step + in + Continue + ( report_id, + fun () -> evaluate_cmd_step ret_fun true prog [] [] [ conf ] [] ) + + (** + Evaluation of procedures + + @param prog GIL program + @param name Identifier of the procedure to be evaluated + @param params Parameters of the procedure to be evaluated + @state state Current state + @preds preds Current predicate set + @return List of final configurations +*) + let evaluate_proc + (ret_fun : result_t -> 'a) + (prog : UP.prog) + (name : string) + (params : string list) + (state : State.t) : 'a list = + let init_func = init_evaluate_proc ret_fun prog name params state in + evaluate_cmd_iter init_func (** Evaluation of programs @@ -1118,10 +1578,38 @@ struct ~ret_var:"out" ~call_index:(-1) ~continue_index:(-1) ~error_index:(-1) () in + let initial_proc_body_index = 0 in + let initial_state = State.init (Some prog.preds) in let initial_conf = - ConfCont (State.init (Some prog.preds), initial_cs, [], -1, [], 0, 0) + ConfCont + { + state = initial_state; + callstack = initial_cs; + invariant_frames = []; + prev_idx = -1; + loop_ids = []; + next_idx = initial_proc_body_index; + branch_count = 0; + } + in + let report_id = + L.normal_specific + (L.Loggable.make cmd_step_pp cmd_step_of_yojson cmd_step_to_yojson + { + callstack = initial_cs; + proc_body_index = initial_proc_body_index; + state = Some initial_state; + errors = []; + }) + L.LoggingConstants.ContentType.cmd_step + in + let init_func = + Continue + ( report_id, + fun () -> + evaluate_cmd_step ret_fun true prog [] [] [ initial_conf ] [] ) in - evaluate_cmd_iter ret_fun true prog [] [] [ initial_conf ] [] + evaluate_cmd_iter init_func (** Configuration pretty-printer *) let pp_result (ft : Format.formatter) (reslt : result_t list) : unit = diff --git a/GillianCore/engine/GeneralSemantics/General/GInterpreter.mli b/GillianCore/engine/GeneralSemantics/General/GInterpreter.mli new file mode 100644 index 000000000..5990d90a4 --- /dev/null +++ b/GillianCore/engine/GeneralSemantics/General/GInterpreter.mli @@ -0,0 +1,112 @@ +module type S = sig + module CallStack : CallStack.S + + type vt + + type st + + type store_t + + type state_t + + type state_err_t + + type state_vt + + type heap_t + + module Val : Val.S with type t = vt + + module Store : Store.S with type t = store_t and type vt = vt + + type invariant_frames = (string * state_t) list + + type err_t = (vt, state_err_t) ExecErr.t [@@deriving yojson] + + type cconf_t = + | ConfErr of { + callstack : CallStack.t; + proc_idx : int; + error_state : state_t; + errors : err_t list; + } + | ConfCont of { + state : state_t; + callstack : CallStack.t; + invariant_frames : invariant_frames; + prev_idx : int; + next_idx : int; + loop_ids : string list; + branch_count : int; + } + | ConfFinish of { flag : Flag.t; ret_val : state_vt; final_state : state_t } + (** Equal to Conf cont + the id of the required spec *) + | ConfSusp of { + spec_id : string; + state : state_t; + callstack : CallStack.t; + invariant_frames : invariant_frames; + prev_idx : int; + next_idx : int; + loop_ids : string list; + branch_count : int; + } + + type conf_t = BConfErr of err_t list | BConfCont of state_t + + type result_t = (state_t, state_vt, err_t) ExecRes.t + + type 'a cont_func = + | Finished of 'a list + | Continue of (Logging.ReportId.t option * (unit -> 'a cont_func)) + + type cmd_step = { + callstack : CallStack.t; + proc_body_index : int; + state : state_t option; + errors : err_t list; + } + [@@deriving yojson] + + val pp_err : Format.formatter -> (vt, state_err_t) ExecErr.t -> unit + + val pp_result : Format.formatter -> result_t list -> unit + + val call_graph : CallGraph.t + + val reset : unit -> unit + + val evaluate_lcmds : UP.prog -> LCmd.t list -> state_t -> state_t list + + val init_evaluate_proc : + (result_t -> 'a) -> + UP.prog -> + string -> + string list -> + state_t -> + 'a cont_func + + val evaluate_proc : + (result_t -> 'a) -> UP.prog -> string -> string list -> state_t -> 'a list + + val evaluate_prog : UP.prog -> result_t list +end + +(** General GIL Interpreter *) +module Make + (Val : Val.S) + (ESubst : ESubst.S with type vt = Val.t and type t = Val.et) + (Store : Store.S with type vt = Val.t) + (State : State.S + with type vt = Val.t + and type st = ESubst.t + and type store_t = Store.t) + (External : External.S) : + S + with type vt = Val.t + and type st = ESubst.t + and type store_t = Store.t + and type state_t = State.t + and type state_err_t = State.err_t + and type state_vt = State.vt + and type heap_t = State.heap_t diff --git a/GillianCore/engine/GeneralSemantics/State.ml b/GillianCore/engine/GeneralSemantics/State.ml index 7cf702902..a63643da0 100644 --- a/GillianCore/engine/GeneralSemantics/State.ml +++ b/GillianCore/engine/GeneralSemantics/State.ml @@ -8,7 +8,7 @@ module type S = sig type vt (** Type of GIL general states *) - type t + type t [@@deriving yojson] (** Type of GIL substitutions *) type st @@ -16,10 +16,12 @@ module type S = sig (** Type of GIL stores *) type store_t + type heap_t + (** Errors *) type m_err_t - type err_t = (m_err_t, vt) StateErr.err_t + type err_t = (m_err_t, vt) StateErr.err_t [@@deriving yojson] type fix_t @@ -184,4 +186,6 @@ module type S = sig val apply_fixes : t -> fix_t list -> t option * Asrt.t list val get_equal_values : t -> vt list -> vt list + + val get_heap : t -> heap_t end diff --git a/GillianCore/engine/GeneralSemantics/StateErr.ml b/GillianCore/engine/GeneralSemantics/StateErr.ml index 192ae91c7..01d526660 100644 --- a/GillianCore/engine/GeneralSemantics/StateErr.ml +++ b/GillianCore/engine/GeneralSemantics/StateErr.ml @@ -5,6 +5,7 @@ type ('mem_err, 'value) err_t = | EPure of Formula.t (* Missing formula that should be true *) | EVar of Var.t (* Undefined variable *) | EAsrt of ('value list * Formula.t * Asrt.t list list) +[@@deriving yojson] let get_recovery_vals (errs : ('a, 'b) err_t list) (mem_recovery_vals : 'a -> 'b list) : 'b list = diff --git a/GillianCore/engine/SymbolicSemantics/SMemory.ml b/GillianCore/engine/SymbolicSemantics/SMemory.ml index 361ecc628..88d3299d5 100644 --- a/GillianCore/engine/SymbolicSemantics/SMemory.ml +++ b/GillianCore/engine/SymbolicSemantics/SMemory.ml @@ -9,10 +9,10 @@ module type S = sig type c_fix_t - type err_t + type err_t [@@deriving yojson] (** Type of GIL general states *) - type t + type t [@@deriving yojson] type action_ret = | ASucc of (t * vt list * Formula.t list * (string * Type.t) list) list diff --git a/GillianCore/engine/SymbolicSemantics/SState.ml b/GillianCore/engine/SymbolicSemantics/SState.ml index c5f7291be..f6c898850 100644 --- a/GillianCore/engine/SymbolicSemantics/SState.ml +++ b/GillianCore/engine/SymbolicSemantics/SState.ml @@ -1,25 +1,34 @@ open Literal -open Containers open Names module L = Logging module SSubst = SVal.SESubst +module type S = sig + include State.S + + val get_typ_env : t -> TypEnv.t + + val get_pfs : t -> PFS.t +end + module Make (SMemory : SMemory.S) : - State.S + S with type st = SVal.SESubst.t and type vt = SVal.M.t - and type store_t = SStore.t = struct - type vt = SVal.M.t + and type store_t = SStore.t + and type heap_t = SMemory.t + and type m_err_t = SMemory.err_t = struct + type vt = SVal.M.t [@@deriving yojson] type st = SVal.M.et - type heap_t = SMemory.t + type heap_t = SMemory.t [@@deriving yojson] - type store_t = SStore.t + type store_t = SStore.t [@@deriving yojson] - type m_err_t = SMemory.err_t + type m_err_t = SMemory.err_t [@@deriving yojson] - type t = heap_t * store_t * PFS.t * TypEnv.t * SS.t + type t = heap_t * store_t * PFS.t * TypEnv.t * SS.t [@@deriving yojson] type fix_t = | MFix of SMemory.c_fix_t @@ -27,7 +36,7 @@ module Make (SMemory : SMemory.S) : | FSVars of SS.t | FAsrt of Asrt.t - type err_t = (m_err_t, vt) StateErr.err_t + type err_t = (m_err_t, vt) StateErr.err_t [@@deriving yojson] type action_ret = ASucc of (t * vt list) list | AFail of err_t list @@ -831,4 +840,16 @@ module Make (SMemory : SMemory.S) : let get_equal_values state les = let _, _, pfs, _, _ = state in les @ List.concat_map (Reduction.get_equal_expressions pfs) les + + let get_heap state = + let heap, _, _, _, _ = state in + heap + + let get_typ_env state = + let _, _, _, typ_env, _ = state in + typ_env + + let get_pfs state = + let _, _, pfs, _, _ = state in + pfs end diff --git a/GillianCore/engine/SymbolicSemantics/SState.mli b/GillianCore/engine/SymbolicSemantics/SState.mli index e234f521c..ca65cb575 100644 --- a/GillianCore/engine/SymbolicSemantics/SState.mli +++ b/GillianCore/engine/SymbolicSemantics/SState.mli @@ -1,5 +1,15 @@ +module type S = sig + include State.S + + val get_typ_env : t -> TypEnv.t + + val get_pfs : t -> PFS.t +end + module Make (SMemory : SMemory.S) : - State.S + S with type st = SVal.SESubst.t and type vt = SVal.M.t and type store_t = SStore.t + and type heap_t = SMemory.t + and type m_err_t = SMemory.err_t diff --git a/GillianCore/engine/dune b/GillianCore/engine/dune index 847f7d6f7..8a51c5a2d 100644 --- a/GillianCore/engine/dune +++ b/GillianCore/engine/dune @@ -7,5 +7,5 @@ logging incrementalAnalysis) (preprocess (pps ppx_deriving.std ppx_deriving_yojson)) - (flags :standard -open Utils -open Gil_syntax -open IncrementalAnalysis - -open Utils.Prelude)) + (flags :standard -open Utils -open Gil_syntax -open Utils.Prelude -open + IncrementalAnalysis)) diff --git a/GillianCore/lib/dune b/GillianCore/lib/dune index 9e984a425..b00e9e3c6 100644 --- a/GillianCore/lib/dune +++ b/GillianCore/lib/dune @@ -11,4 +11,5 @@ ;gillian_bulk_rely logging incrementalAnalysis - monadic)) + monadic + debugger)) diff --git a/GillianCore/lib/gillian.ml b/GillianCore/lib/gillian.ml index e2d71fe69..2df436331 100644 --- a/GillianCore/lib/gillian.ml +++ b/GillianCore/lib/gillian.ml @@ -6,6 +6,7 @@ module Concrete = Engine.Concrete module General = Engine.General module Bulk = Bulk module Monadic = Monadic +module Debugger = Debugger module Logic = struct module Reduction = Engine.Reduction diff --git a/GillianCore/logging/logDatabase.ml b/GillianCore/logging/logDatabase.ml index a3d67eb95..df2cfa9db 100644 --- a/GillianCore/logging/logDatabase.ml +++ b/GillianCore/logging/logDatabase.ml @@ -30,7 +30,7 @@ let exec db ~log ~stmt = let zero_or_one_row db ~log ~stmt = match Sqlite3.step stmt with | ROW -> ( - let row = Sqlite3.row_blobs stmt in + let row = Sqlite3.row_data stmt in match Sqlite3.step stmt with | DONE -> Some row | ROW -> error "%s: expected zero or one row, got more than one row" log @@ -95,10 +95,15 @@ let get_report id = let stmt = Sqlite3.prepare db "SELECT content, type FROM report WHERE id=?;" in - Sqlite3.bind stmt 1 (Sqlite3.Data.TEXT id) + Sqlite3.bind stmt 1 (Sqlite3.Data.INT id) |> check_result_code db ~log:"get report bind id"; let row = zero_or_one_row db ~log:"step: get next report" ~stmt in - let report_fields = Option.map (fun row -> (row.(0), row.(1))) row in + let report_fields = + Option.map + (fun row -> + (Sqlite3.Data.to_string_exn row.(0), Sqlite3.Data.to_string_exn row.(1))) + row + in Sqlite3.finalize stmt |> check_result_code db ~log:"finalize: get report"; report_fields @@ -110,10 +115,12 @@ let get_previous_report_id id = report WHERE id=?) AND type='cmd_step' ORDER BY elapsed_time DESC LIMIT \ 1;" in - Sqlite3.bind stmt 1 (Sqlite3.Data.TEXT id) + Sqlite3.bind stmt 1 (Sqlite3.Data.INT id) |> check_result_code db ~log:"get previous report bind id"; let row = zero_or_one_row db ~log:"step: get next report" ~stmt in - let prev_report_id = Option.map (fun row -> row.(0)) row in + let prev_report_id = + Option.map (fun row -> Sqlite3.Data.to_int64_exn row.(0)) row + in Sqlite3.finalize stmt |> check_result_code db ~log:"finalize: get previous report"; prev_report_id @@ -125,10 +132,12 @@ let get_next_report_id id = "SELECT id FROM report WHERE elapsed_time > (SELECT elapsed_time FROM \ report WHERE id=?) AND type='cmd_step' ORDER BY elapsed_time LIMIT 1;" in - Sqlite3.bind stmt 1 (Sqlite3.Data.TEXT id) + Sqlite3.bind stmt 1 (Sqlite3.Data.INT id) |> check_result_code db ~log:"get next report bind id"; let row = zero_or_one_row db ~log:"step: get next report" ~stmt in - let next_report_id = Option.map (fun row -> row.(0)) row in + let next_report_id = + Option.map (fun row -> Sqlite3.Data.to_int64_exn row.(0)) row + in Sqlite3.finalize stmt |> check_result_code db ~log:"finalize: get next report"; next_report_id @@ -150,7 +159,7 @@ let get_previously_freed_annot loc = Sqlite3.bind stmt 3 (Sqlite3.Data.TEXT loc) |> check_result_code db ~log:"get previous freed annot bind loc"; let row = zero_or_one_row db ~log:"step: get previous freed annot" ~stmt in - let annot = Option.map (fun row -> row.(0)) row in + let annot = Option.map (fun row -> Sqlite3.Data.to_string_exn row.(0)) row in Sqlite3.finalize stmt |> check_result_code db ~log:"finalize: get previous freed annot"; annot diff --git a/GillianCore/logging/logging.ml b/GillianCore/logging/logging.ml index e133e05d0..4bf72e842 100644 --- a/GillianCore/logging/logging.ml +++ b/GillianCore/logging/logging.ml @@ -2,8 +2,6 @@ module LoggingConstants = LoggingConstants module Mode = Mode module Report = Report module Reporter = Reporter -module FileReporter = FileReporter -module DatabaseReporter = DatabaseReporter module Loggable = Loggable module LogQueryer = LogQueryer module ReportId = ReportId @@ -14,6 +12,10 @@ let () = Some (Format.asprintf "!!!!!!!!!!\nFAILURE:\n%s\n!!!!!!!!!!\n\n" s) | _ -> None) +let file_reporter : Reporter.t = (module FileReporter) + +let database_reporter : Reporter.t = (module DatabaseReporter) + let reporters = ref [] let initialize (reporters_to_initialize : (module Reporter.S) list) = diff --git a/GillianCore/logging/logging.mli b/GillianCore/logging/logging.mli index 79f75fbc1..5f31ce5bc 100644 --- a/GillianCore/logging/logging.mli +++ b/GillianCore/logging/logging.mli @@ -22,24 +22,28 @@ end module ReportId : sig type t + + val equal : t -> t -> bool + + val pp : Format.formatter -> t -> unit end module Reporter : sig - module type S = sig - (** Initializes the reporter *) - val initialize : unit -> unit + type t + + (** Calls a given reporter module's `initialize` function *) + val initialize : t -> unit - (** Logs a report *) - val log : Report.t -> unit + (** Calls a given reporter module's `log` function *) + val log : t -> Report.t -> unit - (** Runs any clean up code *) - val wrap_up : unit -> unit - end + (** Calls a given reporter module's `wrap_up` function *) + val wrap_up : t -> unit end -module DatabaseReporter : Reporter.S +val database_reporter : Reporter.t -module FileReporter : Reporter.S +val file_reporter : Reporter.t module Loggable : sig (** Type storing the functions required to log the specified type and the @@ -57,15 +61,15 @@ end module LogQueryer : sig (* Returns the content and the content type given the report id *) - val get_report : string -> (string * string) option + val get_report : ReportId.t -> (string * string) option (* Returns the previous report id which has type cmd_step given the current report id *) - val get_previous_report_id : string -> string option + val get_previous_report_id : ReportId.t -> ReportId.t option (* Returns the next report id which has type cmd_step given the current report id *) - val get_next_report_id : string -> string option + val get_next_report_id : ReportId.t -> ReportId.t option (* Returns the annotation corresponding to the previous set freed action for a given location in the current phase if it exists *) @@ -74,7 +78,7 @@ end (** Initializes the logging module with the specified reporters and initializes the reporters *) -val initialize : (module Reporter.S) list -> unit +val initialize : Reporter.t list -> unit (** Runs any clean up code *) val wrap_up : unit -> unit diff --git a/GillianCore/logging/mode.ml b/GillianCore/logging/mode.ml index 6cf595e1a..3ee2ed4d3 100644 --- a/GillianCore/logging/mode.ml +++ b/GillianCore/logging/mode.ml @@ -4,12 +4,15 @@ type level = | Verbose (** Verbose output *) | TMI (** Too much information *) +(** Type specifying the logging mode *) type t = Disabled | Enabled of level let logging_mode = ref @@ Enabled Verbose +(** Returns whether logging is enabled or not *) let enabled () = !logging_mode <> Disabled +(** Sets the logging mode *) let set_mode mode = logging_mode := mode (** Pretty print function for logging mode type *) diff --git a/GillianCore/logging/reportId.ml b/GillianCore/logging/reportId.ml index e615f9200..24944154c 100644 --- a/GillianCore/logging/reportId.ml +++ b/GillianCore/logging/reportId.ml @@ -8,3 +8,5 @@ let next = c let equal = Int64.equal + +let pp = Fmt.int64 diff --git a/GillianCore/logging/reportId.mli b/GillianCore/logging/reportId.mli index 472be1dc9..e1058bb75 100644 --- a/GillianCore/logging/reportId.mli +++ b/GillianCore/logging/reportId.mli @@ -3,3 +3,5 @@ type t = int64 val next : unit -> t val equal : t -> t -> bool + +val pp : Format.formatter -> t -> unit diff --git a/GillianCore/monadic/MonadicSMemory.ml b/GillianCore/monadic/MonadicSMemory.ml index af27b3182..d54c2d564 100644 --- a/GillianCore/monadic/MonadicSMemory.ml +++ b/GillianCore/monadic/MonadicSMemory.ml @@ -137,4 +137,22 @@ module Lift (MSM : S) : SMemory.S = struct (fun (bch : t Branch.t) -> (bch.value, bch.pc.learned, bch.pc.learned_types)) leeloo_dallas_multibranch + + let of_yojson _ = + failwith + "Please implement of_yojson to enable logging this type to a database" + + let to_yojson _ = + failwith + "Please implement to_yojson to enable logging this type to a database" + + let err_t_of_yojson _ = + failwith + "Please implement err_t_of_yojson to enable logging this type to a \ + database" + + let err_t_to_yojson _ = + failwith + "Please implement err_t_to_yojson to enable logging this type to a \ + database" end diff --git a/GillianCore/parserAndCompiler/ParserAndCompiler.mli b/GillianCore/parserAndCompiler/ParserAndCompiler.mli index f2f4a343f..156d2e67a 100644 --- a/GillianCore/parserAndCompiler/ParserAndCompiler.mli +++ b/GillianCore/parserAndCompiler/ParserAndCompiler.mli @@ -1,5 +1,6 @@ (** This defines an interface that allows a user to indicate how to parse their own programming language, preprocess the obtained language and compile it to GIL (type [Prog.t]) *) + type 'tl_ast compiled_progs = { gil_progs : (string * (Annot.t, string) Prog.t) list; source_files : SourceFiles.t; @@ -8,9 +9,6 @@ type 'tl_ast compiled_progs = { module type S = sig module TargetLangOptions : sig - (** {2 Target-language specific options} - For more help, see Cmdliner documentation *) - (** Command line options specific to the target language. *) type t diff --git a/GillianCore/utils/extList.ml b/GillianCore/utils/extList.ml index 779a00ab9..afec1c6ce 100644 --- a/GillianCore/utils/extList.ml +++ b/GillianCore/utils/extList.ml @@ -1,10 +1,12 @@ type 'a cell = Nil | Cons of { mutable contents : 'a; mutable next : 'a cell } +[@@deriving yojson] type 'a t = { mutable length : int; mutable first : 'a cell; mutable last : 'a cell; } +[@@deriving yojson] let make () = { length = 0; first = Nil; last = Nil } @@ -158,11 +160,11 @@ let remove_duplicates ?(equal = ( = )) l = If the condition is true, then the filtering stops and the function returns true. If the condition is false, then the element is replaced. If the condition is never met, the function returns false - + For example [let f = (fun x -> if x < 5 then `Filter else if x = 10 then `Stop else `Replace (x + 1))] - + [filter_map_stop_cond f \[ 1; 2; 6;7; 4 \]] will modify the list into [\[ 7; 8 \]] and return false [filter_map_stop_cond f \[ 1; 2; 6; 7; 10; 8; 4 \]] will modify the list into [\[ 7; 8; 10; 8; 4 \]] and return true *) diff --git a/GillianCore/utils/extList.mli b/GillianCore/utils/extList.mli index d24657716..0ab6b676d 100644 --- a/GillianCore/utils/extList.mli +++ b/GillianCore/utils/extList.mli @@ -43,11 +43,11 @@ val remove_duplicates : ?equal:('a -> 'a -> bool) -> 'a t -> unit If the condition is true, then the filtering stops and the function returns true. If the condition is false, then the element is replaced. If the condition is never met, the function returns false - + For example [let f = (fun x -> if x < 5 then `Filter else if x = 10 then `Stop else `Replace (x + 1))] - + [filter_map_stop_cond f \[ 1; 2; 6;7; 4 \]] will modify the list into [\[ 7; 8 \]] and return false [filter_map_stop_cond f \[ 1; 2; 6; 7; 10; 8; 4 \]] will modify the list into [\[ 7; 8; 10; 8; 4 \]] and return true *) @@ -57,7 +57,7 @@ val filter_map_stop : (** Works like [filter_map_stop], except it cannot replace elements. [keep] says if the element should be kept and [cond] if the filtering should stop. If an element is not kept, the stop condition is not checked. - + [filter_stop_cond ~keep:(fun x -> x > 5) ~cond:(fun x -> x = 10) \[ 1; 2; 6; 10; 4 \]] will return [\[ 6; 10; 4 \]] *) diff --git a/GillianCore/utils/prelude.ml b/GillianCore/utils/prelude.ml index 0f61bd058..2a662310c 100644 --- a/GillianCore/utils/prelude.ml +++ b/GillianCore/utils/prelude.ml @@ -99,3 +99,4 @@ end module SS = Containers.SS module SI = Containers.SI module SN = Containers.SN +module Syntaxes = Syntaxes diff --git a/GillianCore/utils/syntaxes.ml b/GillianCore/utils/syntaxes.ml index 73b71641b..155048616 100644 --- a/GillianCore/utils/syntaxes.ml +++ b/GillianCore/utils/syntaxes.ml @@ -3,3 +3,9 @@ module Result = struct let ( let* ) o f = Result.bind o f end + +module Option = struct + let ( let+ ) f o = Option.map o f + + let ( let* ) o f = Option.bind o f +end diff --git a/wisl/bin/dune b/wisl/bin/dune index c872828fc..b87689e8e 100644 --- a/wisl/bin/dune +++ b/wisl/bin/dune @@ -6,4 +6,4 @@ (name wisl) (public_name wisl) (package wisl) - (libraries gillian wSemantics wParserAndCompiler wUtils)) + (libraries gillian wSemantics wParserAndCompiler wUtils wDebugging)) diff --git a/wisl/bin/wisl.ml b/wisl/bin/wisl.ml index 6f81e450b..b5bec7682 100644 --- a/wisl/bin/wisl.ml +++ b/wisl/bin/wisl.ml @@ -3,5 +3,6 @@ module CLI = (Gillian.General.External.Dummy) (WParserAndCompiler) (Gillian.Bulk.Runner.DummyRunners) + (WDebugging.WislLifter) let () = CLI.main () diff --git a/wisl/lib/ParserAndCompiler/wParserAndCompiler.ml b/wisl/lib/ParserAndCompiler/wParserAndCompiler.ml index 74e2738fc..01bb6d343 100644 --- a/wisl/lib/ParserAndCompiler/wParserAndCompiler.ml +++ b/wisl/lib/ParserAndCompiler/wParserAndCompiler.ml @@ -3,10 +3,10 @@ open WLexer type err = unit -let pp_err _ () = () - type tl_ast = WProg.t +let pp_err _ () = () + let parse_with_error token lexbuf = try token read lexbuf with | SyntaxError message -> failwith ("SYNTAX ERROR" ^ message) diff --git a/wisl/lib/debugging/dune b/wisl/lib/debugging/dune new file mode 100644 index 000000000..895c3f6b6 --- /dev/null +++ b/wisl/lib/debugging/dune @@ -0,0 +1,4 @@ +(library + (name wDebugging) + (libraries gillian str wParserAndCompiler wSemantics wSyntax wUtils) + (flags :standard -open WUtils -open Gillian.Utils.Prelude)) diff --git a/wisl/lib/debugging/wislLifter.ml b/wisl/lib/debugging/wislLifter.ml new file mode 100644 index 000000000..a3347c2de --- /dev/null +++ b/wisl/lib/debugging/wislLifter.ml @@ -0,0 +1,141 @@ +open WSemantics +open WSyntax +open Gil_syntax +open Debugger + +type memory_error = WislSMemory.err_t + +type tl_ast = WParserAndCompiler.tl_ast + +type memory = WislSMemory.t + +let get_wisl_stmt gil_cmd wisl_ast = + let open Syntaxes.Option in + let* wisl_ast = wisl_ast in + let* annot = + match gil_cmd with + | Some (_, annot) -> Some annot + | _ -> None + in + let origin_id = Annot.get_origin_id annot in + let wprog = WProg.get_by_id wisl_ast origin_id in + match wprog with + | `WStmt wstmt -> Some wstmt.snode + | _ -> None + +let get_cell_var_from_cmd gil_cmd wisl_ast = + let open Syntaxes.Option in + match wisl_ast with + | Some ast -> ( + let* stmt = get_wisl_stmt gil_cmd (Some ast) in + match stmt with + | WStmt.Lookup (_, e) | WStmt.Update (e, _) -> Some (WExpr.str e) + | _ -> None) + | None -> ( + let open WislLActions in + match gil_cmd with + | Some (Cmd.LAction (_, name, [ _; Expr.BinOp (PVar var, _, _) ]), _) + when name = str_ac GetCell -> Some var + | _ -> None) + +let free_error_to_string msg_prefix prev_annot gil_cmd wisl_ast = + let open Syntaxes.Option in + let var = + match wisl_ast with + | Some ast -> ( + let* stmt = get_wisl_stmt gil_cmd (Some ast) in + match stmt with + (* TODO: Catch all the cases that use after free can happen to get the + variable names *) + | WStmt.Dispose e | WStmt.Lookup (_, e) | WStmt.Update (e, _) -> + Some (WExpr.str e) + | _ -> None) + | None -> ( + let open WislLActions in + let* cmd, _ = gil_cmd in + match cmd with + | Cmd.LAction (_, name, [ Expr.BinOp (PVar var, _, _) ]) + when name = str_ac Dispose -> Some var + | Cmd.LAction (_, name, [ _; Expr.BinOp (PVar var, _, _) ]) + when name = str_ac GetCell -> Some var + | _ -> None) + in + let var = Option.value ~default:"" var in + let msg_prefix = msg_prefix var in + match prev_annot with + | None -> Fmt.str "%s in specification" msg_prefix + | Some annot -> ( + let origin_loc = Annot.get_origin_loc annot in + match origin_loc with + | None -> Fmt.str "%s at unknown location" msg_prefix + | Some origin_loc -> + let origin_loc = + DebuggerUtils.location_to_display_location origin_loc + in + Fmt.str "%s at %a" msg_prefix Location.pp origin_loc) + +let get_previously_freed_annot loc = + let annot = Logging.LogQueryer.get_previously_freed_annot loc in + match annot with + | None -> None + | Some annot -> + annot |> Yojson.Safe.from_string |> Annot.of_yojson |> Result.to_option + +let get_missing_resource_var wstmt = + match wstmt with + | Some stmt -> ( + match stmt with + | WStmt.Lookup (_, e) | Update (e, _) -> Some (WExpr.str e) + | _ -> None) + | None -> None + +let get_missing_resource_msg missing_resource_error_info gil_cmd wisl_ast = + let core_pred, loc, offset = missing_resource_error_info in + let default_err_msg = + let prefix = + Fmt.str "Missing %s at location='%s'" (WislLActions.str_ga core_pred) loc + in + match offset with + | None -> prefix + | Some offset -> Fmt.str "%s, offset='%a'" prefix Expr.pp offset + in + match core_pred with + | WislLActions.Cell -> ( + let wstmt = get_wisl_stmt gil_cmd wisl_ast in + let var = get_missing_resource_var wstmt in + match var with + | Some var -> Fmt.str "Try adding %s -> #new_var to the specification" var + | None -> default_err_msg) + | _ -> default_err_msg + +let memory_error_to_exception_info info : Debugger.DebuggerTypes.exception_info + = + let open Gil_to_tl_lifter in + let id = Fmt.to_to_string WislSMemory.pp_err info.error in + let description = + match info.error with + | WislSHeap.MissingResource missing_resource_error_info -> + Some + (get_missing_resource_msg missing_resource_error_info info.command + info.tl_ast) + | DoubleFree loc -> + let prev_annot = get_previously_freed_annot loc in + let msg_prefix var = Fmt.str "%s already freed" var in + Some + (free_error_to_string msg_prefix prev_annot info.command info.tl_ast) + | UseAfterFree loc -> + let prev_annot = get_previously_freed_annot loc in + let msg_prefix var = Fmt.str "%s freed" var in + Some + (free_error_to_string msg_prefix prev_annot info.command info.tl_ast) + | OutOfBounds (bound, _, _) -> + let var = get_cell_var_from_cmd info.command info.tl_ast in + Some + (Fmt.str "%a is not in bounds %a" (Fmt.option Fmt.string) var + (Fmt.option ~none:(Fmt.any "none") Fmt.int) + bound) + | _ -> None + in + { id; description } + +let add_variables = WislSMemory.add_debugger_variables diff --git a/wisl/lib/debugging/wislLifter.mli b/wisl/lib/debugging/wislLifter.mli new file mode 100644 index 000000000..7496afd95 --- /dev/null +++ b/wisl/lib/debugging/wislLifter.mli @@ -0,0 +1,7 @@ +open WSemantics + +include + Gillian.Debugger.Gil_to_tl_lifter.S + with type memory_error = WSemantics.WislSHeap.err + and type tl_ast = WParserAndCompiler.tl_ast + and type memory = WislSMemory.t diff --git a/wisl/lib/semantics/dune b/wisl/lib/semantics/dune index 08ae1c299..fb7804d1d 100644 --- a/wisl/lib/semantics/dune +++ b/wisl/lib/semantics/dune @@ -1,6 +1,6 @@ (library (name wSemantics) (libraries wSyntax wUtils gillian fmt) - (flags :standard -open WUtils -open Gillian.Utils.Prelude) (preprocess - (pps ppx_deriving_yojson))) + (pps ppx_deriving_yojson)) + (flags :standard -open WUtils -open Utils.Prelude)) diff --git a/wisl/lib/semantics/wislLActions.ml b/wisl/lib/semantics/wislLActions.ml index bdb66f6a9..2409208da 100644 --- a/wisl/lib/semantics/wislLActions.ml +++ b/wisl/lib/semantics/wislLActions.ml @@ -11,7 +11,7 @@ type ac = | Alloc | Dispose -type ga = Cell | Bound | Freed +type ga = Cell | Bound | Freed [@@deriving yojson] let str_ac = function | SetCell -> "setcell" diff --git a/wisl/lib/semantics/wislSHeap.ml b/wisl/lib/semantics/wislSHeap.ml index 43d915fa6..6071d0715 100644 --- a/wisl/lib/semantics/wislSHeap.ml +++ b/wisl/lib/semantics/wislSHeap.ml @@ -5,11 +5,11 @@ module Solver = Gillian.Logic.FOSolver module Reduction = Gillian.Logic.Reduction type err = - | MissingRessource - | DoubleFree - | UseAfterFree + | MissingResource of (WislLActions.ga * string * Expr.t option) + | DoubleFree of string + | UseAfterFree of string | MemoryLeak - | OutOfBound + | OutOfBounds of (int option * string * Expr.t) | InvalidLocation [@@deriving yojson] @@ -68,6 +68,23 @@ let init () = Hashtbl.create 1 let copy heap = Hashtbl.copy heap +(****** Types and functions for logging when blocks have been freed ********) + +type set_freed_info = { loc : string } [@@deriving yojson] + +let set_freed_info_pp fmt set_freed = + Fmt.pf fmt "Set Freed at location %s" set_freed.loc + +let set_freed_with_logging heap loc = + let set_freed_info = { loc } in + let _ = + Logging.normal_specific + (Logging.Loggable.make set_freed_info_pp set_freed_info_of_yojson + set_freed_info_to_yojson set_freed_info) + Logging.LoggingConstants.ContentType.set_freed_info + in + Hashtbl.replace heap loc Block.Freed + (***** Implementation of local actions *****) let alloc (heap : t) size = @@ -86,8 +103,10 @@ let alloc (heap : t) size = let dispose (heap : t) loc = match Hashtbl.find_opt heap loc with - | Some (Allocated { data = _; bound = None }) | None -> Error MissingRessource - | Some Freed -> Error DoubleFree + | None -> Error (MissingResource (Cell, loc, None)) + | Some (Allocated { data = _; bound = None }) -> + Error (MissingResource (Bound, loc, None)) + | Some Freed -> Error (DoubleFree loc) | Some (Allocated { data; bound = Some i }) -> let has_all = let so_far = ref true in @@ -97,14 +116,14 @@ let dispose (heap : t) loc = !so_far in if has_all then - let () = Hashtbl.replace heap loc Freed in + let () = set_freed_with_logging heap loc in Ok () - else Error MissingRessource + else Error (MissingResource (Bound, loc, None)) let get_cell ~pfs ~gamma heap loc ofs = match Hashtbl.find_opt heap loc with - | None -> Error MissingRessource - | Some Block.Freed -> Error UseAfterFree + | None -> Error (MissingResource (Cell, loc, Some ofs)) + | Some Block.Freed -> Error (UseAfterFree loc) | Some (Allocated { data; bound }) -> ( let maybe_out_of_bound = match bound with @@ -114,7 +133,7 @@ let get_cell ~pfs ~gamma heap loc ofs = let open Formula.Infix in Solver.sat ~unification:false ~pfs ~gamma [ n #<= ofs ] in - if maybe_out_of_bound then Error OutOfBound + if maybe_out_of_bound then Error (OutOfBounds (bound, loc, ofs)) else match SFVL.get ofs data with | Some v -> Ok (loc, ofs, v) @@ -125,7 +144,7 @@ let get_cell ~pfs ~gamma heap loc ofs = data with | Some (o, v) -> Ok (loc, o, v) - | None -> Error MissingRessource)) + | None -> Error (MissingResource (Cell, loc, Some ofs)))) let set_cell ~pfs ~gamma heap loc_name ofs v = match Hashtbl.find_opt heap loc_name with @@ -134,7 +153,7 @@ let set_cell ~pfs ~gamma heap loc_name ofs v = let bound = None in let () = Hashtbl.replace heap loc_name (Allocated { data; bound }) in Ok () - | Some Block.Freed -> Error UseAfterFree + | Some Block.Freed -> Error (UseAfterFree loc_name) | Some (Allocated { data; bound }) -> let maybe_out_of_bound = match bound with @@ -144,7 +163,7 @@ let set_cell ~pfs ~gamma heap loc_name ofs v = let open Formula.Infix in Solver.sat ~unification:false ~pfs ~gamma [ n #<= ofs ] in - if maybe_out_of_bound then Error UseAfterFree + if maybe_out_of_bound then Error (UseAfterFree loc_name) else let equality_test = Solver.is_equal ~pfs ~gamma in let data = SFVL.add_with_test ~equality_test ofs v data in @@ -153,8 +172,8 @@ let set_cell ~pfs ~gamma heap loc_name ofs v = let rem_cell heap loc offset = match Hashtbl.find_opt heap loc with - | None -> Error MissingRessource - | Some Block.Freed -> Error UseAfterFree + | None -> Error (MissingResource (Cell, loc, Some offset)) + | Some Block.Freed -> Error (UseAfterFree loc) | Some (Allocated { bound; data }) -> let data = SFVL.remove offset data in let () = Hashtbl.replace heap loc (Allocated { bound; data }) in @@ -162,14 +181,16 @@ let rem_cell heap loc offset = let get_bound heap loc = match Hashtbl.find_opt heap loc with - | Some Block.Freed -> Error UseAfterFree - | None | Some (Allocated { bound = None; _ }) -> Error MissingRessource + | Some Block.Freed -> Error (UseAfterFree loc) + | None -> Error (MissingResource (Cell, loc, None)) + | Some (Allocated { bound = None; _ }) -> + Error (MissingResource (Bound, loc, None)) | Some (Allocated { bound = Some bound; _ }) -> Ok bound let set_bound heap loc bound = let prev = Option.value ~default:Block.empty (Hashtbl.find_opt heap loc) in match prev with - | Freed -> Error UseAfterFree + | Freed -> Error (UseAfterFree loc) | Allocated { data; _ } -> let changed = Block.Allocated { data; bound = Some bound } in let () = Hashtbl.replace heap loc changed in @@ -177,8 +198,10 @@ let set_bound heap loc bound = let rem_bound heap loc = match Hashtbl.find_opt heap loc with - | Some Block.Freed -> Error UseAfterFree - | None | Some (Allocated { bound = None; _ }) -> Error MissingRessource + | Some Block.Freed -> Error (UseAfterFree loc) + | None -> Error (MissingResource (Cell, loc, None)) + | Some (Allocated { bound = None; _ }) -> + Error (MissingResource (Bound, loc, None)) | Some (Allocated { data; _ }) -> let () = Hashtbl.replace heap loc (Allocated { data; bound = None }) in Ok () @@ -187,16 +210,16 @@ let get_freed heap loc = match Hashtbl.find_opt heap loc with | Some Block.Freed -> Ok () | Some _ -> Error MemoryLeak - | None -> Error MissingRessource + | None -> Error (MissingResource (Freed, loc, None)) -let set_freed heap loc = Hashtbl.replace heap loc Block.Freed +let set_freed heap loc = set_freed_with_logging heap loc let rem_freed heap loc = match Hashtbl.find_opt heap loc with | Some Block.Freed -> Hashtbl.remove heap loc; Ok () - | None -> Error MissingRessource + | None -> Error (MissingResource (Freed, loc, None)) | Some _ -> Error MemoryLeak (***** Some things specific to symbolic heaps ********) @@ -263,3 +286,96 @@ let pp fmt heap = ( Fmt.iter_bindings ~sep:(Fmt.any "@\n@\n") Hashtbl.iter @@ fun ft (l, b) -> Block.pp ~loc:l ft b ) heap + +let get_store_vars store is_gil_file = + List.filter_map + (fun (var, (value : Gil_syntax.Expr.t)) -> + if (not is_gil_file) && Str.string_match (Str.regexp "gvar") var 0 then + None + else + let match_offset lst loc loc_pp = + match lst with + | [ Expr.Lit (Num offset) ] -> + Fmt.str "-> (%a, %.0f)" (Fmt.hbox loc_pp) loc offset + | [ offset ] -> + Fmt.str "-> (%a, %a)" (Fmt.hbox loc_pp) loc (Fmt.hbox Expr.pp) + offset + | _ -> Fmt.to_to_string (Fmt.hbox Expr.pp) + value + in + let value = + match value with + | Expr.EList (Lit (Loc loc) :: rest) | Expr.EList (LVar loc :: rest) + -> match_offset rest loc Fmt.string + | _ -> Fmt.to_to_string (Fmt.hbox Expr.pp) value + in + Some + ({ name = var; value; type_ = None; var_ref = 0 } + : Debugger.DebuggerTypes.variable)) + store + |> List.sort Stdlib.compare + +let add_memory_vars (smemory : t) (get_new_scope_id : unit -> int) variables : + Debugger.DebuggerTypes.variable list = + let open Debugger.DebuggerTypes in + let vstr = Fmt.to_to_string (Fmt.hbox Expr.pp) in + let compare_offsets (v, _) (w, _) = + try + let open Expr.Infix in + let difference = v -. w in + match difference with + | Expr.Lit (Num f) -> if f < 0. then -1 else if f > 0. then 1 else 0 + | _ -> 0 + with _ -> (* Do not sort the offsets if an exception has occurred *) + 0 + in + let cell_vars l : variable list = + List.sort compare_offsets l + |> List.map (fun (offset, value) : variable -> + (* Display offset as a number to match the printing of WISL pointers *) + let offset_str = + match offset with + | Expr.Lit (Num f) -> Fmt.str "%.0f" f + | other -> vstr other + in + create_leaf_variable offset_str (vstr value) ()) + in + smemory |> Hashtbl.to_seq + |> Seq.map (fun (loc, blocks) -> + match blocks with + | Block.Freed -> create_leaf_variable loc "freed" () + | Allocated { data; bound } -> + let bound = + match bound with + | None -> "none" + | Some bound -> string_of_int bound + in + let bound = create_leaf_variable "bound" bound () in + let cells_id = get_new_scope_id () in + let () = + Hashtbl.replace variables cells_id + (cell_vars (SFVL.to_list data)) + in + let cells = create_node_variable "cells" cells_id () in + let loc_id = get_new_scope_id () in + let () = Hashtbl.replace variables loc_id [ bound; cells ] in + create_node_variable loc loc_id ~value:"allocated" ()) + |> List.of_seq + +let add_debugger_variables + ~store ~memory ~is_gil_file ~get_new_scope_id variables = + let open Debugger.DebuggerTypes in + let store_id = get_new_scope_id () in + let memory_id = get_new_scope_id () in + let scopes : scope list = + [ { id = store_id; name = "Store" }; { id = memory_id; name = "Memory" } ] + in + let store_vars = get_store_vars store is_gil_file in + let memory_vars = add_memory_vars memory get_new_scope_id variables in + let vars = [ store_vars; memory_vars ] in + let () = + List.iter2 + (fun (scope : scope) vars -> Hashtbl.replace variables scope.id vars) + scopes vars + in + scopes diff --git a/wisl/lib/semantics/wislSHeap.mli b/wisl/lib/semantics/wislSHeap.mli index fe3ee66ab..c335f5063 100644 --- a/wisl/lib/semantics/wislSHeap.mli +++ b/wisl/lib/semantics/wislSHeap.mli @@ -4,11 +4,11 @@ open Gil_syntax type t [@@deriving yojson] type err = - | MissingRessource - | DoubleFree - | UseAfterFree + | MissingResource of (WislLActions.ga * string * Expr.t option) + | DoubleFree of string + | UseAfterFree of string | MemoryLeak - | OutOfBound + | OutOfBounds of (int option * string * Expr.t) | InvalidLocation [@@deriving yojson] @@ -62,3 +62,11 @@ val substitution_in_place : list val assertions : t -> Gillian.Gil_syntax.Asrt.t list + +val add_debugger_variables : + store:(string * Gillian.Gil_syntax.Expr.t) list -> + memory:t -> + is_gil_file:bool -> + get_new_scope_id:(unit -> int) -> + Debugger.DebuggerTypes.variables -> + Debugger.DebuggerTypes.scope list diff --git a/wisl/lib/semantics/wislSMemory.ml b/wisl/lib/semantics/wislSMemory.ml index ae6e915de..bca616610 100644 --- a/wisl/lib/semantics/wislSMemory.ml +++ b/wisl/lib/semantics/wislSMemory.ml @@ -287,12 +287,12 @@ let get_print_info _ _ = (SS.empty, SS.empty) let pp_err fmt t = Fmt.string fmt (match t with - | WislSHeap.MissingRessource -> "MissingRessource" - | DoubleFree -> "Double Free" - | UseAfterFree -> "Use After Free" - | MemoryLeak -> "Memory Leak" - | OutOfBound -> "Out of bound" - | InvalidLocation -> "Invalid Location") + | WislSHeap.MissingResource _ -> "Missing Resource" + | DoubleFree _ -> "Double Free" + | UseAfterFree _ -> "Use After Free" + | MemoryLeak -> "Memory Leak" + | OutOfBounds _ -> "Out Of Bounds" + | InvalidLocation -> "Invalid Location") let get_recovery_vals _ _ = [] @@ -320,3 +320,5 @@ let apply_fix m _ _ _ = m let get_fixes ?simple_fix:_ _ _ _ _ = [] let get_failing_constraint _ = Formula.True + +let add_debugger_variables = WislSHeap.add_debugger_variables diff --git a/wisl/lib/semantics/wislSMemory.mli b/wisl/lib/semantics/wislSMemory.mli index cd9fd2360..300ca7c03 100644 --- a/wisl/lib/semantics/wislSMemory.mli +++ b/wisl/lib/semantics/wislSMemory.mli @@ -1 +1,9 @@ -include Gillian.Symbolic.Memory_S +include Gillian.Symbolic.Memory_S with type err_t = WislSHeap.err + +val add_debugger_variables : + store:(string * Gillian.Gil_syntax.Expr.t) list -> + memory:t -> + is_gil_file:bool -> + get_new_scope_id:(unit -> int) -> + Debugger.DebuggerTypes.variables -> + Debugger.DebuggerTypes.scope list diff --git a/wisl/runtime/wisl_core.gil b/wisl/runtime/wisl_core.gil index b41d17c0e..8a37342b5 100644 --- a/wisl/runtime/wisl_core.gil +++ b/wisl/runtime/wisl_core.gil @@ -9,4 +9,4 @@ pred i__pred_cell (+ptr: List, value): pred freed(+ptr: List): (ptr == {{ #l, 0. }}) * types(#l: Obj) * - (#l;); + (#l;);