Update charon

Author: Nadrieril

charon-pin

@@ -1,2 +1,2 @@
 # This is the commit from https://github.com/AeneasVerif/charon that should be used with this version of aeneas.
-e341486cc6fece9c176a1189e1a75a6c105360ac
+93e45d693a2ad424ec89b934cc1140d72b49f328

flake.lock

@@ -663,7 +663,7 @@ let greedy_expand_symbolics_with_borrows (config : config) (span : Meta.span) :
                       > 1 variants (option \
                       [greedy_expand_symbolics_with_borrows] of [config]): "
                     ^ name_to_string ctx def.item_meta.name)
-              | Alias _ | Opaque | TError _ ->
+              | Alias _ | Opaque | TDeclError _ ->
                   craise __FILE__ __LINE__ span
                     "Attempted to greedily expand an alias or opaque type"
               | Union _ ->
@@ -689,7 +689,8 @@ let greedy_expand_symbolics_with_borrows (config : config) (span : Meta.span) :
         | TTraitType _
         | TArrow _
         | TRawPtr _
-        | TDynTrait _ -> craise __FILE__ __LINE__ span "Unreachable"
+        | TDynTrait _
+        | TError _ -> craise __FILE__ __LINE__ span "Unreachable"
       in
       (* *)
       log#ltrace

src/interp/InterpreterExpansion.ml

@@ -266,6 +266,9 @@ let rec norm_ctx_normalize_ty (ctx : norm_ctx) (ty : ty) : ty =
   | TDynTrait _ ->
       craise_opt_span __FILE__ __LINE__ ctx.span
         "Dynamic trait types are not supported yet"
+  | TError _ ->
+      craise_opt_span __FILE__ __LINE__ ctx.span
+        "Found type error in the output of charon"
 
 (** This returns the normalized trait instance id together with an optional
     reference to a trait **implementation** (the `trait_ref` we return has

src/llbc/AssociatedTypes.ml

@@ -181,6 +181,9 @@ let compute_regions_hierarchy_for_sig (span : Meta.span option) (crate : crate)
     | TDynTrait _ ->
         craise_opt_span __FILE__ __LINE__ span
           "Dynamic trait types are not supported yet"
+    | TError _ ->
+        craise_opt_span __FILE__ __LINE__ span
+          "Found type error in the output of charon"
   and explore_generics (outer : region list) (generics : generic_args) =
     let { regions; types; const_generics = _; trait_refs = _ } = generics in
     List.iter (fun long -> add_edges ~long ~shorts:outer) regions;

src/llbc/RegionsHierarchy.ml

@@ -365,6 +365,9 @@ let analyze_full_ty (span : Meta.span option) (updated : bool ref)
             ty_info inputs
         in
         analyze span expl_info ty_info output
+    | TError _ ->
+        craise_opt_span __FILE__ __LINE__ span
+          "Found type error in the output of charon"
   in
   (* Explore *)
   analyze span expl_info_init ty_info ty
@@ -394,7 +397,7 @@ let analyze_type_decl (updated : bool ref) (infos : type_infos)
             "type aliases should have been removed earlier"
       | Union _ ->
           craise __FILE__ __LINE__ def.item_meta.span "unions are not supported"
-      | Opaque | TError _ ->
+      | Opaque | TDeclError _ ->
           craise __FILE__ __LINE__ def.item_meta.span "unreachable"
     in
     (* Explore the types and accumulate information *)

src/llbc/TypesAnalysis.ml

@@ -195,7 +195,7 @@ let symbolic_value_is_greedily_expandable (span : Meta.span option)
           | Struct _ | Enum ([] | [ _ ]) ->
               (* Structure or enumeration with <= 1 variant *)
               true
-          | Enum (_ :: _) | Alias _ | Opaque | TError _ | Union _ ->
+          | Enum (_ :: _) | Alias _ | Opaque | TDeclError _ | Union _ ->
               (* Enumeration with > 1 variants *)
               false
         end

src/llbc/ValuesUtils.ml

@@ -1525,7 +1525,7 @@ let simplify_aggregates (ctx : ctx) (def : fun_decl) : fun_decl =
                 in
                 let fields =
                   match adt_decl.kind with
-                  | Enum _ | Alias _ | Opaque | TError _ ->
+                  | Enum _ | Alias _ | Opaque | TDeclError _ ->
                       craise __FILE__ __LINE__ def.item_meta.span "Unreachable"
                   | Union _ ->
                       craise __FILE__ __LINE__ def.item_meta.span

src/pure/PureMicroPasses.ml

@@ -575,6 +575,9 @@ let rec translate_sty (span : Meta.span option) (ty : T.ty) : ty =
   | TDynTrait _ ->
       craise_opt_span __FILE__ __LINE__ span
         "Dynamic trait types are not supported yet"
+  | TError _ ->
+      craise_opt_span __FILE__ __LINE__ span
+        "Found type error in the output of charon"
 
 and translate_sgeneric_args (span : Meta.span option)
     (generics : T.generic_args) : generic_args =
@@ -652,7 +655,7 @@ let translate_type_decl_kind (span : Meta.span) (kind : T.type_decl_kind) :
   | Alias _ ->
       craise __FILE__ __LINE__ span
         "type aliases should have been removed earlier"
-  | T.Union _ | T.Opaque | T.TError _ -> Opaque
+  | T.Union _ | T.Opaque | T.TDeclError _ -> Opaque
 
 (** Compute which input parameters should be implicit or explicit.
 
@@ -813,6 +816,9 @@ let rec translate_fwd_ty (span : Meta.span option) (type_infos : type_infos)
   | TDynTrait _ ->
       craise_opt_span __FILE__ __LINE__ span
         "Dynamic trait types are not supported yet"
+  | TError _ ->
+      craise_opt_span __FILE__ __LINE__ span
+        "Found type error in the output of charon"
 
 and translate_fwd_generic_args (span : Meta.span option)
     (type_infos : type_infos) (generics : T.generic_args) : generic_args =
@@ -931,6 +937,9 @@ let rec translate_back_ty (span : Meta.span option) (type_infos : type_infos)
   | TDynTrait _ ->
       craise_opt_span __FILE__ __LINE__ span
         "Dynamic trait types are not supported yet"
+  | TError _ ->
+      craise_opt_span __FILE__ __LINE__ span
+        "Found type error in the output of charon"
 
 (** Simply calls [translate_back_ty] *)
 let ctx_translate_back_ty (ctx : bs_ctx) (keep_region : 'r -> bool)

src/symbolic/SymbolicToPure.ml

@@ -92,7 +92,7 @@ let synthesize_symbolic_expansion (span : Meta.span) (sv : symbolic_value)
         | _ -> craise __FILE__ __LINE__ span "Ill-formed borrow expansion")
     | TVar _
     | TLiteral TChar
-    | TNever | TTraitType _ | TArrow _ | TRawPtr _ | TDynTrait _ ->
+    | TNever | TTraitType _ | TArrow _ | TRawPtr _ | TDynTrait _ | TError _ ->
         craise __FILE__ __LINE__ span "Ill-formed symbolic expansion"
   in
   Expansion (place, sv, expansion)