Update charon

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.
-13502d2f3bd477ee86acafe5974016dc7707db83
+597fe150c3952fd197e37bc7b5ae2cb2f0d07c81

compiler/FunsAnalysis.ml

@@ -104,8 +104,15 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t)
 
           method! visit_rvalue _env rv =
             match rv with
-            | Use _ | RvRef _ | Global _ | Discriminant _ | Aggregate _ | Len _
-              -> ()
+            | Use _
+            | RvRef _
+            | Global _
+            | Discriminant _
+            | Aggregate _
+            | Len _
+            | NullaryOp _
+            | RawPtr _
+            | ShallowInitBox _ -> ()
             | UnaryOp (uop, _) -> can_fail := unop_can_fail uop || !can_fail
             | BinaryOp (bop, _, _) ->
                 can_fail := binop_can_fail bop || !can_fail

compiler/InterpreterExpressions.ml

@@ -862,6 +862,9 @@ let eval_rvalue_not_global (config : config) (span : Meta.span)
          AST"
   | Global _ -> craise __FILE__ __LINE__ span "Unreachable"
   | Len _ -> craise __FILE__ __LINE__ span "Unhandled Len"
+  | _ ->
+      craise __FILE__ __LINE__ span
+        ("Unsupported operation: " ^ Print.EvalCtx.rvalue_to_string ctx rvalue)
 
 let eval_fake_read (config : config) (span : Meta.span) (p : place) : cm_fun =
  fun ctx ->

compiler/InterpreterStatements.ml

@@ -952,18 +952,22 @@ and eval_statement_raw (config : config) (st : statement) : stl_cm_fun =
                   | Global _ -> craise __FILE__ __LINE__ st.span "Unreachable"
                   | Len _ ->
                       craise __FILE__ __LINE__ st.span "Len is not handled yet"
+                  | ShallowInitBox _ ->
+                      craise __FILE__ __LINE__ st.span "ShallowInitBox"
                   | Use _
                   | RvRef (_, (BShared | BMut | BTwoPhaseMut | BShallow))
-                  | UnaryOp _ | BinaryOp _ | Discriminant _ | Aggregate _ ->
+                  | NullaryOp _
+                  | UnaryOp _
+                  | BinaryOp _
+                  | Discriminant _
+                  | Aggregate _
+                  | RawPtr _ ->
+                      let p = S.mk_mplace st.span p ctx in
                       let rp = rvalue_get_place rvalue in
                       let rp =
-                        match rp with
-                        | Some rp -> Some (S.mk_mplace st.span rp ctx)
-                        | None -> None
+                        Option.map (fun rp -> S.mk_mplace st.span rp ctx) rp
                       in
-                      S.synthesize_assignment ctx
-                        (S.mk_mplace st.span p ctx)
-                        rv rp
+                      S.synthesize_assignment ctx p rv rp
                 in
                 let ctx, cc =
                   comp cc (assign_to_place config st.span rv p ctx)

compiler/InterpreterUtils.ml

@@ -293,8 +293,14 @@ let rvalue_get_place (rv : rvalue) : place option =
   match rv with
   | Use (Copy p | Move p) -> Some p
   | Use (Constant _) -> None
-  | Len (p, _, _) | RvRef (p, _) -> Some p
-  | UnaryOp _ | BinaryOp _ | Global _ | Discriminant _ | Aggregate _ -> None
+  | Len (p, _, _) | RvRef (p, _) | RawPtr (p, _) -> Some p
+  | NullaryOp _
+  | UnaryOp _
+  | BinaryOp _
+  | Global _
+  | Discriminant _
+  | Aggregate _ -> None
+  | ShallowInitBox _ -> failwith "ShallowInitBox"
 
 (** See {!ValuesUtils.symbolic_value_has_borrows} *)
 let symbolic_value_has_borrows (ctx : eval_ctx) (sv : symbolic_value) : bool =

compiler/Print.ml

@@ -613,6 +613,10 @@ module EvalCtx = struct
     let env = eval_ctx_to_fmt_env ctx in
     operand_to_string env op
 
+  let rvalue_to_string (ctx : eval_ctx) (rval : rvalue) : string =
+    let env = eval_ctx_to_fmt_env ctx in
+    rvalue_to_string env rval
+
   let call_to_string (ctx : eval_ctx) (call : call) : string =
     let env = eval_ctx_to_fmt_env ctx in
     call_to_string env "" call

compiler/SymbolicToPure.ml

@@ -2325,7 +2325,7 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
             let dest = mk_typed_pattern_from_var dest dest_mplace in
             (ctx, Unop (Neg int_ty), effect_info, args, dest)
         | _ -> craise __FILE__ __LINE__ ctx.span "Unreachable")
-    | S.Unop (E.Cast cast_kind) -> (
+    | S.Unop (E.Cast cast_kind) -> begin
         match cast_kind with
         | CastScalar (src_ty, tgt_ty) ->
             (* Note that cast can fail *)
@@ -2344,7 +2344,12 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
         | CastFnPtr _ ->
             craise __FILE__ __LINE__ ctx.span "TODO: function casts"
         | CastUnsize _ ->
-            craise __FILE__ __LINE__ ctx.span "TODO: unsize coercions")
+            craise __FILE__ __LINE__ ctx.span "TODO: unsize coercions"
+        | CastRawPtr _ ->
+            craise __FILE__ __LINE__ ctx.span "Unsupported: raw ptr casts"
+        | CastTransmute _ ->
+            craise __FILE__ __LINE__ ctx.span "Unsupported: transmute"
+      end
     | S.Binop binop -> (
         match args with
         | [ arg0; arg1 ] ->