Merge pull request #75 from AeneasVerif/protz_confusion

Fix confusion in the construction of clause mappings that refer to parent clauses

bin/main.ml

@@ -243,15 +243,16 @@ Supported options:|}
   let files = Eurydice.Cleanup2.remove_implicit_array_copies#visit_files () files in
   (* These two need to come before... *)
   let files = Krml.Inlining.cross_call_analysis files in
-  Eurydice.Logging.log "Phase2.7" "%a" pfiles files;
   let files = Krml.Simplify.remove_unused files in
   (* This chunk which reuses key elements of simplify2 *)
   let files = Krml.Simplify.sequence_to_let#visit_files () files in
+  Eurydice.Logging.log "Phase2.7" "%a" pfiles files;
   let files = Krml.Simplify.hoist#visit_files [] files in
+  Eurydice.Logging.log "Phase2.75" "%a" pfiles files;
   let files = Krml.Simplify.fixup_hoist#visit_files () files in
+  Eurydice.Logging.log "Phase2.8" "%a" pfiles files;
   let files = Krml.Simplify.misc_cosmetic#visit_files () files in
   let files = Krml.Simplify.let_to_sequence#visit_files () files in
-  Eurydice.Logging.log "Phase2.8" "%a" pfiles files;
   let files = Eurydice.Cleanup3.bonus_cleanups#visit_files [] files in
   (* Macros stemming from globals *)
   let files, macros = Eurydice.Cleanup2.build_macros files in
@@ -330,9 +331,15 @@ Supported options:|}
   in
 
   Eurydice.Logging.log "Phase3.3" "%a" pfiles files;
-  let files = List.map (fun (f, ds) -> f, List.filter (fun d ->
-    not (Krml.Idents.LidSet.mem (Krml.Ast.lid_of_decl d) Eurydice.Builtin.skip))
-  ds) files in
+  let files =
+    List.map
+      (fun (f, ds) ->
+        ( f,
+          List.filter
+            (fun d -> not (Krml.Idents.LidSet.mem (Krml.Ast.lid_of_decl d) Eurydice.Builtin.skip))
+            ds ))
+      files
+  in
   let files = AstToCStar.mk_files files c_name_map Idents.LidSet.empty macros in
 
   let headers = CStarToC11.mk_headers c_name_map files in

include/eurydice_glue.h

@@ -18,13 +18,13 @@ extern "C" {
 #include "krml/lowstar_endianness.h"
 
 #define LowStar_Ignore_ignore(e, t, _ret_t) ((void)e)
-#define EURYDICE_ASSERT(test, msg) do { \
-  if (!(test)) { \
-    fprintf(stderr, \
-           "assertion \"%s\" failed: file \"%s\", line %d\n", \
-                               msg, __FILE__, __LINE__); \
-  } \
-} while (0)
+#define EURYDICE_ASSERT(test, msg)                                             \
+  do {                                                                         \
+    if (!(test)) {                                                             \
+      fprintf(stderr, "assertion \"%s\" failed: file \"%s\", line %d\n", msg,  \
+              __FILE__, __LINE__);                                             \
+    }                                                                          \
+  } while (0)
 
 // SLICES, ARRAYS, ETC.
 

lib/AstOfLlbc.ml

@@ -449,12 +449,16 @@ let push_clause_binders env bs = List.fold_left push_clause_binder env bs
 
 let lookup_clause_binder env clause_id item_name =
   let i, (v, t) =
-    findi
-      (function
-        | TraitClauseMethod (clause_id2, item_name2, _), _ ->
-            clause_id2 = clause_id && item_name2 = item_name
-        | _ -> false)
-      env.binders
+    try
+      findi
+        (function
+          | TraitClauseMethod (clause_id2, item_name2, _), _ ->
+              clause_id2 = clause_id && item_name2 = item_name
+          | _ -> false)
+        env.binders
+    with Not_found ->
+      Krml.KPrint.bprintf "Error looking up %s.%s\n" (C.show_trait_instance_id clause_id) item_name;
+      raise Not_found
   in
   i, t, thd3 (assert_trait_clause_method v)
 
@@ -726,7 +730,10 @@ let blocklisted_trait_decls =
    the types we obtain by looking up the trait declaration have Self as 0
    (DeBruijn).
 *)
-let rec build_trait_clause_mapping env (trait_clauses : C.trait_clause list) =
+let rec build_trait_clause_mapping env (trait_clauses : C.trait_clause list) :
+    ((C.trait_instance_id * string)
+    * (C.generic_args * K.type_scheme * Charon.Types.name * C.fun_sig))
+    list =
   List.concat_map
     (fun tc ->
       let { C.clause_id; trait = { trait_decl_id; decl_generics }; _ } = tc in
@@ -765,13 +772,20 @@ let rec build_trait_clause_mapping env (trait_clauses : C.trait_clause list) =
           (trait_decl.C.required_methods @ trait_decl.C.provided_methods)
         @ List.flatten
             (List.mapi
-               (fun i (parent_clause : C.trait_clause) ->
+               (fun _i (parent_clause : C.trait_clause) ->
                  (* Mapping of the methods of the parent clause *)
                  let m = build_trait_clause_mapping env [ parent_clause ] in
                  List.map
-                   (fun ((clause_id, m), v) ->
-                     (* This is the parent clause `i` of `clause_id` -- see comments in charon/types.rs  *)
-                     let id = C.(ParentClause (clause_id, trait_decl_id, TraitClauseId.of_int i)) in
+                   (fun (((clause_id' : C.trait_instance_id), m), v) ->
+                     (* This is the parent clause `clause_id'` of `clause_id` -- see comments in charon/types.rs  *)
+                     let clause_id' =
+                       match clause_id' with
+                       | Clause clause_id' -> clause_id'
+                       | _ -> fail "not a clause??"
+                     in
+                     let id : C.trait_instance_id =
+                       ParentClause (Clause clause_id, trait_decl_id, clause_id')
+                     in
                      (id, m), v)
                    m)
                trait_decl.C.parent_clauses)

lib/Builtin.ml

@@ -18,9 +18,10 @@ let option : K.lident = [ "core"; "option" ], "Option"
 let mk_option (t : K.typ) : K.typ = K.TApp (option, [ t ])
 let array_copy = [ "Eurydice" ], "array_copy"
 let macros = Krml.Idents.LidSet.of_list []
+
 (* Things that could otherwise be emitted as an extern prototype, but for some
    reason ought to be skipped. *)
-let skip = Krml.Idents.LidSet.of_list [ ["Eurydice"], "assert" ]
+let skip = Krml.Idents.LidSet.of_list [ [ "Eurydice" ], "assert" ]
 let result = [ "core"; "result" ], "Result"
 let mk_result t1 t2 = K.TApp (result, [ t1; t2 ])
 let nonzero = [ "core"; "num"; "nonzero" ], "NonZero"
@@ -305,16 +306,16 @@ let min_u32 =
 (* Not fully general *)
 let static_assert, static_assert_ref =
   let name = [ "Eurydice" ], "assert" in
-  let typ =Krml.Helpers.fold_arrow [ TBool;
-    Krml.Checker.c_string ] TUnit in
-  K.DExternal (None, [ Krml.Common.Private; Macro ], 0, 0,
-    name, typ,
-    [ "test"; "msg" ]), K.(with_type typ (EQualified name))
+  let typ = Krml.Helpers.fold_arrow [ TBool; Krml.Checker.c_string ] TUnit in
+  ( K.DExternal (None, [ Krml.Common.Private; Macro ], 0, 0, name, typ, [ "test"; "msg" ]),
+    K.(with_type typ (EQualified name)) )
 
 let unwrap : K.decl =
   let open Krml in
   let open Ast in
-  let lid = [ "core"; "result"; "{core::result::Result<T, E>}" ], "unwrap" in
+  let lid =
+    [ "core"; "result"; "{core::result::Result<T, E>[TraitClause@0, TraitClause@1]}" ], "unwrap"
+  in
   let t_T = TBound 1 in
   let t_E = TBound 0 in
   let t_result = mk_result t_T t_E in

lib/Cleanup2.ml

@@ -702,9 +702,8 @@ let recognize_asserts =
       match e1.typ, e2.node, e3.node with
       | TBool, EUnit, EAbort (_, msg) ->
           (* if not (e1) then abort msg else ()  -->  static_assert(e1, msg) *)
-          EApp (Builtin.static_assert_ref, [ e1; with_type
-          Krml.Checker.c_string (EString (Option.value ~default:"" msg)) ])
-      | _ ->
-          super#visit_EIfThenElse env e1 e2 e3
-
+          EApp
+            ( Builtin.static_assert_ref,
+              [ e1; with_type Krml.Checker.c_string (EString (Option.value ~default:"" msg)) ] )
+      | _ -> super#visit_EIfThenElse env e1 e2 e3
   end

lib/Cleanup3.ml

@@ -9,7 +9,6 @@
 *)
 
 module B = Builtin
-
 open Krml
 open Ast