Fix WISL lifter bugs

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

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

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

debugger-vscode-extension/sampleWorkspace/wpst/llen_wpst.wisl

@@ -24,6 +24,7 @@ function build_list(size) {
 
 function main() {
   fresh x;
+  assume_type (x, Int);
   assume (x >= 2);
   assume (x <= 3);
   l := build_list(x);

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 ()

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 }

wisl/lib/ParserAndCompiler/WParser.mly

@@ -3,7 +3,7 @@
 (* key words *)
 %token <CodeLoc.t> TRUE FALSE NULL WHILE IF ELSE SKIP FRESH NEW DELETE
 %token <CodeLoc.t> FUNCTION RETURN PREDICATE LEMMA
-%token <CodeLoc.t> INVARIANT PACKAGE FOLD UNFOLD NOUNFOLD APPLY ASSERT ASSUME EXIST FORALL
+%token <CodeLoc.t> INVARIANT PACKAGE FOLD UNFOLD NOUNFOLD APPLY ASSERT ASSUME ASSUME_TYPE EXIST FORALL
 %token <CodeLoc.t> STATEMENT WITH VARIANT PROOF
 
 (* punctuation *)
@@ -28,6 +28,7 @@
 %token <CodeLoc.t> TLIST
 %token <CodeLoc.t> TINT
 %token <CodeLoc.t> TBOOL
+%token <CodeLoc.t> TSTRING
 
 (* names *)
 %token <CodeLoc.t * string> 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

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")

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

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)

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 }
 

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

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