Bump Charon and Obol

.github/workflows/ci.yml

@@ -19,7 +19,7 @@ concurrency:
 
 env:
   OBOL_REPO: soteria-tools/obol
-  OBOL_COMMIT_HASH: 3dbf5acb55ede0c2efe8648cd07e06d4830a12f4
+  OBOL_COMMIT_HASH: bf524f4242a874d716ab3964dd344cda833ba3f8
 
 jobs:
   build:

soteria-rust.opam

@@ -52,6 +52,6 @@ build: [
 ]
 dev-repo: "git+https://github.com/soteria-tools/soteria.git"
 pin-depends: [
-  ["name_matcher_parser.~dev" "git+https://github.com/soteria-tools/charon#dc438b20ff10b213dc8c5c9917e575e030af3db0"]
-  ["charon.~dev" "git+https://github.com/soteria-tools/charon#dc438b20ff10b213dc8c5c9917e575e030af3db0"]
+  ["name_matcher_parser.~dev" "git+https://github.com/soteria-tools/charon#c85ee4ec891be10fdb4c57dc30a1c9356c0d556a"]
+  ["charon.~dev" "git+https://github.com/soteria-tools/charon#c85ee4ec891be10fdb4c57dc30a1c9356c0d556a"]
 ]

soteria-rust.opam.template

@@ -1,4 +1,4 @@
 pin-depends: [
-  ["name_matcher_parser.~dev" "git+https://github.com/soteria-tools/charon#dc438b20ff10b213dc8c5c9917e575e030af3db0"]
-  ["charon.~dev" "git+https://github.com/soteria-tools/charon#dc438b20ff10b213dc8c5c9917e575e030af3db0"]
+  ["name_matcher_parser.~dev" "git+https://github.com/soteria-tools/charon#c85ee4ec891be10fdb4c57dc30a1c9356c0d556a"]
+  ["charon.~dev" "git+https://github.com/soteria-tools/charon#c85ee4ec891be10fdb4c57dc30a1c9356c0d556a"]
 ]

soteria-rust/lib/builtins/intrinsics_impl.ml

@@ -615,9 +615,9 @@ module M (Rust_state_m : Rust_state_m.S) :
       (layout.size, layout.align)
     else
       match (t, meta) with
-      | TAdt { id = TBuiltin (TSlice | TStr); _ }, (Thin | VTable _) ->
+      | (TSlice _ | TAdt { id = TBuiltin TStr; _ }), (Thin | VTable _) ->
           failwith "size_and_align_of_val: Invalid metadata for slice type"
-      | TAdt { id = TBuiltin (TSlice | TStr); _ }, Len meta ->
+      | (TSlice _ | TAdt { id = TBuiltin TStr; _ }), Len meta ->
           let sub_ty = Layout.dst_slice_ty t in
           let* sub_ty =
             of_opt_not_impl "size_of_val: missing a DST slice type" sub_ty

soteria-rust/lib/builtins/rusteria.ml

@@ -48,8 +48,7 @@ module M (Rust_state_m : Rust_state_m.S) = struct
     let+ () = assume [ Typed.BitVec.to_bool to_assume ] in
     unit_
 
-  let nondet (fun_sig : Charon.UllbcAst.fun_sig) _ =
-    Layout.nondet fun_sig.output
+  let nondet (fun_sig : Charon.Types.fun_sig) _ = Layout.nondet fun_sig.output
 
   let panic ?msg args =
     let* msg =

soteria-rust/lib/charon_util.ml

@@ -39,26 +39,22 @@ let rec pp_ty fmt : Types.ty -> unit = function
   | TAdt { id = TBuiltin TBox; generics = { types = [ ty ]; _ } } ->
       Fmt.pf fmt "Box<%a>" pp_ty ty
   | TAdt { id = TBuiltin TBox; _ } -> Fmt.string fmt "Box<?>"
-  | TAdt
-      {
-        id = TBuiltin TArray;
-        generics =
-          { types = [ ty ]; const_generics = [ CgValue (VScalar len) ]; _ };
-      } ->
+  | TArray (ty, CgValue (VScalar len)) ->
       Fmt.pf fmt "[%a; %a]" pp_ty ty Z.pp_print (z_of_scalar len)
-  | TAdt { id = TBuiltin TArray; _ } -> Fmt.string fmt "[?; ?]"
-  | TAdt { id = TBuiltin TSlice; generics = { types = [ ty ]; _ } } ->
-      Fmt.pf fmt "[%a]" pp_ty ty
-  | TAdt { id = TBuiltin TSlice; _ } -> Fmt.string fmt "[?]"
+  | TArray (ty, _) -> Fmt.pf fmt "[%a; ?]" pp_ty ty
+  | TSlice ty -> Fmt.pf fmt "[%a]" pp_ty ty
   | TAdt { id = TBuiltin TStr; _ } -> Fmt.string fmt "str"
   | TLiteral lit -> pp_literal_ty fmt lit
   | TNever -> Fmt.string fmt "!"
   | TRef (_, ty, RMut) -> Fmt.pf fmt "&mut %a" pp_ty ty
   | TRef (_, ty, RShared) -> Fmt.pf fmt "&%a" pp_ty ty
   | TRawPtr (ty, RMut) -> Fmt.pf fmt "*mut %a" pp_ty ty
   | TRawPtr (ty, RShared) -> Fmt.pf fmt "*const %a" pp_ty ty
-  | TFnPtr { binder_value = ins, out; _ } ->
-      Fmt.pf fmt "fn (%a) -> %a" Fmt.(list ~sep:(any ", ") pp_ty) ins pp_ty out
+  | TFnPtr { binder_value = { inputs; output; is_unsafe }; _ } ->
+      Fmt.pf fmt "%sfn (%a) -> %a"
+        (if is_unsafe then "unsafe " else "")
+        Fmt.(list ~sep:(any ", ") pp_ty)
+        inputs pp_ty output
   | TDynTrait _ -> Fmt.string fmt "dyn <trait>"
   | TTraitType (_, name) -> Fmt.pf fmt "Trait<?>::%s" name
   | TFnDef { binder_value = { kind = FunId (FRegular fid); _ }; _ } ->
@@ -116,17 +112,7 @@ let fields_of_tys : Types.ty list -> Types.field list =
       })
 
 let mk_array_ty ty len : Types.ty =
-  TAdt
-    {
-      id = TBuiltin TArray;
-      generics =
-        {
-          types = [ ty ];
-          const_generics = [ CgValue (VScalar (UnsignedScalar (Usize, len))) ];
-          regions = [];
-          trait_refs = [];
-        };
-    }
+  TArray (ty, CgValue (VScalar (UnsignedScalar (Usize, len))))
 
 (** The type [*const ()] *)
 let unit_ptr = Types.TRawPtr (TypesUtils.mk_unit_ty, RShared)
@@ -172,6 +158,7 @@ let pp_span_data ft ({ file; beg_loc; end_loc } : Meta.span_data) =
     match name with
     | Local name -> Fmt.string ft (clean_filename name)
     | Virtual name -> Fmt.pf ft "%s (virtual)" (clean_filename name)
+    | NotReal name -> Fmt.pf ft "%s (synthetic)" (clean_filename name)
   in
   let pp_range ft ((start, stop) : Meta.loc * Meta.loc) =
     if start.line = stop.line then

soteria-rust/lib/crate.ml

@@ -29,14 +29,15 @@ let[@inline] mk_pp_indent to_string =
   let to_str = to_string (as_fmt_env ()) "" in
   Fmt.pf ft "%s" (to_str v)
 
-let pp_name = mk_pp PrintTypes.name_to_string
-let pp_statement = mk_pp_indent PrintUllbcAst.Ast.statement_to_string
-let pp_terminator = mk_pp_indent PrintUllbcAst.Ast.terminator_to_string
+let pp_constant_expr = mk_pp PrintExpressions.constant_expr_to_string
 let pp_fn_operand = mk_pp PrintUllbcAst.Ast.fn_operand_to_string
 let pp_fun_decl_ref = mk_pp PrintTypes.fun_decl_ref_to_string
 let pp_generic_args = mk_pp PrintTypes.generic_args_to_string
 let pp_global_decl_ref = mk_pp PrintTypes.global_decl_ref_to_string
+let pp_name = mk_pp PrintTypes.name_to_string
 let pp_place = mk_pp PrintExpressions.place_to_string
+let pp_statement = mk_pp_indent PrintUllbcAst.Ast.statement_to_string
+let pp_terminator = mk_pp_indent PrintUllbcAst.Ast.terminator_to_string
 
 let get_adt id =
   let crate = get_crate () in

soteria-rust/lib/encoder.ml

@@ -123,18 +123,10 @@ module Make (Sptr : Sptr.S) = struct
       @@
       match ty with
       | TAdt { id = TTuple; generics = { types; _ } } -> Iter.of_list types
-      | TAdt
-          {
-            id = TBuiltin TArray;
-            generics = { types = [ ty ]; const_generics = [ len ]; _ };
-          } ->
-          Iter.repeatz (z_of_const_generic len) ty
-      | TAdt { id = TBuiltin ((TStr | TSlice) as kind); generics } -> (
+      | TArray (ty, len) -> Iter.repeatz (z_of_const_generic len) ty
+      | TSlice _ | TAdt { id = TBuiltin TStr; _ } -> (
           let sub_ty =
-            match kind with
-            | TSlice -> List.hd generics.types
-            | TStr -> TLiteral (TUInt U8)
-            | _ -> failwith "unreachable"
+            match ty with TSlice ty -> ty | _ -> TLiteral (TUInt U8)
           in
           match meta with
           | Len len when Option.is_some (BV.to_z len) ->

soteria-rust/lib/frontend.ml

@@ -508,7 +508,7 @@ module Diagnostic = struct
             ?content:span.file.contents file (to_loc span.beg_loc)
             (to_loc span.end_loc);
         ]
-    | Virtual _ -> []
+    | Virtual _ | NotReal _ -> []
 
   let print_diagnostic ~fname ~call_trace ~error =
     Soteria.Terminal.Diagnostic.print_diagnostic ~call_trace ~as_ranges

soteria-rust/lib/interp.ml

@@ -252,6 +252,10 @@ module Make (State : State_intf.S) = struct
         in
         Union blocks
     | COpaque msg -> Fmt.kstr not_impl "Opaque constant: %s" msg
+    | CAdt _ | CArray _ | CSlice _ | CGlobal _ | CRef _ | CPtr _ | CFnPtr _
+    | CPtrNoProvenance _ ->
+        Fmt.kstr not_impl "TODO: complex constant %a" Crate.pp_constant_expr
+          const
     | CVar _ -> not_impl "TODO: resolve const Var (mono error)"
 
   (** Resolves a place to a pointer *)
@@ -315,14 +319,8 @@ module Make (State : State_intf.S) = struct
         let len =
           match (meta, base.ty) with
           (* Array with static size *)
-          | ( Thin,
-              TAdt
-                {
-                  id = TBuiltin TArray;
-                  generics = { const_generics = [ len ]; _ };
-                } ) ->
-              BV.usize_of_const_generic len
-          | Len len, TAdt { id = TBuiltin TSlice; _ } -> Typed.cast_i Usize len
+          | Thin, TArray (_, len) -> BV.usize_of_const_generic len
+          | Len len, TSlice _ -> Typed.cast_i Usize len
           | _ -> Fmt.failwith "Index projection: unexpected arguments"
         in
         let* idx = eval_operand idx in
@@ -341,17 +339,8 @@ module Make (State : State_intf.S) = struct
         let ty, len =
           match (meta, base.ty) with
           (* Array with static size *)
-          | ( Thin,
-              TAdt
-                {
-                  id = TBuiltin TArray;
-                  generics = { const_generics = [ len ]; types = [ ty ]; _ };
-                } ) ->
-              (ty, BV.usize_of_const_generic len)
-          | ( Len len,
-              TAdt { id = TBuiltin TSlice; generics = { types = [ ty ]; _ } } )
-            ->
-              (ty, Typed.cast len)
+          | Thin, TArray (ty, len) -> (ty, BV.usize_of_const_generic len)
+          | Len len, TSlice ty -> (ty, Typed.cast len)
           | _ -> Fmt.failwith "Index projection: unexpected arguments"
         in
         let* from = eval_operand from in
@@ -563,29 +552,29 @@ module Make (State : State_intf.S) = struct
               match meta with
               | MetaLength length ->
                   ok @@ Len (BV.usize_of_const_generic length)
-              | MetaVTableDirect (_, glob) ->
+              | MetaVTable (_, glob) ->
                   (* the global adds one level of indirection *)
                   let* glob = of_opt_not_impl "Missing VTable global" glob in
                   let* ptr = resolve_global glob in
                   let+ vtable = State.load ptr unit_ptr in
                   let vtable, _ = as_ptr vtable in
                   VTable vtable
-              (* We don't check validity of the metadata if the unsizing
-                  doesn't need to modify the VTable. *)
-              | MetaVTableNested (_, None) -> ok prev
-              | MetaVTableNested (_, Some field) -> (
+              | MetaVTableUpcast fields -> (
                   match prev with
                   | Thin -> failwith "Unsizing VTable with no meta?"
                   | Len _ -> error `UBDanglingPointer
                   | VTable vt ->
-                      let idx = Types.FieldId.to_int field in
-                      let* vt_addr =
-                        Sptr.offset ~ty:unit_ptr ~signed:false vt
-                          (BV.usizei idx)
+                      let+ vt' =
+                        fold_list fields ~init:vt ~f:(fun vt field ->
+                            let idx = Types.FieldId.to_int field in
+                            let* vt_addr =
+                              Sptr.offset ~ty:unit_ptr ~signed:false vt
+                                (BV.usizei idx)
+                            in
+                            let+ vt = State.load (vt_addr, Thin) unit_ptr in
+                            fst (as_ptr vt))
                       in
-                      let+ vt = State.load (vt_addr, Thin) unit_ptr in
-                      let vt, _ = as_ptr vt in
-                      VTable vt)
+                      VTable vt')
               | MetaUnknown ->
                   Fmt.kstr not_impl "Unsupported metadata in CastUnsize: %a"
                     Expressions.pp_unsizing_metadata meta

soteria-rust/lib/layout.ml

@@ -113,7 +113,7 @@ let empty_generics = TypesUtils.empty_generic_args
 type meta_kind = LenKind | VTableKind | NoneKind
 
 let rec dst_kind : Types.ty -> meta_kind = function
-  | TAdt { id = TBuiltin TStr; _ } | TAdt { id = TBuiltin TSlice; _ } -> LenKind
+  | TAdt { id = TBuiltin TStr; _ } | TSlice _ -> LenKind
   | TDynTrait _ -> VTableKind
   | TAdt { id = TAdtId id; _ } when Crate.is_struct id -> (
       match List.last_opt (Crate.as_struct id) with
@@ -125,8 +125,7 @@ let rec dst_kind : Types.ty -> meta_kind = function
     element. *)
 let rec dst_slice_ty : Types.ty -> Types.ty option = function
   | TAdt { id = TBuiltin TStr; _ } -> Some (TLiteral (TUInt U8))
-  | TAdt { id = TBuiltin TSlice; generics = { types = [ sub_ty ]; _ } } ->
-      Some sub_ty
+  | TSlice sub_ty -> Some sub_ty
   | TAdt { id = TAdtId id; _ } when Crate.is_struct id -> (
       match List.last_opt (Crate.as_struct id) with
       | None -> None
@@ -184,11 +183,8 @@ let rec layout_of (ty : Types.ty) : (t, 'e, 'f) Rustsymex.Result.t =
      the tail in a DST struct.
      FIXME: Maybe we should mark the layout as a DST, and ensure a DST layout's size is never
      used for an allocation. *)
-  | TAdt { id = TBuiltin (TStr as ty); generics }
-  | TAdt { id = TBuiltin (TSlice as ty); generics } ->
-      let sub_ty =
-        if ty = TSlice then List.hd generics.types else TLiteral (TUInt U8)
-      in
+  | TAdt { id = TBuiltin TStr; _ } | TSlice _ ->
+      let sub_ty = match ty with TSlice ty -> ty | _ -> TLiteral (TUInt U8) in
       let++ sub_layout = layout_of sub_ty in
       mk ~size:(BV.usizei 0) ~align:sub_layout.align
         ~fields:(Array sub_layout.size) ()
@@ -207,14 +203,12 @@ let rec layout_of (ty : Types.ty) : (t, 'e, 'f) Rustsymex.Result.t =
       | _, Enum variants -> compute_enum_layout ty variants
       | _, (Opaque | TDeclError _ | Alias _) -> not_impl_layout "unexpected" ty)
   (* Arrays *)
-  | TAdt { id = TBuiltin TArray; generics } ->
+  | TArray (subty, size) ->
       let max_array_len sub_size =
         (* We calculate the max array size for a 32bit architecture, like Miri does. *)
         let isize_bits = 32 - 1 in
         BV.usize Z.(one lsl isize_bits) /@ Typed.cast sub_size
       in
-      let size = List.hd generics.const_generics in
-      let subty = List.hd generics.types in
       let len = BV.of_const_generic size in
       let** sub_layout = layout_of subty in
       let++ () =
@@ -497,11 +491,7 @@ let rec nondet : Types.ty -> ('a rust_val, 'e, 'f) Result.t =
   | TAdt { id = TTuple; generics = { types; _ } } ->
       let++ fields = nondets types in
       Tuple fields
-  | TAdt
-      {
-        id = TBuiltin TArray;
-        generics = { const_generics = [ len ]; types = [ ty ]; _ };
-      } ->
+  | TArray (ty, len) ->
       let size = Charon_util.int_of_const_generic len in
       let++ fields = nondets @@ List.init size (fun _ -> ty) in
       Tuple fields
@@ -573,9 +563,7 @@ let rec as_zst : Types.ty -> 'a rust_val option =
   let as_zsts tys = Monad.OptionM.all as_zst tys in
   function
   | TNever -> Some (Tuple [])
-  | TAdt { id = TBuiltin TArray; generics = { const_generics = [ len ]; _ } }
-    when int_of_const_generic len = 0 ->
-      Some (Tuple [])
+  | TArray (_, len) when z_of_const_generic len = Z.zero -> Some (Tuple [])
   | TAdt { id = TAdtId id; _ } -> (
       let adt = Crate.get_adt id in
       match adt.kind with
@@ -628,9 +616,7 @@ let rec is_unsafe_cell : Types.ty -> bool = function
             @@ Iter.flat_map_l (fun (v : Types.variant) -> field_tys v.fields)
             @@ Iter.of_list vs
         | _ -> false)
-  | TAdt { id = TBuiltin (TArray | TSlice); generics = { types = [ ty ]; _ } }
-    ->
-      is_unsafe_cell ty
+  | TArray (ty, _) | TSlice ty -> is_unsafe_cell ty
   | TAdt { id = TTuple; generics = { types; _ } } ->
       List.exists is_unsafe_cell types
   | _ -> false
@@ -650,9 +636,7 @@ let rec ref_tys_in ?(include_ptrs = false) (v : 'a rust_val) (ty : Types.ty) :
   | Tuple vs, TAdt { id = TAdtId adt_id; _ } ->
       let fields = Crate.as_struct adt_id in
       List.concat_map2 f vs (field_tys fields)
-  | ( Tuple vs,
-      TAdt { id = TBuiltin (TArray | TSlice); generics = { types = [ ty ]; _ } }
-    ) ->
+  | Tuple vs, (TArray (ty, _) | TSlice ty) ->
       List.concat_map (fun v -> f v ty) vs
   | Tuple vs, TAdt { id = TTuple; generics = { types; _ } } ->
       List.concat_map2 f vs types
@@ -712,9 +696,7 @@ let rec update_ref_tys_in
       let fields = Crate.as_struct adt_id in
       let++ vs, acc = fs2 init vs (field_tys fields) in
       (Tuple vs, acc)
-  | ( Tuple vs,
-      TAdt { id = TBuiltin (TArray | TSlice); generics = { types = [ ty ]; _ } }
-    ) ->
+  | Tuple vs, (TArray (ty, _) | TSlice ty) ->
       let++ vs, acc = fs init vs ty in
       (Tuple vs, acc)
   | Tuple vs, TAdt { id = TTuple; generics = { types; _ } } ->