diff --git a/GillianCore/GIL_Syntax/Branch_case.ml b/GillianCore/GIL_Syntax/Branch_case.ml index 4b169e55d..cdeaffc99 100644 --- a/GillianCore/GIL_Syntax/Branch_case.ml +++ b/GillianCore/GIL_Syntax/Branch_case.ml @@ -6,7 +6,7 @@ type t = | LActionFail of int [@@deriving show, yojson] -type path = t list [@@deriving yojson] +type path = t list [@@deriving yojson, show] let pp_short fmt = function | GuardedGoto b -> Fmt.pf fmt "%B" b diff --git a/GillianCore/GIL_Syntax/Gil_syntax.mli b/GillianCore/GIL_Syntax/Gil_syntax.mli index 2651f68ee..2b92a3f14 100644 --- a/GillianCore/GIL_Syntax/Gil_syntax.mli +++ b/GillianCore/GIL_Syntax/Gil_syntax.mli @@ -1017,7 +1017,7 @@ module Branch_case : sig (** A list of branch cases describes the path of execution. Every termination of a symbolic execution is uniquely identified by its branch path. *) - type path = t list [@@deriving yojson] + type path = t list [@@deriving yojson, show] val pp_short : Format.formatter -> t -> unit end diff --git a/GillianCore/engine/general_semantics/general/g_interpreter.ml b/GillianCore/engine/general_semantics/general/g_interpreter.ml index 294f963df..19f4f2fc4 100644 --- a/GillianCore/engine/general_semantics/general/g_interpreter.ml +++ b/GillianCore/engine/general_semantics/general/g_interpreter.ml @@ -158,7 +158,7 @@ struct type conf_selector = | Path of Branch_case.path | IdCase of L.Report_id.t * Branch_case.t option - [@@deriving to_yojson] + [@@deriving to_yojson, show] type 'result cont_func_f = ?selector:conf_selector -> unit -> 'result cont_func @@ -1963,7 +1963,10 @@ struct in match List.find_map pred results with | Some result -> Ok result - | None -> Error "No result for selector!" + | None -> + Fmt.error "No result for selector (%a)!" + (pp_option pp_conf_selector) + selector let end_of_branch results eval_step_state = let { conf; rest_confs; ret_fun; f; selector; _ } = eval_step_state in diff --git a/wisl/bin/wisl.ml b/wisl/bin/wisl.ml index 33d7baac9..db94608a4 100644 --- a/wisl/bin/wisl.ml +++ b/wisl/bin/wisl.ml @@ -3,6 +3,10 @@ open Gillian.Debugger module SMemory = Gillian.Symbolic.Legacy_s_memory.Modernize (WSemantics.WislSMemory) +module Lifter = + Lifter.Gil_fallback_lifter.Make (SMemory) (WParserAndCompiler) + (WDebugging.WislLifter.Make) + module CLI = Gillian.Command_line.Make (Gillian.General.Init_data.Dummy) @@ -11,7 +15,6 @@ module CLI = (WParserAndCompiler) (Gillian.General.External.Dummy (WParserAndCompiler.Annot)) (Gillian.Bulk.Runner.DummyRunners) - (Lifter.Gil_fallback_lifter.Make (SMemory) (WParserAndCompiler) - (WDebugging.WislLifter.Make)) + (Lifter) let () = CLI.main () diff --git a/wisl/lib/ParserAndCompiler/WLexer.mll b/wisl/lib/ParserAndCompiler/WLexer.mll index 6dcc44ac0..4c870d392 100644 --- a/wisl/lib/ParserAndCompiler/WLexer.mll +++ b/wisl/lib/ParserAndCompiler/WLexer.mll @@ -46,6 +46,7 @@ rule read = | "apply" { APPLY (curr lexbuf) } | "assert" { ASSERT (curr lexbuf) } | "assume" { ASSUME (curr lexbuf) } + | "assume_type" { ASSUME_TYPE (curr lexbuf) } | "with" { WITH (curr lexbuf) } | "variant" { VARIANT (curr lexbuf) } | "statement" { STATEMENT (curr lexbuf) } @@ -57,6 +58,7 @@ rule read = | "List" { TLIST (curr lexbuf) } | "Int" { TINT (curr lexbuf) } | "Bool" { TBOOL (curr lexbuf) } + | "String" { TSTRING (curr lexbuf) } (* strings and comments *) | '"' { let () = l_start_string := curr lexbuf in read_string (Buffer.create 17) lexbuf } diff --git a/wisl/lib/ParserAndCompiler/WParser.mly b/wisl/lib/ParserAndCompiler/WParser.mly index 3e23adcf1..6f7b0df60 100644 --- a/wisl/lib/ParserAndCompiler/WParser.mly +++ b/wisl/lib/ParserAndCompiler/WParser.mly @@ -3,7 +3,7 @@ (* key words *) %token TRUE FALSE NULL WHILE IF ELSE SKIP FRESH NEW DELETE %token FUNCTION RETURN PREDICATE LEMMA -%token INVARIANT PACKAGE FOLD UNFOLD NOUNFOLD APPLY ASSERT ASSUME EXIST FORALL +%token INVARIANT PACKAGE FOLD UNFOLD NOUNFOLD APPLY ASSERT ASSUME ASSUME_TYPE EXIST FORALL %token STATEMENT WITH VARIANT PROOF (* punctuation *) @@ -28,6 +28,7 @@ %token TLIST %token TINT %token TBOOL +%token TSTRING (* names *) %token IDENTIFIER @@ -189,6 +190,11 @@ logic_cmds: | LCMD; lcmds = separated_list(SEMICOLON, logic_command); RCBRACE { lcmds } */ +type_target: + | TLIST { WType.WList } + | TINT { WType.WInt } + | TBOOL { WType.WBool } + | TSTRING { WType.WString } statement: | loc = SKIP { WStmt.make WStmt.Skip loc } @@ -269,6 +275,12 @@ statement: let loc = CodeLoc.merge lstart lend in WStmt.make bare_stmt loc } + | lstart = ASSUME_TYPE; LBRACE; e = expression; COMMA; t = type_target; lend = RBRACE; + { + let bare_stmt = WStmt.AssumeType (e, t) in + let loc = CodeLoc.merge lstart lend in + WStmt.make bare_stmt loc + } expr_list: @@ -391,11 +403,6 @@ predicate: pred_id; } } -type_target: - | TLIST { WType.WList } - | TINT { WType.WInt } - | TBOOL { WType.WBool } - pred_param_ins: | inp = option(PLUS); lx = IDENTIFIER; option(preceded(COLON, type_target)) { let (_, x) = lx in diff --git a/wisl/lib/ParserAndCompiler/wisl2Gil.ml b/wisl/lib/ParserAndCompiler/wisl2Gil.ml index f10582a33..b7cc2a063 100644 --- a/wisl/lib/ParserAndCompiler/wisl2Gil.ml +++ b/wisl/lib/ParserAndCompiler/wisl2Gil.ml @@ -674,12 +674,13 @@ let rec compile_stmt_list ?(fname = "main") ?(is_loop_prefix = false) stmtl = WAnnot.make ~origin_id:sid_while ~origin_loc:(CodeLoc.to_location sloc) () in + let annot_branch = { annot with branch_kind = Some WhileLoopKind } in let annot_hidden = WAnnot.{ annot with stmt_kind = Hidden } in let headlabopt = Some looplab in let headcmd = Cmd.Skip in let headcmd_lab = (annot_hidden, headlabopt, headcmd) in let loopcmd = Cmd.GuardedGoto (guard, bodlab, endlab) in - let loopcmd_lab = (annot, None, loopcmd) in + let loopcmd_lab = (annot_branch, None, loopcmd) in let backcmd = Cmd.Goto looplab in let backcmd_lab = (annot_hidden, None, backcmd) in let endcmd = Cmd.Skip in @@ -914,6 +915,15 @@ let rec compile_stmt_list ?(fname = "main") ?(is_loop_prefix = false) stmtl = in let comp_rest, new_functions = compile_list rest in (cmdle @ [ (annot, None, cmd) ] @ comp_rest, new_functions) + | { snode = AssumeType (e, t); sid; sloc } :: rest -> + let typ = WType.to_gil t in + let annot = + WAnnot.make ~origin_id:sid ~origin_loc:(CodeLoc.to_location sloc) () + in + let cmdle, comp_e = compile_expr e in + let cmd = Cmd.Logic (LCmd.AssumeType (comp_e, typ)) in + let comp_rest, new_functions = compile_list rest in + (cmdle @ [ (annot, None, cmd) ] @ comp_rest, new_functions) let compile_spec ?(fname = "main") diff --git a/wisl/lib/debugging/wislLifter.ml b/wisl/lib/debugging/wislLifter.ml index ac4a921de..9fd771f2d 100644 --- a/wisl/lib/debugging/wislLifter.ml +++ b/wisl/lib/debugging/wislLifter.ml @@ -231,18 +231,14 @@ struct | _ -> NoSubmap in let++ kind = - match ends with - | _ when is_return exec_data -> Ok Final - | [] -> Ok Final - | [ (Unknown, _) ] -> - if is_loop_end ~is_loop_func ~proc_name exec_data then Ok Final - else Ok Normal - | ends -> - let++ cases = ends_to_cases ~nest_kind ends in - let cases = - List.sort (fun (a, _) (b, _) -> Branch_case.compare a b) cases - in - Branch cases + let++ cases = ends_to_cases ~nest_kind ends in + match cases with + | _ when is_return exec_data -> Final + | [] -> Final + | [ (Case (Unknown, _), _) ] -> + if is_loop_end ~is_loop_func ~proc_name exec_data then Final + else Normal + | _ -> Branch cases in Finished { @@ -274,7 +270,7 @@ struct | None, prev_case -> Ok prev_case | Some prev_kind, Unknown -> ( match prev_kind with - | IfElseKind -> ( + | IfElseKind | WhileLoopKind -> ( match gil_case with | Some (Gil_branch_case.GuardedGoto b) -> Ok (IfElse b) | _ -> Error "IfElseKind expects a GuardedGoto gil case")) @@ -423,18 +419,9 @@ struct let update = Update.f - let find_or_init ~partials ~get_prev ~exec_data prev_id = - let ({ id; _ } : exec_data) = exec_data in + let find_or_init ~partials ~get_prev prev_id = let partial = let* prev_id = prev_id in - let () = - DL.log (fun m -> - let t_json = - partials |> to_yojson |> Yojson.Safe.pretty_to_string - in - m "%a: Looking for prev_id %a in:\n%s" pp_rid id pp_rid prev_id - t_json) - in Hashtbl.find_opt partials prev_id in match partial with @@ -463,7 +450,7 @@ struct ~prev_id exec_data = let partial = - find_or_init ~partials ~get_prev ~exec_data prev_id + find_or_init ~partials ~get_prev prev_id |> Result_utils.or_else (fun e -> failwith ~exec_data ~partials e) in Hashtbl.replace partials exec_data.id partial; @@ -525,6 +512,7 @@ struct let Partial_cmds.{ all_ids; kind; callers; _ } = finished_partial in match (kind, callers) with | Final, caller_id :: _ -> + let () = DL.log (fun m -> m "A") in let label, count = match Hashtbl.find_opt state.func_return_map caller_id with | Some (label, count) -> (label, count) @@ -535,7 +523,9 @@ struct let cont_id = all_ids |> List.rev |> List.hd in let** () = update_caller_branches ~caller_id ~cont_id label state in Ok (Some label) - | _ -> Ok None + | _ -> + let () = DL.log (fun m -> m "B") in + Ok None let make_new_cmd ~func_return_label finished_partial : map = let Partial_cmds. @@ -606,26 +596,42 @@ struct parent_data.submap <- Submap new_cmd; Ok () - let insert_cmd ~state ~prev ~stack_direction ~func_return_label new_cmd = + let insert_cmd ~state ~prev ~stack_direction new_cmd = match (stack_direction, state.map, prev) with | Some _, Nothing, _ -> Error "stepping in our out with empty map!" | _, Nothing, Some _ -> Error "inserting to empty map with prev!" | None, Nothing, None -> state.map <- new_cmd; - Ok () + Ok new_cmd | _, _, None -> Error "inserting to non-empty map with no prev!" - | Some In, _, Some (_, Some _) -> Error "stepping in with branch case!" + | Some In, _, Some (parent_id, Some FuncExitPlaceholder) | Some In, _, Some (parent_id, None) -> - insert_as_submap ~state ~parent_id new_cmd + let new_cmd = new_cmd |> map_data (fun d -> { d with prev = None }) in + let++ () = insert_as_submap ~state ~parent_id new_cmd in + new_cmd + | Some In, _, Some (_, Some case) -> + Fmt.error "stepping in with branch case (%a)!" Branch_case.pp case | None, _, Some (prev_id, case) -> - insert_as_next ~state ~prev_id ?case new_cmd - | Some (Out prev_id), _, _ -> + let++ () = insert_as_next ~state ~prev_id ?case new_cmd in + new_cmd + | Some (Out prev_id), _, Some (inner_prev_id, _) -> let** case = + let func_return_label = + match Hashtbl.find state.id_map inner_prev_id with + | Nothing -> None + | Cmd { data; _ } | BranchCmd { data; _ } | FinalCmd { data } -> + data.func_return_label + in match func_return_label with | Some (label, ix) -> Ok (Case (FuncExit label, ix)) | None -> Error "stepping out without function return label!" in - insert_as_next ~state ~prev_id ~case new_cmd + let new_cmd = + new_cmd + |> map_data (fun d -> { d with prev = Some (prev_id, Some case) }) + in + let++ () = insert_as_next ~state ~prev_id ~case new_cmd in + new_cmd let f ~state finished_partial = let r = @@ -637,9 +643,7 @@ struct resolve_func_branches ~state finished_partial in let new_cmd = make_new_cmd ~func_return_label finished_partial in - let** () = - insert_cmd ~state ~prev ~stack_direction ~func_return_label new_cmd - in + let** new_cmd = insert_cmd ~state ~prev ~stack_direction new_cmd in all_ids |> List.iter (fun id -> Hashtbl.replace id_map id new_cmd); Ok new_cmd in @@ -685,8 +689,8 @@ struct in match map with | Nothing -> Error "got Nothing map!" - | FinalCmd _ -> Error "prev map is Final!" - | Cmd { data; _ } -> Ok (Some (data.id, None, data.callers)) + | FinalCmd { data } | Cmd { data; _ } -> + Ok (Some (data.id, None, data.callers)) | BranchCmd { data; nexts } -> ( let case = Hashtbl.find_map diff --git a/wisl/lib/syntax/WStmt.ml b/wisl/lib/syntax/WStmt.ml index 052f1a055..f3e634999 100644 --- a/wisl/lib/syntax/WStmt.ml +++ b/wisl/lib/syntax/WStmt.ml @@ -15,6 +15,7 @@ type tt = | Logic of WLCmd.t | Assert of WExpr.t | Assume of WExpr.t + | AssumeType of WExpr.t * WType.t and t = { sid : int; sloc : CodeLoc.t; snode : tt } @@ -53,6 +54,8 @@ and pp fmt stmt = | Logic lcmd -> Format.fprintf fmt "@[[[ %a ]]@]" WLCmd.pp lcmd | Assert e -> Format.fprintf fmt "@[assert %a@]" WExpr.pp e | Assume e -> Format.fprintf fmt "@[assume %a@]" WExpr.pp e + | AssumeType (e, t) -> + Format.fprintf fmt "@[assume_type (%a, %a)@]" WExpr.pp e WType.pp t and pp_head fmt stmt = match get stmt with @@ -93,8 +96,12 @@ let rec get_by_id id stmt = let lcmd_getter = WLCmd.get_by_id id in let aux s = match get s with - | Dispose e | Lookup (_, e) | VarAssign (_, e) | Assert e | Assume e -> - expr_getter e + | Dispose e + | Lookup (_, e) + | VarAssign (_, e) + | Assert e + | Assume e + | AssumeType (e, _) -> expr_getter e | Update (e1, e2) -> expr_getter e1 |>> (expr_getter, e2) | FunCall (_, _, el, _) -> expr_list_visitor el | While (e, sl) -> expr_getter e |>> (list_visitor, sl) diff --git a/wisl/lib/syntax/WStmt.mli b/wisl/lib/syntax/WStmt.mli index 2588bc449..be9051654 100644 --- a/wisl/lib/syntax/WStmt.mli +++ b/wisl/lib/syntax/WStmt.mli @@ -13,6 +13,7 @@ type tt = | Logic of WLCmd.t (** logic command *) | Assert of WExpr.t (** non-SL assertion *) | Assume of WExpr.t (** non-SL assumption *) + | AssumeType of WExpr.t * WType.t (** type assumption *) and t = { sid : int; sloc : CodeLoc.t; snode : tt } diff --git a/wisl/lib/syntax/WType.ml b/wisl/lib/syntax/WType.ml index 79d4e4c31..2817f6bea 100644 --- a/wisl/lib/syntax/WType.ml +++ b/wisl/lib/syntax/WType.ml @@ -37,6 +37,13 @@ let pp fmt t = | WAny -> s "Any" | WSet -> s "Set" +let to_gil = function + | WList -> Gil_syntax.Type.ListType + | WInt -> Gil_syntax.Type.IntType + | WString -> Gil_syntax.Type.StringType + | WBool -> Gil_syntax.Type.BooleanType + | t -> Fmt.failwith "Can't convert type '%a' to GIL!" pp t + exception Unmatching_types module TypeMap = Map.Make (struct diff --git a/wisl/lib/syntax/WType.mli b/wisl/lib/syntax/WType.mli index 1f9de6cc6..6f66fc142 100644 --- a/wisl/lib/syntax/WType.mli +++ b/wisl/lib/syntax/WType.mli @@ -3,6 +3,7 @@ type t = WList | WNull | WBool | WString | WPtr | WInt | WAny | WSet val compatible : t -> t -> bool val strongest : t -> t -> t val pp : Format.formatter -> t -> unit +val to_gil : t -> Gillian.Gil_syntax.Type.t exception Unmatching_types diff --git a/wisl/lib/utils/wBranchCase.ml b/wisl/lib/utils/wBranchCase.ml index f3b36ecea..d8b80279d 100644 --- a/wisl/lib/utils/wBranchCase.ml +++ b/wisl/lib/utils/wBranchCase.ml @@ -1,31 +1,15 @@ -type kind = IfElseKind [@@deriving yojson] -type case = IfElse of bool | FuncExit of string | Unknown [@@deriving yojson] +type kind = IfElseKind | WhileLoopKind [@@deriving yojson] + +type case = IfElse of bool | WhileLoop of bool | FuncExit of string | Unknown +[@@deriving yojson] + type t = Case of case * int | FuncExitPlaceholder [@@deriving yojson] let pp fmt = function | Case (Unknown, i) -> Fmt.pf fmt "%d" i - | Case (IfElse b, -1) -> Fmt.pf fmt "%B" b - | Case (IfElse b, i) -> Fmt.pf fmt "%B - %d" b i + | Case ((IfElse b | WhileLoop b), -1) -> Fmt.pf fmt "%B" b + | Case ((IfElse b | WhileLoop b), i) -> Fmt.pf fmt "%B - %d" b i | Case (FuncExit label, i) -> Fmt.pf fmt "%s-%d" label i | FuncExitPlaceholder -> Fmt.pf fmt "" let display = Fmt.str "%a" pp - -let compare a b = - let compare_pair (a1, a2) (b1, b2) = - let cmp = Int.compare a1 b1 in - if cmp = 0 then String.compare a2 b2 else cmp - in - let get_ix = function - | FuncExitPlaceholder -> (0, "") - | Case (IfElse false, _) -> (1, "") - | Case (IfElse true, _) -> (2, "") - | Case (FuncExit l, _) -> (3, l) - | Case (Unknown, _) -> (4, "") - in - let cmp = compare_pair (get_ix a) (get_ix b) in - match (cmp, a, b) with - | 0, FuncExitPlaceholder, _ | 0, _, FuncExitPlaceholder -> - failwith "impossible" - | 0, Case (_, a), Case (_, b) -> Int.compare a b - | cmp, _, _ -> cmp