add support for thread spawning

lib/ast/astDef.ml

@@ -1212,6 +1212,7 @@ module Stmt = struct
     call_lhs : qual_ident list;
     call_name : qual_ident;
     call_args : expr list;
+    call_is_spawn : bool;
   }
 
 
@@ -1377,7 +1378,7 @@ module Stmt = struct
     | Call cstm -> (
         match cstm.call_lhs with
         | [] ->
-            fprintf ppf "@[%a(@[%a@])@]" QualIdent.pr cstm.call_name
+            fprintf ppf "@[%s%a(@[%a@])@]" (if cstm.call_is_spawn then "spawn " else "") QualIdent.pr cstm.call_name
               Expr.pr_list cstm.call_args
         | _ ->
             fprintf ppf "@[<2>%a@ :=@ @[%a(@[%a@])@]@]" QualIdent.pr_list
@@ -1508,8 +1509,8 @@ module Stmt = struct
   let mk_cond ~loc ?(cond_if_assumes_false = false) test then_ else_ =
     { stmt_desc = Cond { cond_test = test; cond_then = then_; cond_else = else_; cond_if_assumes_false }; stmt_loc = loc }
 
-  let mk_call ~loc ?(lhs=[]) name args =
-    { stmt_desc = Basic (Call { call_lhs = lhs; call_name = name; call_args = args }); stmt_loc = loc }
+  let mk_call ~loc ?(lhs=[]) name args ~is_spawn =
+    { stmt_desc = Basic (Call { call_lhs = lhs; call_name = name; call_args = args; call_is_spawn = is_spawn }); stmt_loc = loc }
 
   let mk_assign ~loc lhs rhs =
     { stmt_desc = Basic (Assign { assign_lhs = lhs; assign_rhs = rhs; assign_is_init = false }); stmt_loc = loc }

lib/ast/rewriter.ml

@@ -864,7 +864,7 @@ module Stmt = struct
             let call_name = f call.call_name in
             {
               stmt with
-              stmt_desc = Basic (Call { call_lhs; call_name; call_args });
+              stmt_desc = Basic (Call { call with call_lhs; call_name; call_args });
             }
         | Use use_desc ->
             let use_name = f use_desc.use_name in

lib/ast/symbolTbl.ml

@@ -217,7 +217,8 @@ let resolve name (tbl : t) :
               else Set.add inst_scopes target_qual_ident
             in
             go_forward new_inst_scopes tbl.tbl_root subst new_path
-            (* /// why do we jump to tbl.root from here? *)
+            (* /// why do we jump to tbl.root from here?
+               TW: Because the remainder of the path to be traversed has been requalified relative to target_qual_ident, which is a fully qualified id. *)
         | Import qual_ident, _ ->
             (* Logs.debug (fun m -> m "SymbolTbl.resolve.go_forward: 2"); *)
             let target_qual_ident = (*QualIdent.requalify subst*) qual_ident in
@@ -442,11 +443,6 @@ let add_symbol ?(scope : scope option = None) symbol tbl =
     | ModInst mod_inst ->
         let mod_inst_qual_ident, subst =
           match mod_inst.mod_inst_def with
-          | None ->
-              let _, mod_inst_type, _mod_inst_symbol, _ =
-                resolve_and_find_exn mod_inst.mod_inst_type tbl
-              in
-              (mod_inst_type, [])
           | Some (mod_inst_func, mod_inst_args) -> (
               let _, mod_inst_func, mod_inst_symbol, _subst1 =
                 resolve_and_find_exn mod_inst_func tbl
@@ -467,12 +463,18 @@ let add_symbol ?(scope : scope option = None) symbol tbl =
                     (formal_id, QualIdent.to_list arg))
               in
               match res with
-              | Ok subst -> (mod_inst_func, subst)
+              | Ok subst ->
+                (mod_inst_func, subst)
               | Unequal_lengths ->
                   Error.type_error symbol_loc
                     (Printf.sprintf
                        !"Module %{QualIdent} expects %d arguments"
                        mod_inst_func (List.length formals)))
+          | None ->
+              let _, mod_inst_type, _mod_inst_symbol, _ =
+                resolve_and_find_exn mod_inst.mod_inst_type tbl
+              in
+              (mod_inst_type, [])
         in
         let is_abstract = mod_inst.mod_inst_is_interface in
         add_to_map

lib/frontend/lexer.mll

@@ -61,6 +61,7 @@ let _ =
       ("returns", RETURNS);
       (* ("subseteq", SUBSETEQ); *)
       ("Set", SET);
+      ("spawn", SPAWN);
       ("true", CONSTVAL (Expr.Bool true));
       ("type", TYPE);
       ("unfold", USE (Stmt.Unfold));

lib/frontend/parser.mly

@@ -20,7 +20,7 @@ open Ast
 %token <Ast.Stmt.spec_kind> SPEC
 %token <Ast.Stmt.use_kind> USE  
 %token HAVOC NEW RETURN OWN AU
-%token IF ELSE WHILE CAS
+%token IF ELSE WHILE CAS SPAWN
 %token <Ast.Callable.call_kind> FUNC
 %token PROC AXIOM LEMMA
 %token CASE DATA INT REAL BOOL PERM SET MAP ATOMICTOKEN FIELD REF
@@ -432,6 +432,18 @@ stmt_wo_trailing_substmt:
   in
   Stmt.(Basic (Assign assign))
 }
+(* thread spawn *)
+| SPAWN; id = qual_ident; LPAREN; args = separated_list(COMMA, expr); RPAREN; SEMICOLON {
+  let open Stmt in
+  let call =
+    { call_lhs = [];
+      call_name = Expr.to_qual_ident id;
+      call_args = args;
+      call_is_spawn = true
+    }
+  in
+  Basic (Call call)
+}
 (* assignment / allocation *)
 | es = separated_nonempty_list(COMMA, expr); COLONEQ; e = assign_rhs; SEMICOLON {
   let open Stmt in

lib/frontend/rewrites/rewrites.ml

@@ -620,7 +620,7 @@ let rec rewrite_loops (stmt : Stmt.t) : Stmt.t Rewriter.t =
 
           Stmt.mk_call ~loc ~lhs:lhs_list
             (QualIdent.from_ident loop_proc_name)
-            args_list
+            args_list ~is_spawn:false
         in
 
         (* TODO: Rename variables from curr_vars to loop_vars in loop body *)
@@ -700,7 +700,7 @@ let rec rewrite_loops (stmt : Stmt.t) : Stmt.t Rewriter.t =
 
         Stmt.mk_call ~loc ~lhs:lhs_list
           (QualIdent.from_ident loop_proc_name)
-          args_list
+          args_list ~is_spawn:false
       in
 
       Logs.debug (fun m -> m "Loop new_stmt:\n %a" Stmt.pr new_stmt);
@@ -1104,7 +1104,10 @@ let rec rewrite_call_stmts (stmt : Stmt.t) : Stmt.t Rewriter.t =
 
       let call_decl, call_def =
         match symbol with
-        | CallDef c -> (c.call_decl, c.call_def)
+        | CallDef c ->
+          if call_desc.call_is_spawn
+          then ({c.call_decl with call_decl_postcond = []; call_decl_returns= []}, c.call_def)
+          else (c.call_decl, c.call_def)
         | _ -> Error.error stmt.stmt_loc "Expected a call_def"
       in
 

lib/frontend/typing.ml

@@ -1282,6 +1282,7 @@ module ProcessCallable = struct
                     List.map var_decls_lhs ~f:(fun var -> var.var_name |> QualIdent.from_ident);
                   call_name = proc_qual_ident;
                   call_args = args;
+                  call_is_spawn = false;
                 }
               in                      
               (Stmt.Call call_desc, disam_tbl)
@@ -1562,7 +1563,7 @@ module ProcessCallable = struct
          This function is not expected to go over these parts of the AST again. If the following constructs are
          discovered by this function, then something unexpected has happened. *)
       (* Now that we call process_symbol on arbitrarily AST elements, we need to deal with these constructs too *)
-    | Call call_desc -> (
+    | Call call_desc -> (        
         let* call_lhs, var_decls_lhs =
           Rewriter.List.fold_right call_desc.call_lhs ~init:([], [])
             ~f:(fun orig_qual_ident (assign_lhs, var_decls_lhs) ->
@@ -1592,6 +1593,7 @@ module ProcessCallable = struct
         | App (Var proc_qual_ident, args, _expr_attr) ->
           let (call_desc : Stmt.call_desc) =
             {
+              call_desc with
               call_lhs;
               call_name = proc_qual_ident;
               call_args = args;