tcheck: make global env0 mutable

necessary for correct unmarshalling, as this
must contain global variables

bin/asli.ml

@@ -370,7 +370,7 @@ let main () =
         LNoise.history_set ~max_length:100 |> ignore;
 
         let denv = Dis.build_env env in
-        let tcenv = TC.Env.mkEnv TC.env0 and cpu = Cpu.mkCPU env denv in
+        let tcenv = TC.Env.mkEnv !TC.env0 and cpu = Cpu.mkCPU env denv in
 
         repl tcenv cpu
     end

libASL/dis.ml

@@ -180,7 +180,7 @@ module LocalEnv = struct
 
     let init (env: Eval.Env.t) =
         let eval e = val_expr (Eval.eval_expr Unknown env e) in
-        let tenv = Tcheck.env0 in
+        let tenv = !Tcheck.env0 in
         let get_global_type id =
             (match Tcheck.GlobalEnv.getGlobalVar tenv id with
             | Some (Type_Bits e) ->
@@ -642,7 +642,7 @@ and width_of_type (loc: l) (t: ty): int =
   | _ -> unsupported loc @@ "Can't get bit width of type: " ^ pp_type t
 
 and width_of_field (loc: l) (t: ty) (f: ident): int =
-  let env = Tcheck.env0 in
+  let env = !Tcheck.env0 in
   let ft =
     (match Tcheck.typeFields env loc t with
     | FT_Record rfs -> Tcheck.get_recordfield loc rfs f
@@ -654,7 +654,7 @@ and width_of_field (loc: l) (t: ty) (f: ident): int =
 
 (** Determine the type of memory access expression (Var, Array, Field) *)
 and type_of_load (loc: l) (x: expr): ty rws =
-  let env = Tcheck.env0 in
+  let env = !Tcheck.env0 in
   (match x with
   | Expr_Var(id) ->
       let+ (_,(t,_)) = DisEnv.gets (LocalEnv.resolveGetVar loc id) in

libASL/eval.ml

@@ -1359,7 +1359,7 @@ let evaluation_environment (prelude: LoadASL.source) (files: LoadASL.source list
             None
     ) in
 
-    let tcenv = TC.Env.mkEnv Tcheck.env0 in
+    let tcenv = TC.Env.mkEnv !Tcheck.env0 in
     Option.iter (fun env -> List.iter (evaluate_prj_minimal tcenv env) prjs) env;
     env
 

libASL/tcheck.ml

@@ -2448,7 +2448,7 @@ let genPrototypes (ds: AST.declaration list): (AST.declaration list * AST.declar
     (List.rev !pre, List.rev !post)
 
 (** Overall typechecking environment shared by all invocations of typechecker *)
-let env0 = GlobalEnv.mkempty ()
+let env0 = ref (GlobalEnv.mkempty ())
 
 (** Typecheck a list of declarations - main entrypoint into typechecker *)
 let tc_declarations (isPrelude: bool) (ds: AST.declaration list): AST.declaration list =
@@ -2463,8 +2463,8 @@ let tc_declarations (isPrelude: bool) (ds: AST.declaration list): AST.declaratio
      *)
     let (pre, post) = if isPrelude then (ds, []) else genPrototypes ds in
     if verbose then Printf.printf "  - Typechecking %d phase 1 declarations\n" (List.length pre);
-    let pre'  = List.map (tc_declaration env0) pre  in
-    let post' = List.map (tc_declaration env0) post in
+    let pre'  = List.map (tc_declaration !env0) pre  in
+    let post' = List.map (tc_declaration !env0) post in
     if verbose then List.iter (fun ds -> List.iter (fun d -> Printf.printf "\nTypechecked %s\n" (Utils.to_string (PP.pp_declaration d))) ds) post';
     if verbose then Printf.printf "  - Typechecking %d phase 2 declarations\n" (List.length post);
     List.append (List.concat pre') (List.concat post')

tests/test_asl.ml

@@ -101,7 +101,7 @@ let test_compare env () : unit =
 let tests : unit Alcotest.test_case list =
     let prelude = LoadASL.read_file (FileSource "../../../prelude.asl") true false in
     let mra = List.map (fun tool -> LoadASL.read_file tool false false) (mra_tools ()) in
-    let tcenv   = TC.Env.mkEnv TC.env0 in
+    let tcenv   = TC.Env.mkEnv !TC.env0 in
     let env     = Eval.build_evaluation_environment (prelude @ List.concat mra) in
     [
         ("arith", `Quick, test_arith tcenv env);