[rust] [2/2] Support the elaborated box reprenstation for precise-drops (#2036)

Summary:
and some partial support for modeling drops when retrieving drop glue with --desugar-drops.

We do some abstraction over Box, and NonNull since the compiler has some special handling for how it treats Box and NonNull and their ABI are equivalent.

Merge after #2035

Pull Request resolved: #2036

Reviewed By: martintrojer

Differential Revision: D105306414

Pulled By: dulmarod

fbshipit-source-id: 053875db8b4e14478e7af10efde68b783bb95e22

Author: ArjanSeijs

infer/lib/rust/models.sil

@@ -35,16 +35,16 @@
 // For example the following code:
 //      let b = Box::new(10);
 //      let value = *b;
-// By default boxes are handled as pointers by the use of the Deref Trait. ULLBC: 
+// (1) By default boxes are handled as pointers by the use of the Deref Trait. ULLBC: 
 //      `value = copy (*(b@1))`;
-// When using --mir-elaborated boxes are treated as a pointer to Unqiue and then derefenced : 
+// (2) When using --mir-elaborated or --precise-drops boxes are treated as a pointer to Unqiue and then derefenced : 
 //      @3 := transmute<NonNull<i32>, *const i32>(copy ((*(b@1)).0));
 //      value@2 := copy (*(@3));
-// When using --mir-elaborated --raw-boxes boxes are handled as:
+// (3) When using --mir-elaborated --raw-boxes boxes are handled as:
 //      @3 := transmute<NonNull<i32>, *const i32>(copy (((b@1).0).0));
 //      value@2 := copy (*(@3));
-// At some point we want to move to model the --mir-elaborated version since this allows us the get drop-elaboration to
-// get precise information on when a a value is freed.
+// With the default charon arguments defined Rust.ml we model version 2.
+// We do special handling for Box, Unqiue, and NonNull in RustMir2Textual.ml to treat them as pointers.
 define __sil_boxnew(o : int): *int {
   local ptr : *int
   #entry:
@@ -59,4 +59,15 @@ define __sil_boxnew(o : int): *int {
   #invalid:
     unreachable
 
+}
+
+// The function for dropping a box containg a primitive type
+// when using the --desugar-drops.
+// This is a model for the function:
+// alloc::boxed::Box::<i32>::drop_in_place(&Box)
+// 
+define __sil_boxdrop(o : **int): void {
+  #entry:
+    n1 = __sil_free([[&o:**int]:*int])
+    ret null
 }

infer/src/rust/RustMir2Textual.ml

@@ -108,9 +108,28 @@ let mk_typename_from_type_decl crate (type_decl : Charon.Generated_Types.type_de
   Textual.TypeName.of_string name
 
 
+(* Model for box drops when using --desugar-drops *)
+let is_box_primitive_drop_in_place crate fun_decl_id =
+  let decl = fun_map_find_id crate fun_decl_id in
+  match (decl.item_meta.name, decl.signature.inputs) with
+  | ( PeIdent ("alloc", _)
+      :: PeIdent ("boxed", _)
+      :: PeIdent ("Box", _)
+      :: _
+      :: PeIdent ("drop_in_place", _)
+      :: _
+    , TRawPtr (TAdt {id= TBuiltin TBox; generics= {types= TLiteral _ :: _}}, _) :: _ ) ->
+      true
+  | _, _ ->
+      false
+
+
 let fun_name_from_fun_operand (crate : Charon.UllbcAst.crate)
     (operand : Charon.Generated_GAst.fn_operand) : Textual.QualifiedProcName.t =
   match operand with
+  | FnOpRegular {kind= FunId (FRegular fun_decl_id)}
+    when is_box_primitive_drop_in_place crate fun_decl_id ->
+      Textual.ProcDecl.boxdrop_name
   | FnOpRegular {kind= FunId (FRegular fun_decl_id)} ->
       let decl = fun_map_find_id crate fun_decl_id in
       mk_qualified_proc_name crate decl.item_meta
@@ -225,6 +244,33 @@ let proc_name_from_binop (op : Charon.Generated_Expressions.binop) (typ : Textua
   (Textual.ProcDecl.of_binop bin_op, typ)
 
 
+(* Model Unqiue<T> and NonNull<T> as *T *)
+let is_pointer_type crate (name : Charon.Generated_Types.name) =
+  let name = name |> List.map ~f:(name_of_path_element crate) in
+  match name with
+  | "core" :: "ptr" :: "non_null" :: "NonNull" :: _ ->
+      true
+  | "core" :: "ptr" :: "unique" :: "Unique" :: _ ->
+      true
+  | _ ->
+      false
+
+
+let is_ty_decl_pointer_type crate type_decl_id =
+  let type_decl = type_decl_map_find_id crate type_decl_id in
+  is_pointer_type crate type_decl.item_meta.name
+
+
+let is_ty_pointer_type crate (ty : Charon.Generated_Types.ty) =
+  match ty with
+  | TAdt {id= TAdtId type_decl_id} ->
+      is_ty_decl_pointer_type crate type_decl_id
+  | TAdt {id= TBuiltin TBox} ->
+      true
+  | _ ->
+      false
+
+
 let rec mk_struct_args crate (types : Charon.Generated_Types.ty list) =
   List.map types ~f:(fun typ ->
       Textual.TypeName.of_string (Format.asprintf "%a" Textual.Typ.pp (ty_to_textual_typ crate typ)) )
@@ -239,13 +285,25 @@ and mk_tuple_struct_typ crate type_decl_ref =
   Textual.Typ.Struct (mk_tuple_type_name crate type_decl_ref)
 
 
+and mk_ptr_from_generics_types crate (types : Charon.Generated_Types.ty list) =
+  match types with
+  | typ :: _ ->
+      Textual.Typ.mk_ptr (ty_to_textual_typ crate typ)
+  | _ ->
+      Textual.Typ.mk_ptr Textual.Typ.Void
+
+
 and adt_ty_to_textual_typ crate (type_decl_ref : Charon.Generated_Types.type_decl_ref) :
     Textual.Typ.t =
   (* TODO: Implement other adt types *)
   match type_decl_ref.id with
   | TTuple ->
       if List.is_empty type_decl_ref.generics.types then Textual.Typ.Void
       else mk_tuple_struct_typ crate type_decl_ref.generics.types
+  | TAdtId type_decl_id
+    when let type_decl = type_decl_map_find_id crate type_decl_id in
+         is_pointer_type crate type_decl.item_meta.name ->
+      mk_ptr_from_generics_types crate type_decl_ref.generics.types
   | TAdtId type_decl_id -> (
       let type_decl = type_decl_map_find_id crate type_decl_id in
       match type_decl.kind with
@@ -257,12 +315,8 @@ and adt_ty_to_textual_typ crate (type_decl_ref : Charon.Generated_Types.type_dec
           Textual.Typ.Struct type_name
       | _ ->
           Textual.Typ.Void )
-  | TBuiltin TBox -> (
-    match type_decl_ref.generics.types with
-    | typ :: _ ->
-        Textual.Typ.mk_ptr (ty_to_textual_typ crate typ)
-    | _ ->
-        Textual.Typ.mk_ptr Textual.Typ.Void )
+  | TBuiltin TBox ->
+      mk_ptr_from_generics_types crate type_decl_ref.generics.types
   | TBuiltin TStr ->
       Textual.Typ.Struct Textual.TypeName.sil_string
 
@@ -377,10 +431,31 @@ let rec mk_exp_from_place ~loc (crate : Charon.UllbcAst.crate) (place_map : plac
   | PlaceLocal var_id ->
       let exp = Textual.Exp.Lvar (place_map_find_id place_map var_id) in
       exp
+  (* This models the --precise-drop versions of Box, Unqiue and NonNull as pointers since the 
+  compiler has some special handling for how it treats Box and NonNull and their ABI are equivalent.
+  For example:
+    let b = Box::new(10);
+    let value = *b;
+  Is lowered in mir to 
+    b_1 = @BoxNew<i32>
+    _3 := transmute<NonNull<i32>, *const i32>(copy (( *(b_1)).0));
+    value_2 := copy ( *(_3));
+  There are two abstractions here:
+  (1) *b_1 is the derefence of the box struct, box that access the underlying unique. 
+  The .0 is then a regular field acces of the unqiue that gets The NonNull.
+  (2) The transmute treats the NonNull struct the same is it's field.
+  This skips the ( *(b_1)) step.
+  *)
+  | PlaceProjection (({ty= TAdt {id= TBuiltin TBox}} as projection_place), Deref)
+    when is_ty_pointer_type crate place.ty ->
+      mk_exp_from_place ~loc crate place_map projection_place
   | PlaceProjection (projection_place, Deref) ->
       let proj_typ = ty_to_textual_typ crate projection_place.ty in
       let exp = mk_exp_from_place ~loc crate place_map projection_place in
       Textual.Exp.Load {exp; typ= Some proj_typ}
+  (* This skips the NonNull<T>.0 and Unqiue<T>.0 step *)
+  | PlaceProjection (projection_place, Field _) when is_ty_pointer_type crate projection_place.ty ->
+      mk_exp_from_place ~loc crate place_map projection_place
   | PlaceProjection (projection_place, Field (ProjAdt (type_decl_id, variant), field_id)) ->
       let exp = mk_exp_from_place ~loc crate place_map projection_place in
       let type_decl = type_decl_map_find_id crate type_decl_id in
@@ -630,21 +705,26 @@ let mk_terminator (crate : Charon.UllbcAst.crate) (idx : int) (place_map : place
   (* A drop frees the memory of a value once it goes out of scope.
     The following implementation is a simplified model for drops 
     of boxes created by Box::new() of types using the global allocator.
+
     https://doc.rust-lang.org/1.93.1/alloc/alloc/struct.Global.html
     https://rustc-dev-guide.rust-lang.org/mir/drop-elaboration.html
     https://doc.rust-lang.org/1.93.1/alloc/alloc/trait.GlobalAlloc.html#tymethod.dealloc
   *)
-  | Drop (Precise, ({ty= TAdt {id= TBuiltin TBox}} as place), _trait_ref, target, on_unwind) ->
-      let exp, _ = mk_exp_from_place_load ~loc crate place_map place in
-      let qualified_free_name = Textual.ProcDecl.free_name in
-      let free_call = Textual.Exp.call_non_virtual qualified_free_name [exp] in
-      let free_instr = Textual.Instr.Let {id= None; exp= free_call; loc} in
-      let on_unwind = mk_label (Charon.Generated_UllbcAst.BlockId.to_int on_unwind) in
-      let target = mk_jump target in
-      ([], [free_instr], target, [on_unwind])
+  | Drop (Precise, place, _trait_ref, target, on_unwind) -> (
+    match place.ty with
+    | TAdt {id= TBuiltin TBox; generics= {types= TLiteral _ :: _}} ->
+        let exp, _ = mk_exp_from_place_load ~loc crate place_map place in
+        let qualified_free_name = Textual.ProcDecl.free_name in
+        let free_call = Textual.Exp.call_non_virtual qualified_free_name [exp] in
+        let free_instr = Textual.Instr.Let {id= None; exp= free_call; loc} in
+        let on_unwind = mk_label (Charon.Generated_UllbcAst.BlockId.to_int on_unwind) in
+        let target = mk_jump target in
+        ([], [free_instr], target, [on_unwind])
+    | ty ->
+        L.die UserError "[ERROR] Unsupported drop for type: @. > %a @." Charon.Types.pp_ty ty )
   | _ ->
-      L.die UserError "[ERROR] Unsupported terminator: %a " Charon.Generated_UllbcAst.pp_terminator
-        terminator
+      L.die UserError "[ERROR] Unsupported terminator: @. > %a @."
+        Charon.Generated_UllbcAst.pp_terminator terminator
 
 
 let mk_field_store_instr_from_rvalue ~loc crate lexp enclosing_class place_map field_id
@@ -680,16 +760,7 @@ let mk_instr crate (place_map : place_map_ty) (statement : Charon.Generated_Ullb
   | Assign (lhs, Aggregate (AggregatedAdt ({id= TAdtId type_decl_id}, None, None), ops)) ->
       let lexp = mk_exp_from_place ~loc crate place_map lhs in
       let type_decl = type_decl_map_find_id crate type_decl_id in
-      let fields =
-        match type_decl.kind with
-        | Struct fields ->
-            fields
-        | _ ->
-            L.die UserError
-              "[ERROR] Should not be reachable: Encountered none struct kind even tough variant \
-               and field_id are None. @. > %a @."
-              Charon.Generated_Types.pp_type_decl_kind type_decl.kind
-      in
+      let fields = Charon.TypesUtils.type_decl_get_fields type_decl None in
       let enclosing_class = mk_typename_from_type_decl crate type_decl None in
       mk_field_store_instrs_from_rvalues ~loc crate lexp enclosing_class place_map ops fields
   (* Enum Variant *)
@@ -749,6 +820,10 @@ let mk_instr crate (place_map : place_map_ty) (statement : Charon.Generated_Ullb
       []
   | StorageLive _ ->
       []
+  | PlaceMention place ->
+      let exp, _ = mk_exp_from_place_load ~loc crate place_map place in
+      let instr = Textual.Instr.Let {id= None; exp; loc} in
+      [instr]
   | s ->
       L.die UserError "[ERROR] Unsupported statement: @. > %a @."
         Charon.Generated_UllbcAst.pp_statement_kind s

infer/src/rust/unit/RustMir2TextualTestPointers.ml

@@ -436,7 +436,6 @@ let%expect_test "box_memoryleak" =
     |}]
 
 
-(* TODO: Support for precise box drops will be added in the next commit *)
 let%expect_test "box_use_after_free" =
   let source =
     {|
@@ -458,4 +457,57 @@ let%expect_test "box_use_after_free" =
        --start-from=crate::main"
     source ;
   [%expect
-    {| Test failed: expression [&x_2:*int] has type *int, while a pointer of struct type was expected |}]
+    {|
+    .source_language = "Rust"
+
+    type alloc::alloc::Global = {}
+
+    type core::marker::PhantomData::<i32> = {}
+
+    type core::ptr::non_null::NonNull::<i32> = {pointer: *int}
+
+    type core::ptr::unique::Unique::<i32> = {pointer: *void; _marker: core::marker::PhantomData::<i32>}
+
+    define dummy::main() : void {
+      local var_0: void, ptr_1: *int, x_2: *int, var_3: *int, var_4: *int, ub_5: int, var_6: *int
+      #node_0:
+          store &var_0 <- null:void
+          n0 = __sil_boxnew(50)
+          store &x_2 <- n0:*int
+          jmp node_2
+          .handlers node_1
+
+      #node_1:
+          throw "UnwindResume"
+
+      #node_2:
+          n1:*void = load &x_2
+          store &var_6 <- __sil_cast(<*int>, n1):*int
+          n2:*int = load &var_6
+          store &var_4 <- n2:*int
+          n3:*int = load &var_4
+          store &var_3 <- n3:*int
+          n4:*int = load &var_3
+          store &ptr_1 <- n4:*int
+          n5:*int = load &x_2
+          n6 = __sil_free(n5)
+          jmp node_3
+          .handlers node_4
+
+      #node_3:
+          n7:*int = load &ptr_1
+          n8:int = load n7
+          store &ub_5 <- n8:int
+          store &var_0 <- null:void
+          n9:void = load &var_0
+          ret n9
+
+      #node_4:
+          throw "UnwindResume"
+
+    }
+
+    declare alloc::alloc::Global::{TraitImpl@1}::drop_in_place(*alloc::alloc::Global) : void
+
+    declare alloc::boxed::Box::{TraitImpl@2}::drop_in_place::<i32, alloc::alloc::Global>(**int) : void
+    |}]

infer/src/textual/Textual.ml

@@ -208,7 +208,9 @@ let builtin_get_lazy_class = "__sil_get_lazy_class"
 
 let builtin_instanceof = "__sil_instanceof"
 
-let builin_boxnew = "__sil_boxnew"
+let builtin_boxnew = "__sil_boxnew"
+
+let builtin_boxdrop = "__sil_boxdrop"
 
 module BaseTypeName : sig
   include NAME
@@ -874,7 +876,9 @@ module ProcDecl = struct
 
   let instanceof_name = make_toplevel_name builtin_instanceof Location.Unknown
 
-  let boxnew_name = make_toplevel_name builin_boxnew Location.Unknown
+  let boxnew_name = make_toplevel_name builtin_boxnew Location.Unknown
+
+  let boxdrop_name = make_toplevel_name builtin_boxdrop Location.Unknown
 
   let unop_table : (Unop.t * string) list =
     [(Neg, "__sil_neg"); (BNot, "__sil_bnot"); (LNot, "__sil_lnot")]
@@ -1075,7 +1079,7 @@ module ProcDecl = struct
     [builtin_assert_fail; builtin_swift_alloc; builtin_objc_alloc] @ unop_builtins @ binop_builtins
 
 
-  let builtins_rust = [builtin_free; builtin_malloc; builin_boxnew]
+  let builtins_rust = [builtin_free; builtin_malloc; builtin_boxnew; builtin_boxdrop]
 
   let is_builtin (proc : QualifiedProcName.t) lang =
     match lang with

infer/src/textual/Textual.mli

@@ -431,6 +431,8 @@ module ProcDecl : sig
 
   val boxnew_name : QualifiedProcName.t
 
+  val boxdrop_name : QualifiedProcName.t
+
   val is_allocate_array_builtin : QualifiedProcName.t -> bool
 
   val is_get_lazy_class_builtin : QualifiedProcName.t -> bool

infer/tests/codetoanalyze/rust/pulse/issues.exp

@@ -1,3 +1,4 @@
+box_free.rs, box_free::main, 10, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,in call to `__sil_boxnew`,allocated by call to `malloc` (modelled),returned,return from call to `__sil_boxnew`,assigned,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,in call to `__sil_boxnew`,allocated by call to `malloc` (modelled),returned,return from call to `__sil_boxnew`,assigned,assigned,assigned,assigned,assigned,invalid access occurs here]
 box_leak.rs, box_leak::main, 4, MEMORY_LEAK_C, no_bucket, ERROR, [allocation part of the trace starts here,when calling `__sil_boxnew` here,allocated by `malloc` here,memory becomes unreachable here]
 dangling.rs, dangling::create_evil_pointer, 7, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, [variable `x_1` accessed here,assigned,assigned,assigned,returned here]
 dangling.rs, dangling::main, 11, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `dangling::create_evil_pointer` here,variable `x_1` accessed here,is the address of a stack variable `x_1` whose lifetime has ended,use-after-lifetime part of the trace starts here,in call to `dangling::create_evil_pointer`,variable `x_1` accessed here,assigned,assigned,assigned,returned,return from call to `dangling::create_evil_pointer`,assigned,invalid access occurs here]

infer/tests/codetoanalyze/rust/sil/box_free.rs.ullbc.sil

@@ -8,5 +8,42 @@
 
 type alloc::alloc::Global = {}
 
-declare box_free::main() : void
+define box_free::main() : void {
+  local var_0: void, ptr_1: *int, x_2: *int, var_3: *int, var_4: *int, ub_5: int, var_6: *int
+  #node_0:
+      store &var_0 <- null:void
+      n0 = __sil_boxnew(50)
+      store &x_2 <- n0:*int
+      jmp node_2
+      .handlers node_1
+      
+  #node_1:
+      throw "UnwindResume"
+      
+  #node_2:
+      n1:*int = load &x_2
+      store &var_6 <- __sil_cast(<*int>, n1):*int
+      n2:*int = load &var_6
+      store &var_4 <- n2:*int
+      n3:*int = load &var_4
+      store &var_3 <- n3:*int
+      n4:*int = load &var_3
+      store &ptr_1 <- n4:*int
+      n5:*int = load &x_2
+      n6 = __sil_free(n5)
+      jmp node_3
+      .handlers node_4
+      
+  #node_3:
+      n7:*int = load &ptr_1
+      n8:int = load n7
+      store &ub_5 <- n8:int
+      store &var_0 <- null:void
+      n9:void = load &var_0
+      ret n9
+      
+  #node_4:
+      throw "UnwindResume"
+      
+}