diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 211fef6ef..67dc6f02a 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -19,7 +19,7 @@ concurrency: env: OBOL_REPO: soteria-tools/obol - OBOL_COMMIT_HASH: e34fe507a4be3fbec04be0c31b2c951bc2ddc904 + OBOL_COMMIT_HASH: 3dbf5acb55ede0c2efe8648cd07e06d4830a12f4 jobs: build: diff --git a/soteria-rust/lib/builtins/intrinsics_impl.ml b/soteria-rust/lib/builtins/intrinsics_impl.ml index f36f5db19..cf93d51fb 100644 --- a/soteria-rust/lib/builtins/intrinsics_impl.ml +++ b/soteria-rust/lib/builtins/intrinsics_impl.ml @@ -43,16 +43,6 @@ module M (Rust_state_m : Rust_state_m.S) : let mul_with_overflow = checked_op (Mul OUB) let align_of ~t = Layout.align_of t - let align_of_val ~t ~ptr = - match (t, ptr) with - | Types.TDynTrait _, (_, VTable vt) -> - let* align_ptr = - Sptr.offset ~signed:false ~ty:(TLiteral (TUInt Usize)) vt Usize.(2s) - in - let+ align = State.load (align_ptr, Thin) (TLiteral (TUInt Usize)) in - as_base_i Usize align - | _ -> Layout.align_of t - let arith_offset ~t ~dst:(dst, meta) ~offset = let+ dst' = Sptr.offset ~signed:true ~check:false ~ty:t dst offset in (dst', meta) @@ -617,39 +607,71 @@ module M (Rust_state_m : Rust_state_m.S) : let saturating_sub = saturating (Sub OUB) let size_of ~t = Layout.size_of t + let rec size_and_align_of_val ~t ~meta = + (* Takes inspiration from rustc, to calculate the size and alignment of DSTs. + https://github.com/rust-lang/rust/blob/a8664a1534913ccff491937ec2dc7ec5d973c2bd/compiler/rustc_codegen_ssa/src/size_of_val.rs *) + if not (Layout.is_dst t) then + let+ layout = Layout.layout_of t in + (layout.size, layout.align) + else + match (t, meta) with + | TAdt { id = TBuiltin (TSlice | TStr); _ }, (Thin | VTable _) -> + failwith "size_and_align_of_val: Invalid metadata for slice type" + | TAdt { id = TBuiltin (TSlice | 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 + in + let* layout = Layout.layout_of sub_ty in + let len = Typed.cast_i Usize meta in + let size, ovf_mul = layout.size *?@ len in + let+ () = State.assert_not ovf_mul `Overflow in + (size, layout.align) + | TDynTrait _, (Thin | Len _) -> + failwith "size_and_align_of_val: Invalid metadata for dyn type" + | TDynTrait _, VTable vtable -> + let usize = Types.TLiteral (TUInt Usize) in + let* size_ptr = + Sptr.offset ~signed:true ~ty:usize vtable Usize.(1s) + in + let* align_ptr = + Sptr.offset ~signed:true ~ty:usize vtable Usize.(2s) + in + let* size = State.load (size_ptr, Thin) usize in + let+ align = State.load (align_ptr, Thin) usize in + let size = as_base_i Usize size in + let align = as_base_i Usize align in + (size, Typed.cast align) + | TAdt { id = TTuple | TAdtId _; _ }, _ -> + let field_tys = + match t with + | TAdt { id = TAdtId id; _ } -> Crate.as_struct id |> field_tys + | TAdt { id = TTuple; generics = { types; _ } } -> types + | _ -> failwith "impossible" + in + let last_field_ty = List.last field_tys in + let* layout = Layout.layout_of t in + let last_field_ofs = + match layout.fields with + | Arbitrary (_, offsets) -> offsets.(Array.length offsets - 1) + | _ -> failwith "size_and_align_of_val: Unexpected layout for ADT" + in + let+ unsized_size, unsized_align = + size_and_align_of_val ~t:last_field_ty ~meta + in + let align = BV.max ~signed:false unsized_align layout.align in + let size = last_field_ofs +!!@ unsized_size in + let size = Layout.size_to_fit ~size ~align in + (size, align) + | _ -> not_impl "size_and_align_of_val: Unexpected type" + let size_of_val ~t ~ptr:(_, meta) = - (* for DSTs, the size of the type is the size of all non-DST fields, - to which we just need to add the size of the DST part. *) - let* base_size = Layout.size_of t in - match meta with - | Len meta -> ( - let sub_ty = Layout.dst_slice_ty t in - match sub_ty with - | None -> ok base_size - | Some sub_ty -> - let len = Typed.cast_i Usize meta in - let* size = Layout.size_of sub_ty in - let size, ovf_mul = size *?@ len in - let size, ovf_add = base_size +?@ size in - let+ () = State.assert_not (ovf_mul ||@ ovf_add) `Overflow in - size) - | VTable vt -> - let* size_ptr = - Sptr.offset ~signed:false ~ty:(TLiteral (TUInt Usize)) vt Usize.(1s) - in - let* dyn_size = State.load (size_ptr, Thin) (TLiteral (TUInt Usize)) in - let dyn_size = as_base_i Usize dyn_size in - let size = base_size +!@ dyn_size in - (* e.g. if alignment of outer container is 8, but dyn size is 1, the added size is 8. - the real computation is a lot more complicated, but this does the trick for general use. - https://github.com/rust-lang/rust/blob/a8664a1534913ccff491937ec2dc7ec5d973c2bd/compiler/rustc_codegen_ssa/src/size_of_val.rs *) - let+ align = Layout.align_of t in - let rem = size %@ align in - let size = - Typed.ite (rem ==@ Usize.(0s)) size (size +!@ (align -!@ rem)) - in - size - | _ -> ok base_size + let+ size, _ = size_and_align_of_val ~t ~meta in + size + + let align_of_val ~t ~ptr:(_, meta) = + let+ _, align = size_and_align_of_val ~t ~meta in + (align :> T.sint Typed.t) let transmute ~t_src ~dst ~src = Core.transmute ~from_ty:t_src ~to_ty:dst src diff --git a/soteria-rust/lib/encoder.ml b/soteria-rust/lib/encoder.ml index e6488185e..271bea57a 100644 --- a/soteria-rust/lib/encoder.ml +++ b/soteria-rust/lib/encoder.ml @@ -263,66 +263,61 @@ module Make (Sptr : Sptr.S) = struct offset, using the provided metadata for DSTs, and returns the associated [Rust_val]. This does not perform any validity checking, aside from erroring if the type is uninhabited. *) - let decode ~meta ~offset : - Types.ty -> (rust_val, 'state, 'e, 'fix) ParserMonad.t = + let rec decode ~meta ~offset ty : (rust_val, 'state, 'e, 'fix) ParserMonad.t = let open ParserMonad in let open ParserMonad.Syntax in - let module T = Typed.T in - (* Base case, parses all types. *) - let rec aux offset ty : (rust_val, 'state, 'e, 'fix) ParserMonad.t = - let* layout = layout_of ty in - match (layout.fields, ty) with - | _, TDynTrait _ -> not_impl "Tried reading a trait object?" - | _, TAdt { id = TAdtId id; _ } when Crate.is_union id -> - if%sat layout.size ==@ Usize.(0s) then ok (Union []) - else - (* FIXME: this isn't exactly correct; union actually doesn't copy the padding - bytes (i.e. the intersection of the padding bytes of all fields). It is - quite painful to actually calculate these padding bytes so we just copy - the whole thing for now. - See https://github.com/rust-lang/unsafe-code-guidelines/issues/518 - And a proper implementation is here: - https://github.com/minirust/minirust/blob/master/tooling/minimize/src/chunks.rs *) - let+ blocks = get_all (Typed.cast layout.size, offset) in - Union blocks - | Primitive, TNever -> error `RefToUninhabited - | Primitive, TFnDef fnptr -> ok (ConstFn fnptr.binder_value) - | Primitive, _ -> query (ty, offset) - | Array _, (TRawPtr (pointee, _) | TRef (_, pointee, _)) -> ( - let+ vs = iter (iter_fields ~meta layout ty) offset in - let vs = as_tuple vs in - match (dst_kind pointee, vs) with - | LenKind, [ Ptr (base, Thin); Int len ] -> Ptr (base, Len len) - | VTableKind, [ Ptr (base, Thin); Ptr (vtable, Thin) ] -> - Ptr (base, VTable vtable) - | _ -> failwith "decode: invalid metadata for pointer type") - | Array _, _ -> iter (iter_fields ~meta layout ty) offset - | Arbitrary (variant, _), _ -> ( - let+ vs = iter (iter_fields ~meta layout ty) offset in - match ty with - | TAdt { id = TAdtId t_id; _ } when Crate.is_enum t_id -> - let variants = Crate.as_enum t_id in - let variant = Types.VariantId.nth variants variant in - let fields = as_tuple vs in - let discr = BV.of_literal variant.discriminant in - Enum (discr, fields) - | _ -> vs) - | Enum _, TAdt { id = TAdtId t_id; _ } -> - let variants = Crate.as_enum t_id in - let* variant = variant_of_enum ~offset ty in - let+ fields = iter (iter_fields ~variant ~meta layout ty) offset in - let fields = as_tuple fields in - let variant = Types.VariantId.nth variants variant in - let discr = BV.of_literal variant.discriminant in - Enum (discr, fields) - | Enum _, _ -> failwith "decode: expected enum type for enum layout" - and iter fields offset = + let iter fields offset = fold_iter fields ~init:[] ~f:(fun vs (ty, o) -> - let+ v = aux (offset +!!@ o) ty in + let+ v = decode ~meta ~offset:(offset +!!@ o) ty in v :: vs) |> (Fun.flip map) (fun vs -> Tuple (List.rev vs)) in - aux offset + let* layout = layout_of ty in + match (layout.fields, ty) with + | _ when layout.uninhabited -> error `RefToUninhabited + | _, TDynTrait _ -> not_impl "Tried reading a trait object?" + | _, TAdt { id = TAdtId id; _ } when Crate.is_union id -> + if%sat layout.size ==@ Usize.(0s) then ok (Union []) + else + (* FIXME: this isn't exactly correct; union actually doesn't copy the + padding bytes (i.e. the intersection of the padding bytes of all + fields). It is quite painful to actually calculate these padding + bytes so we just copy the whole thing for now. + See https://github.com/rust-lang/unsafe-code-guidelines/issues/518 + And a proper implementation is here: + https://github.com/minirust/minirust/blob/master/tooling/minimize/src/chunks.rs *) + let+ blocks = get_all (Typed.cast layout.size, offset) in + Union blocks + | Primitive, TFnDef fnptr -> ok (ConstFn fnptr.binder_value) + | Primitive, _ -> query (ty, offset) + | Array _, (TRawPtr (pointee, _) | TRef (_, pointee, _)) -> ( + let+ vs = iter (iter_fields ~meta layout ty) offset in + let vs = as_tuple vs in + match (dst_kind pointee, vs) with + | LenKind, [ Ptr (base, Thin); Int len ] -> Ptr (base, Len len) + | VTableKind, [ Ptr (base, Thin); Ptr (vtable, Thin) ] -> + Ptr (base, VTable vtable) + | _ -> failwith "decode: invalid metadata for pointer type") + | Array _, _ -> iter (iter_fields ~meta layout ty) offset + | Arbitrary (variant, _), _ -> ( + let+ vs = iter (iter_fields ~meta layout ty) offset in + match ty with + | TAdt { id = TAdtId t_id; _ } when Crate.is_enum t_id -> + let variants = Crate.as_enum t_id in + let variant = Types.VariantId.nth variants variant in + let fields = as_tuple vs in + let discr = BV.of_literal variant.discriminant in + Enum (discr, fields) + | _ -> vs) + | Enum _, TAdt { id = TAdtId t_id; _ } -> + let variants = Crate.as_enum t_id in + let* variant = variant_of_enum ~offset ty in + let+ fields = iter (iter_fields ~variant ~meta layout ty) offset in + let fields = as_tuple fields in + let variant = Types.VariantId.nth variants variant in + let discr = BV.of_literal variant.discriminant in + Enum (discr, fields) + | Enum _, _ -> failwith "decode: expected enum type for enum layout" (** Ensures this value is valid for the given type. This includes checking pointer metadata, e.g. slice lengths and vtables. The [fake_read] function @@ -345,8 +340,11 @@ module Make (Sptr : Sptr.S) = struct (* TODO: check the vtable pointer is of the right trait kind *) ok () in - let* opt_err, st = fake_read p pointee st in - match opt_err with Some err -> error err | None -> ok st) + let** layout = Layout.layout_of pointee in + if layout.uninhabited then error `RefToUninhabited + else + let* opt_err, st = fake_read p pointee st in + match opt_err with Some err -> error err | None -> ok st) | Ptr (p, _), TFnPtr _ -> let++ () = assert_or_error diff --git a/soteria-rust/lib/layout.ml b/soteria-rust/lib/layout.ml index 0cb8d58c5..09bf3500c 100644 --- a/soteria-rust/lib/layout.ml +++ b/soteria-rust/lib/layout.ml @@ -75,16 +75,13 @@ module Fields_shape = struct end (* TODO: size should be an [option], for unsized types *) -(* TODO: add a uninhabited flag (concrete..?) *) type t = { size : T.sint Typed.t; align : T.nonzero Typed.t; + uninhabited : bool; fields : Fields_shape.t; } - -let pp fmt { size; align; fields } = - Format.fprintf fmt "{ size = %a;@, align = %a;@, fields = @[%a@] }" Typed.ppa - size Typed.ppa align Fields_shape.pp fields +[@@deriving show] module Session = struct type ty_key = Types.ty @@ -139,21 +136,25 @@ let rec dst_slice_ty : Types.ty -> Types.ty option = function (** If this is a dynamically sized type (requiring a fat pointer) *) let is_dst ty = dst_kind ty <> NoneKind -let size_to_fit ~size ~align = +let[@inline] size_to_fit ~size ~align = Typed.ite (size %@ align ==@ Usize.(0s)) size - (size +!@ align -!@ (size %@ align)) + (size +!!@ align -!!@ (size %@ align)) -let mk ~size ~align ?(fields : Fields_shape.t = Primitive) () = - { size; align; fields } +let mk ~size ~align ?(uninhabited = false) + ?(fields : Fields_shape.t = Primitive) () = + { size; align; uninhabited; fields } -let mk_concrete ~size ~align ?fields () = - mk ~size:(BV.usizei size) ~align:(BV.usizeinz align) ?fields () +let mk_concrete ~size ~align = + mk ~size:(BV.usizei size) ~align:(BV.usizeinz align) let not_impl_layout msg ty = Fmt.kstr not_impl "Can't compute layout: %s %a" msg pp_ty ty +let layout_warning msg ty = + L.debug (fun m -> m "⚠️ Layout: %s (%a)" msg pp_ty ty) + let rec layout_of (ty : Types.ty) : (t, 'e, 'f) Rustsymex.Result.t = Session.get_or_compute_cached_layout ty @@ fun () -> match ty with @@ -172,8 +173,9 @@ let rec layout_of (ty : Types.ty) : (t, 'e, 'f) Rustsymex.Result.t = (mk_concrete ~size:(ptr_size * 2) ~align:ptr_size ~fields:(Array (BV.usizei ptr_size)) ()) - (* Refs, pointers, boxes *) - | TAdt { id = TBuiltin TBox; _ } | TRef (_, _, _) | TRawPtr (_, _) -> + (* Refs, pointers, boxes, function pointers *) + | TAdt { id = TBuiltin TBox; _ } | TRef (_, _, _) | TRawPtr (_, _) | TFnPtr _ + -> let ptr_size = Crate.pointer_size () in ok (mk_concrete ~size:ptr_size ~align:ptr_size ()) (* Dynamically sized types -- we assume they have a size of 0. In truth, these types should @@ -193,38 +195,17 @@ let rec layout_of (ty : Types.ty) : (t, 'e, 'f) Rustsymex.Result.t = (* Same as above, but here we have even less information ! *) | TDynTrait _ -> ok (mk_concrete ~size:0 ~align:1 ()) (* Tuples *) - | TAdt { id = TTuple; generics = { types; _ } } -> layout_of_members ty types + | TAdt { id = TTuple; generics = { types; _ } } -> + compute_arbitrary_layout ty types (* Custom ADTs (struct, enum, etc.) *) | TAdt { id = TAdtId id; _ } -> ( let adt = Crate.get_adt id in - match adt.kind with - | Struct fields -> layout_of_struct ty adt fields - | Enum variants -> layout_of_enum ty adt variants - | Union fs -> - let++ layouts = - Result.fold_list (Charon_util.field_tys fs) ~init:[] - ~f:(fun acc ty -> - let++ l = layout_of ty in - l :: acc) - in - let layouts = List.rev layouts in - - let hd = List.hd layouts in - let tl = List.tl layouts in - let size, align = - List.fold_left - (fun (size, align) l -> - ( BV.max ~signed:false size l.size, - BV.max ~signed:false align l.align )) - (hd.size, hd.align) tl - in - let size = size_to_fit ~size ~align in - (* All fields in the union start at 0 and overlap *) - let fields = Array.make (List.length fs) (BV.usizei 0) in - mk ~size ~align ~fields:(Arbitrary (Types.VariantId.zero, fields)) () - | Opaque -> not_impl_layout "opaque" ty - | TDeclError _ -> not_impl_layout "decl error" ty - | Alias _ -> not_impl_layout "alias" ty) + match (adt.layout, adt.kind) with + | Some layout, _ -> translate_layout ty layout + | _, Struct fields -> compute_arbitrary_layout ty (field_tys fields) + | _, Union fields -> compute_union_layout ty (field_tys fields) + | _, Enum variants -> compute_enum_layout ty variants + | _, (Opaque | TDeclError _ | Alias _) -> not_impl_layout "unexpected" ty) (* Arrays *) | TAdt { id = TBuiltin TArray; generics } -> let max_array_len sub_size = @@ -246,13 +227,10 @@ let rec layout_of (ty : Types.ty) : (t, 'e, 'f) Rustsymex.Result.t = let size = len *!!@ sub_layout.size in mk ~size ~align:sub_layout.align ~fields:(Array sub_layout.size) () (* Never -- zero sized type *) - | TNever -> ok (mk_concrete ~size:0 ~align:1 ~fields:Primitive ()) + | TNever -> + ok (mk_concrete ~size:0 ~align:1 ~uninhabited:false ~fields:Primitive ()) (* Function definitions -- zero sized type *) | TFnDef _ -> ok (mk_concrete ~size:0 ~align:1 ~fields:Primitive ()) - (* Function pointers (can point to a function or a state-less closure). *) - | TFnPtr _ -> - let ptr_size = Crate.pointer_size () in - ok (mk_concrete ~size:ptr_size ~align:ptr_size ~fields:Primitive ()) (* Others (unhandled for now) *) | TPtrMetadata _ -> not_impl_layout "pointer metadata" ty | TVar _ -> not_impl_layout "type variable" ty @@ -261,7 +239,74 @@ let rec layout_of (ty : Types.ty) : (t, 'e, 'f) Rustsymex.Result.t = let** resolved = resolve_trait_ty tref ty_name in layout_of resolved -and layout_of_members ?fst_size ?fst_align ty members = +and translate_layout ty (layout : Types.layout) = + let size = compute_size ty layout.size in + let align = compute_align ty layout.align in + let uninhabited = layout.uninhabited in + let tag_layout = + Option.map + (fun (discr_layout : Types.discriminant_layout) : Tag_layout.t -> + let tags = + Monad.ListM.map layout.variant_layouts (fun v -> + Option.map BV.of_scalar v.tag) + in + let tags = Array.of_list tags in + let ty = lit_of_int_ty discr_layout.tag_ty in + let offset = BV.usizei discr_layout.offset in + let encoding : Tag_layout.encoding = + match discr_layout.encoding with + | Niche v -> Niche v + | Direct -> Direct + in + { offset; ty; tags; encoding }) + layout.discriminant_layout + in + let variant_layouts = + List.mapi + (fun i (v : Types.variant_layout) : Fields_shape.t -> + if v.uninhabited then Primitive + else + let ofs = Array.of_list (List.map BV.usizei v.field_offsets) in + Arbitrary (Types.VariantId.of_int i, ofs)) + layout.variant_layouts + in + let fields : Fields_shape.t = + match (tag_layout, variant_layouts) with + (* tag layouts only exist on enum layouts *) + | Some tag_layout, _ -> Enum (tag_layout, Array.of_list variant_layouts) + (* no variants, so this is uninhabited; we can use primitive *) + | None, [] -> Primitive + (* there should be only one inhabited (non-Primitive) variant *) + | None, _ -> ( + let is_inhabited = function + | Fields_shape.Arbitrary _ -> true + | _ -> false + in + let inhabited = List.filter is_inhabited variant_layouts in + match inhabited with + | [] -> Primitive + | [ single ] -> single + | _ :: _ :: _ -> failwith ">1 inhabited variants with no tag encoding?") + in + ok @@ mk ~size ~align ~uninhabited ~fields () + +and compute_size ty size = + match size with + | Some s -> BV.usizei s + | None -> + layout_warning "Inferred size=0" ty; + BV.usizei 0 + +and compute_align ty align = + match align with + | Some a -> BV.usizeinz a + | None -> + layout_warning "Inferred align=1" ty; + BV.usizeinz 1 + +and compute_arbitrary_layout ?fst_size ?fst_align + ?(variant = Types.VariantId.zero) ty members = + layout_warning "Computed an arbitrary layout" ty; (* Note: here we manually calculate a layout, à la [repr(C)]. We should avoid doing this, and make it clearer when we do. *) (* Calculates the offsets, size and alignment for a tuple-like type with fields of @@ -283,167 +328,60 @@ and layout_of_members ?fst_size ?fst_align ty members = in let++ () = assert_or_error (Typed.not overflowed) (`InvalidLayout ty) in let size = size_to_fit ~size ~align in - mk ~size ~align - ~fields:(Arbitrary (Types.VariantId.zero, Array.of_list offsets)) - () - -and layout_of_struct ty (adt : Types.type_decl) (fields : Types.field list) = - match adt.layout with - | Some - { - variant_layouts = [ { field_offsets; _ } ]; - size = Some size; - align = Some align; - _; - } -> - let offsets = Array.of_list @@ List.map BV.usizei field_offsets in - ok - (mk_concrete ~size ~align - ~fields:(Arbitrary (Types.VariantId.zero, offsets)) - ()) - | Some { variant_layouts = [ { field_offsets; _ } ]; _ } -> - (* we want to compute a size/align, but keep the field offsets - this is needed for DSTs, where we're not provided a size but we definitely - care about field positions (the size won't matter anyways since we use - the pointer's metadata). *) - let++ base = layout_of_members ty (field_tys fields) in - let offsets = Array.of_list @@ List.map BV.usizei field_offsets in - mk ~size:base.size ~align:base.align - ~fields:(Arbitrary (Types.VariantId.zero, offsets)) - () - | _ -> layout_of_members ty (field_tys fields) - -and layout_of_enum ty (adt : Types.type_decl) (variants : Types.variant list) = - match adt.layout with - | Some { discriminant_layout = None; variant_layouts; _ } -> ( - (* no discriminant: this means there is only one inhabited variant *) - let inhabited = - variant_layouts - |> List.mapi (fun i v -> (i, v)) - |> List.filter (fun (_, (v : Types.variant_layout)) -> - not v.uninhabited) - in - match inhabited with - | [] -> - (* no inhabited variant: uninhabited ZST *) - let tag : Tag_layout.t = - { - offset = Usize.(0s); - ty = TInt I32; - tags = [||]; - encoding = Direct; - } - in - ok (mk_concrete ~size:0 ~align:1 ~fields:(Enum (tag, [||])) ()) - | [ (i, variant_layout) ] -> - let vi = Types.VariantId.of_int i in - let offsets = - Array.of_list @@ List.map BV.usizei variant_layout.field_offsets - in - let variant = Types.VariantId.nth variants vi in - let++ sub_layout = layout_of_members ty (field_tys variant.fields) in - mk ~size:sub_layout.size ~align:sub_layout.align - ~fields:(Arbitrary (vi, offsets)) - () - | _ -> - Fmt.failwith - "More than one inhabited variant, but no discriminant layout? For \ - %a" - Crate.pp_name adt.item_meta.name) - | Some { discriminant_layout = Some _; _ } | None -> ( + mk ~size ~align ~fields:(Arbitrary (variant, Array.of_list offsets)) () + +and compute_enum_layout ty (variants : Types.variant list) = + layout_warning "Computed an enum layout" ty; + match variants with + (* no variants: uninhabited ZST *) + | [] -> + ok (mk_concrete ~size:0 ~align:1 ~uninhabited:true ~fields:Primitive ()) + (* N variants: we assume a tagged variant *) + | _ :: _ -> let tags = - match adt.layout with - | Some { variant_layouts; _ } -> - Monad.ListM.map variant_layouts (fun v -> - Option.map BV.of_scalar v.tag) - | None -> - (* this is bad, best effort *) - Monad.ListM.map variants (fun v -> - Some (BV.mk_lit (TInt I32) (z_of_literal v.discriminant))) + Monad.ListM.map variants (fun v -> Some (BV.of_literal v.discriminant)) in let tags = Array.of_list tags in let tag_layout : Tag_layout.t = - match adt.layout with - | Some { discriminant_layout = None; _ } -> failwith "Handled above" - | Some { discriminant_layout = Some discr_layout; _ } -> - (* there's a discriminant to handle *) - let ty = lit_of_int_ty discr_layout.tag_ty in - let offset = BV.usizei discr_layout.offset in - let encoding : Tag_layout.encoding = - match discr_layout.encoding with - | Niche v -> Niche v - | Direct -> Direct - in - { offset; ty; tags; encoding } - | None -> - (* best effort: we assume direct encoding *) - let ty : Types.literal_type = - match variants with - | [] -> TInt I32 (* Shouldn't matter *) - | v :: _ -> lit_ty_of_lit v.discriminant - in - { offset = Usize.(0s); ty; tags; encoding = Direct } + (* best effort: we assume direct encoding *) + let ty : Types.literal_type = + match variants with + | [] -> TInt I32 (* Shouldn't matter *) + | v :: _ -> lit_ty_of_lit v.discriminant + in + { offset = Usize.(0s); ty; tags; encoding = Direct } in - let** variant_layouts = - match adt.layout with - | Some { variant_layouts; size = Some size; align = Some align; _ } -> - let variant_layouts = - List.mapi - (fun i (v : Types.variant_layout) -> - let ofs = - Array.of_list (List.map BV.usizei v.field_offsets) - in - (Types.VariantId.of_int i, ofs)) - variant_layouts + let** tag = layout_of (TLiteral tag_layout.ty) in + let++ size, align, variants, uninhabited = + Result.fold_list variants + ~init:(Usize.(0s), Usize.(1s), [], true) + ~f:(fun (size, align, variants, uninhabited) v -> + let++ l = + compute_arbitrary_layout ty ~fst_size:tag.size + ~fst_align:tag.align (field_tys v.fields) in - let size = BV.usizei size in - let align = BV.usizeinz align in - let vs = - Monad.ListM.map variant_layouts (fun (i, ofs) -> - mk ~size ~align ~fields:(Arbitrary (i, ofs)) ()) - in - ok vs - | _ -> - let++ vs = - Result.fold_list variants ~init:[] ~f:(fun acc v -> - let++ l = layout_of_members ty (field_tys v.fields) in - l :: acc) - in - List.rev vs + ( BV.max ~signed:false size l.size, + BV.max ~signed:false align l.align, + l.fields :: variants, + uninhabited && l.uninhabited )) in - match variant_layouts with - (* no variants: uninhabited ZST *) - | [] -> - ok (mk_concrete ~size:0 ~align:1 ~fields:(Enum (tag_layout, [||])) ()) - (* N variants: realign variants with prepended tag (if not niche), - use biggest and most aligned *) - | _ -> - let++ variant_layouts = - match tag_layout.encoding with - | Direct -> - (* if we need to prepend the tag, we recompute the layout to consider its - size and alignement (there probably is a smarter way to do this). *) - let** discr_layout = layout_of (TLiteral tag_layout.ty) in - let layout_adjusted = - layout_of_members ty ~fst_size:discr_layout.size - ~fst_align:discr_layout.align - in - let++ vs = - Result.fold_list variants ~init:[] ~f:(fun acc v -> - let++ v = layout_adjusted (field_tys v.fields) in - v :: acc) - in - List.rev vs - | Niche _ -> ok variant_layouts - in - let size, align = - List.fold_left - (fun (size, align) l -> (max size l.size, max align l.align)) - (Usize.(0s), Usize.(1s)) - variant_layouts - in - let fields = List.map (fun v -> v.fields) variant_layouts in - { size; align; fields = Enum (tag_layout, Array.of_list fields) }) + let variants = List.rev variants in + mk ~size ~align ~uninhabited + ~fields:(Enum (tag_layout, Array.of_list variants)) + () + +and compute_union_layout ty members = + layout_warning "Computed a union layout" ty; + let++ size, align = + Result.fold_list members + ~init:(Usize.(0s), Usize.(1s)) + ~f:(fun (size, align) member_ty -> + let++ member = layout_of member_ty in + ( BV.max ~signed:false size member.size, + BV.max ~signed:false align member.align )) + in + let fields = Array.make (List.length members) (BV.usizei 0) in + mk ~size ~align ~fields:(Arbitrary (Types.VariantId.zero, fields)) () and resolve_trait_ty (tref : Types.trait_ref) ty_name = match tref.kind with diff --git a/soteria-rust/scripts/test_exclusions.py b/soteria-rust/scripts/test_exclusions.py index 8a319f9f0..b46248131 100644 --- a/soteria-rust/scripts/test_exclusions.py +++ b/soteria-rust/scripts/test_exclusions.py @@ -112,6 +112,7 @@ "FunctionCall/Variadic/main.rs", "Static/unsafe_extern_static_uninitialized.rs", # unsupported: libc + "Cast/cast_abstract_args_to_concrete.rs", "/LibC/", "/Strings/copy_empty_string_by_intrinsic.rs", "Slice/pathbuf.rs",