From 05db1377f1b987050e58643b9bf001f62a77e303 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 5 Jan 2022 08:43:24 +0100
Subject: Introduce the type_context definition

---
 src/CfimAst.ml     |  7 +++++++
 src/Contexts.ml    |  6 ++++--
 src/Interpreter.ml | 21 +++++++++++----------
 src/Invariants.ml  |  4 ++--
 src/Print.ml       | 10 ++++++----
 src/main.ml        | 40 +++++++++++++++++++++++-----------------
 6 files changed, 53 insertions(+), 35 deletions(-)

(limited to 'src')

diff --git a/src/CfimAst.ml b/src/CfimAst.ml
index 192638cf..6c9b596e 100644
--- a/src/CfimAst.ml
+++ b/src/CfimAst.ml
@@ -86,3 +86,10 @@ type fun_def = {
   body : statement;
 }
 [@@deriving show]
+(** TODO: the type and function definitions contain information like `divergent`
+  * or `copyable`. I wonder if this information should be stored directly inside
+  * the definitions or inside separate maps/sets.
+  * Of course, if everything is stored in separate maps/sets, nothing
+  * prevents us from computing this info in Charon (and thus exporting directly
+  * it with the type/function defs), in which case we just have to implement special
+  * treatment when deserializing, to move the info to a separate map. *)
diff --git a/src/Contexts.ml b/src/Contexts.ml
index 5e8ae3d0..521ea0ed 100644
--- a/src/Contexts.ml
+++ b/src/Contexts.ml
@@ -60,8 +60,10 @@ type interpreter_mode = ConcreteMode | SymbolicMode [@@deriving show]
 type config = { mode : interpreter_mode; check_invariants : bool }
 [@@deriving show]
 
+type type_context = { type_defs : type_def list } [@@deriving show]
+
 type eval_ctx = {
-  type_context : type_def list;
+  type_context : type_context;
   fun_context : fun_def list;
   type_vars : type_var list;
   env : env;
@@ -94,7 +96,7 @@ let ctx_lookup_binder (ctx : eval_ctx) (vid : VarId.id) : binder =
   lookup ctx.env
 
 let ctx_lookup_type_def (ctx : eval_ctx) (tid : TypeDefId.id) : type_def =
-  TypeDefId.nth ctx.type_context tid
+  TypeDefId.nth ctx.type_context.type_defs tid
 
 let ctx_lookup_fun_def (ctx : eval_ctx) (fid : FunDefId.id) : fun_def =
   FunDefId.nth ctx.fun_context fid
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 1107ee20..a335a0d5 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -2361,8 +2361,8 @@ let expand_bottom_value_from_projection (config : C.config)
     | ( Field (ProjAdt (def_id, opt_variant_id), _),
         T.Adt (T.AdtId def_id', regions, types) ) ->
         assert (def_id = def_id');
-        compute_expanded_bottom_adt_value ctx.type_context def_id opt_variant_id
-          regions types
+        compute_expanded_bottom_adt_value ctx.type_context.type_defs def_id
+          opt_variant_id regions types
     (* Tuples *)
     | Field (ProjTuple arity, _), T.Adt (T.Tuple, [], tys) ->
         assert (arity = List.length tys);
@@ -2391,7 +2391,7 @@ let compute_expanded_symbolic_adt_value (expand_enumerations : bool)
     (ctx : C.eval_ctx) : (C.eval_ctx * symbolic_expansion) list =
   (* Lookup the definition and check if it is an enumeration with several
    * variants *)
-  let def = T.TypeDefId.nth ctx.type_context def_id in
+  let def = C.ctx_lookup_type_def ctx def_id in
   assert (List.length regions = List.length def.T.region_params);
   (* Retrieve, for every variant, the list of its instantiated field types *)
   let variants_fields_types =
@@ -2976,7 +2976,7 @@ let constant_value_to_typed_value (ctx : C.eval_ctx) (ty : T.ety)
       assert (def_id = def_id');
       (* Check that the adt definition only has one variant with no fields,
          compute the variant id at the same time. *)
-      let def = T.TypeDefId.nth ctx.type_context def_id in
+      let def = C.ctx_lookup_type_def ctx def_id in
       assert (List.length def.region_params = 0);
       assert (List.length def.type_params = 0);
       let variant_id =
@@ -3382,14 +3382,14 @@ let set_discriminant (config : C.config) (ctx : C.eval_ctx) (p : E.place)
           else
             (* Replace the value *)
             let bottom_v =
-              compute_expanded_bottom_adt_value ctx.type_context def_id
-                (Some variant_id) regions types
+              compute_expanded_bottom_adt_value ctx.type_context.type_defs
+                def_id (Some variant_id) regions types
             in
             let ctx = write_place_unwrap config access p bottom_v ctx in
             Ok (ctx, Unit))
   | T.Adt (T.AdtId def_id, regions, types), V.Bottom ->
       let bottom_v =
-        compute_expanded_bottom_adt_value ctx.type_context def_id
+        compute_expanded_bottom_adt_value ctx.type_context.type_defs def_id
           (Some variant_id) regions types
       in
       let ctx = write_place_unwrap config access p bottom_v ctx in
@@ -3894,7 +3894,7 @@ module Test = struct
   (** Test a unit function (taking no arguments) by evaluating it in an empty
     environment
  *)
-  let test_unit_function (type_defs : T.type_def list)
+  let test_unit_function (type_context : C.type_context)
       (fun_defs : A.fun_def list) (fid : A.FunDefId.id) : unit eval_result =
     (* Retrieve the function declaration *)
     let fdef = A.FunDefId.nth fun_defs fid in
@@ -3911,7 +3911,7 @@ module Test = struct
     (* Create the evaluation context *)
     let ctx =
       {
-        C.type_context = type_defs;
+        C.type_context;
         C.fun_context = fun_defs;
         C.type_vars = [];
         C.env = [];
@@ -3942,7 +3942,8 @@ module Test = struct
       (fun_defs : A.fun_def list) : unit =
     let test_fun (def : A.fun_def) : unit =
       if fun_def_is_unit def then
-        match test_unit_function type_defs fun_defs def.A.def_id with
+        let type_ctx = { C.type_defs } in
+        match test_unit_function type_ctx fun_defs def.A.def_id with
         | Error _ -> failwith "Unit test failed"
         | Ok _ -> ()
       else ()
diff --git a/src/Invariants.ml b/src/Invariants.ml
index fec6b2ed..364c14d0 100644
--- a/src/Invariants.ml
+++ b/src/Invariants.ml
@@ -352,7 +352,7 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
         | V.Adt av, T.Adt (T.AdtId def_id, regions, tys) ->
             (* Retrieve the definition to check the variant id, the number of
              * parameters, etc. *)
-            let def = T.TypeDefId.nth ctx.type_context def_id in
+            let def = C.ctx_lookup_type_def ctx def_id in
             (* Check the number of parameters *)
             assert (List.length regions = List.length def.region_params);
             assert (List.length tys = List.length def.type_params);
@@ -435,7 +435,7 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
         | V.AAdt av, T.Adt (T.AdtId def_id, regions, tys) ->
             (* Retrieve the definition to check the variant id, the number of
              * parameters, etc. *)
-            let def = T.TypeDefId.nth ctx.type_context def_id in
+            let def = C.ctx_lookup_type_def ctx def_id in
             (* Check the number of parameters *)
             assert (List.length regions = List.length def.region_params);
             assert (List.length tys = List.length def.type_params);
diff --git a/src/Print.ml b/src/Print.ml
index 2fd7e336..90f3946b 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -492,17 +492,19 @@ module Contexts = struct
       v.name
     in
     let type_def_id_to_string def_id =
-      let def = T.TypeDefId.nth ctx.type_context def_id in
+      let def = T.TypeDefId.nth ctx.type_context.type_defs def_id in
       PT.name_to_string def.name
     in
     let adt_variant_to_string =
-      type_ctx_to_adt_variant_to_string_fun ctx.type_context
+      type_ctx_to_adt_variant_to_string_fun ctx.type_context.type_defs
     in
     let var_id_to_string vid =
       let bv = C.ctx_lookup_binder ctx vid in
       binder_to_string bv
     in
-    let adt_field_names = type_ctx_to_adt_field_names_fun ctx.C.type_context in
+    let adt_field_names =
+      type_ctx_to_adt_field_names_fun ctx.type_context.type_defs
+    in
     {
       rvar_to_string;
       r_to_string;
@@ -604,7 +606,7 @@ module CfimAst = struct
   let eval_ctx_to_ast_formatter (ctx : C.eval_ctx) : ast_formatter =
     let ctx_fmt = PC.eval_ctx_to_ctx_formatter ctx in
     let adt_field_to_string =
-      type_ctx_to_adt_field_to_string_fun ctx.type_context
+      type_ctx_to_adt_field_to_string_fun ctx.type_context.type_defs
     in
     let fun_def_id_to_string def_id =
       let def = A.FunDefId.nth ctx.fun_context def_id in
diff --git a/src/main.ml b/src/main.ml
index 4616aadf..f2e6eb06 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -1,9 +1,11 @@
 open CfimOfJson
 open Logging
 open Print
+open Contexts
 module T = Types
 module A = CfimAst
 module I = Interpreter
+module C = Contexts
 
 type test = Test [@@deriving show]
 
@@ -13,31 +15,35 @@ let _ = show_test Test
  * reason, the -g option doesn't work *)
 let () = Printexc.record_backtrace true
 
-let usage = Printf.sprintf {|Aenaes: verification of Rust programs by translation
+let usage =
+  Printf.sprintf
+    {|Aenaes: verification of Rust programs by translation
 
 Usage: %s [OPTIONS] FILE
-|} Sys.argv.(0);;
+|}
+    Sys.argv.(0)
 
 let () =
-  let spec = [
-  ] in
+  let spec = [] in
   let spec = Arg.align spec in
   let filename = ref "" in
-  let fail () = print_string usage; exit 1 in
-  Arg.parse spec (fun f ->
-    if not (Filename.check_suffix f ".cfim") then begin
-      print_string "Unrecognized file extension";
-      fail ()
-    end else if not (Sys.file_exists f) then begin
-      print_string "File not found";
-      fail ()
-    end else
-      filename := f
-  ) usage;
-  if !filename = "" then begin
+  let fail () =
     print_string usage;
     exit 1
-  end;
+  in
+  Arg.parse spec
+    (fun f ->
+      if not (Filename.check_suffix f ".cfim") then (
+        print_string "Unrecognized file extension";
+        fail ())
+      else if not (Sys.file_exists f) then (
+        print_string "File not found";
+        fail ())
+      else filename := f)
+    usage;
+  if !filename = "" then (
+    print_string usage;
+    exit 1);
   let json = Yojson.Basic.from_file !filename in
   match cfim_module_of_json json with
   | Error s -> log#error "error: %s\n" s
-- 
cgit v1.2.3