Preserve struct data when converting to byte array (verifast#699)

bin/crt.vfmanifest

@@ -145,6 +145,7 @@
 .provides ./prelude.h#map_uchar_of_char_char_of_uchar
 .provides ./prelude.h#map_char_of_uchar_uchar_of_char
 .provides ./prelude.h#chars_to_uchars
+.provides ./prelude.h#of_chars__chars__of
 .provides ./prelude.h#uchars_to_chars
 .provides ./prelude.h#chars_to_ints
 .provides ./prelude.h#ints_to_chars

bin/prelude.h

@@ -360,6 +360,13 @@ predicate chars(char *array, int count; list<char> cs) =
     :
         character(array, ?c) &*& chars(array + 1, count - 1, ?cs0) &*& cs == cons(c, cs0);
 
+fixpoint list<option<char> > chars__of<t>(void *typeId, t v);
+fixpoint t of_chars_<t>(void *typeId, list<option<char> > cs);
+
+lemma_auto(of_chars_<t>(typeId, chars__of<t>(typeId, v))) void of_chars__chars__of<t>(void *typeId, t v);
+requires true;
+ensures of_chars_<t>(typeId, chars__of<t>(typeId, v)) == v;
+
 lemma_auto void chars_to_chars_(char *array);
     requires [?f]chars(array, ?count, ?cs);
     ensures [f]chars_(array, count, map(some, cs));

bin/rust/prelude_core.rsspec

@@ -140,7 +140,14 @@ fix has_type(p: *_, typeid_: *_) -> bool;
 
 fix ptr_add_(p: pointer, offset: i32, elemTypeid: *_) -> pointer {
     ptr_add(p, offset * std::mem::size_of(elemTypeid))
-}   
+}
+
+fix u8s__of<T>(v: T) -> list<option<u8>>;
+fix of_u8s_<T>(cs: list<option<u8>>) -> T;
+
+lem_auto(of_u8s_::<T>(u8s__of::<T>(v as T))) of_u8s__u8s__of<T>(v: T);
+req true;
+ens of_u8s_::<T>(u8s__of::<T>(v)) == v;
 
 pred points_to_<t>(p: *t; v: option<t>);
 pred points_to<t>(p: *t; v: t) = points_to_::<t>(p, some(v));

examples/mcas/bitops_ex.vfmanifest

@@ -115,6 +115,7 @@
 .requires CRT/prelude.h#map_uchar_of_char_char_of_uchar
 .requires CRT/prelude.h#null_pointer_provenance_max_addr
 .requires CRT/prelude.h#null_pointer_provenance_min_addr
+.requires CRT/prelude.h#of_chars__chars__of
 .requires CRT/prelude.h#pointer_nonzero
 .requires CRT/prelude.h#pointer_of_chars_of_pointer
 .requires CRT/prelude.h#pointer_to_chars

src/assertions.ml

@@ -139,10 +139,10 @@ module Assertions(VerifyProgramArgs: VERIFY_PROGRAM_ARGS) = struct
     let ((_, (_, _, _, _, symb, _, _)), p__opt) = List.assoc (fparent, fname) field_pred_map in
     let tpenv = List.combine tparams targs in
     let frange = instantiate_type tpenv frange in
-    if fghost = Real then begin
-      match tv with
-        Some tv -> assume_bounds tv frange
-      | None -> ()
+    begin match fghost, tv, kind with
+    | Real, Some tv, RegularPointsTo -> assume_bounds tv frange
+    | Real, Some tv, MaybeUninit -> assume_bounds tv (option_type frange)
+    | _ -> ()
     end;
     (* automatic generation of t1 != t2 if t1.f |-> _ &*& t2.f |-> _ *)
     begin fun cont ->
@@ -846,7 +846,7 @@ module Assertions(VerifyProgramArgs: VERIFY_PROGRAM_ARGS) = struct
             in
             prover_convert_term v tp' tp
           in
-          let (_, csym, _, _) = List.assoc sn struct_accessor_map in
+          let (_, csym, _, _, _) = List.assoc sn struct_accessor_map in
           ctxt#mk_app csym vs
       end
     | _ ->
@@ -2275,7 +2275,7 @@ module Assertions(VerifyProgramArgs: VERIFY_PROGRAM_ARGS) = struct
           None -> cont None
         | Some ((coef, v), h) ->
           let tpenv = List.combine tparams wanted_targs in
-          let (_, _, getters, _) = List.assoc sn struct_accessor_map in
+          let (_, _, getters, _, _) = List.assoc sn struct_accessor_map in
           let chunks = List.map2 begin fun (fn', (_, Real, ft', _, _)) (_, getter) ->
             let fv = prover_convert_term (ctxt#mk_app getter [v]) ft' (instantiate_type tpenv ft') in
             let ((_, (_, _, _, _, symb', _, _)), _) = List.assoc (sn, fn') field_pred_map in
@@ -2359,7 +2359,7 @@ module Assertions(VerifyProgramArgs: VERIFY_PROGRAM_ARGS) = struct
             with
               None -> cont None
             | Some ((coef, v), h) ->
-              let (_, csym, _, _) = List.assoc sn struct_accessor_map in
+              let (_, csym, _, _, _) = List.assoc sn struct_accessor_map in
               cont (Some (Chunk ((generic_points_to_symb (), true), [wanted_targ], coef, [structPointerTerm; ctxt#mk_app csym [v]], None)::h))
             end
           | _ ->
@@ -2374,7 +2374,7 @@ module Assertions(VerifyProgramArgs: VERIFY_PROGRAM_ARGS) = struct
             | Some (coef, h) ->
               let rec iter h vs = function
                 [] ->
-                let (_, csym, _, _) = List.assoc sn struct_accessor_map in
+                let (_, csym, _, _, _) = List.assoc sn struct_accessor_map in
                 cont (Some (Chunk ((generic_points_to_symb (), true), [wanted_targ], coef, [structPointerTerm; ctxt#mk_app csym (List.rev vs)], None)::h))
               | (fn, (_, Real, ft, _, _))::fds ->
                 let ((_, (_, _, _, _, symb, _, _)), _) = List.assoc (sn, fn) field_pred_map in

src/verifast.ml

@@ -657,6 +657,43 @@ module VerifyProgram(VerifyProgramArgs: VERIFY_PROGRAM_ARGS) = struct
       with_context (Executing (h, env, l, "Consuming object")) $. fun () ->
       consume_c_object_core_core l real_unit_pat pointerTerm pointeeType h env true false $. fun _ h (Some value) ->
       cont (Chunk ((generic_points_to_symb (), true), [pointeeType], real_unit, [pointerTerm; value], None)::h) env
+    | ExprStmt (CallExpr (l, "open_malloc_block", targs, [], args, Static)) when language = CLang ->
+      require_pure ();
+      let e = match (targs, args) with ([], [LitPat e]) -> e | _ -> static_error l "open_malloc_block expects no type arguments and one argument." None in
+      let (w, tp) = check_expr (pn,ilist) tparams tenv e in
+      let sn, targs = match tp with PtrType (StructType (sn, targs)) -> sn, targs | _ -> static_error l "The argument of open_malloc_block must be of type pointer-to-struct." None in
+      let _, _, body_opt, padding_pred_symb_opt, _ = List.assoc sn structmap in
+      let padding_pred_symb =
+        match padding_pred_symb_opt with
+        | None -> static_error l "open_malloc_block cannot be used for packed structs or structs with ghost fields." None
+        | Some s -> s
+      in
+      eval_h h env w @@ fun h env pointer_term ->
+      let _, (_, _, _, _, malloc_block_symb, _, _) = List.assoc sn malloc_block_pred_map in
+      consume_chunk rules h env [] [] [] l (malloc_block_symb, true) targs real_unit real_unit_pat (Some 1) [TermPat pointer_term] @@ fun _ h _ _ _ _ _ _ ->
+      produce_chunk h (padding_pred_symb, true) targs real_unit None [pointer_term] None @@ fun h ->
+      let size = struct_size l env sn targs in
+      let malloc_pred_symb = get_pred_symb "malloc_block" in
+      produce_chunk h (malloc_pred_symb, true) targs real_unit None [pointer_term; size] None @@ fun h ->
+      cont h env
+    | ExprStmt (CallExpr (l, "close_malloc_block", targs, [], args, static)) when language = CLang ->
+      require_pure ();
+      let e = match (targs, args) with ([], [LitPat e]) -> e | _ -> static_error l "close_malloc_block expects no type arguments and one argument." None in
+      let (w, tp) = check_expr (pn,ilist) tparams tenv e in
+      let sn, targs = match tp with PtrType (StructType (sn, targs)) -> sn, targs | _ -> static_error l "The argument of close_malloc_block must be of type pointer-to-struct." None in
+      let _, _, body_opt, padding_pred_symb_opt, _ = List.assoc sn structmap in
+      let padding_pred_symb =
+        match padding_pred_symb_opt with
+        | None -> static_error l "close_malloc_block cannot be used for packed structs or structs with ghost fields." None
+        | Some s -> s
+      in
+      eval_h h env w @@ fun h env pointer_term ->
+      let _, (_, _, _, _, malloc_block_symb, _, _) = List.assoc sn malloc_block_pred_map in
+      let size = struct_size l env sn targs in
+      consume_chunk rules h env [] [] [] l (get_pred_symb "malloc_block", true) targs real_unit real_unit_pat (Some 1) [TermPat pointer_term; TermPat size] @@ fun _ h _ _ _ _ _ _ ->
+      consume_chunk rules h env [] [] [] l (padding_pred_symb, true) targs real_unit real_unit_pat (Some 1) [TermPat pointer_term] @@ fun _ h _ _ _ _ _ _ ->
+      produce_chunk h (malloc_block_symb, true) targs real_unit None [pointer_term] None @@ fun h ->
+      cont h env
     | ExprStmt (CallExpr (l, ("close_struct" | "close_struct_zero" as name), targs, [], args, Static)) when language = CLang ->
       require_pure ();
       let e = match (targs, args) with ([], [LitPat e]) -> e | _ -> static_error l "close_struct expects no type arguments and one argument." None in
@@ -679,7 +716,14 @@ module VerifyProgram(VerifyProgramArgs: VERIFY_PROGRAM_ARGS) = struct
       end $. fun h elems ->
       let init =
         match name with
-          "close_struct" -> Unspecified
+        | "close_struct" ->
+          begin match List.assoc sn structmap with
+          | _, _, Some (_, fields_map, _), _, _ -> 
+            let of_bytes_symb = get_pure_func_symb (match dialect with Some Rust -> "of_u8s_" | _ -> "of_chars_") in
+            let terms = [typeid_of_core l env (StructType (sn, targs)); elems] in
+            MaybeUninitTerm (mk_app of_bytes_symb terms)
+          | _ -> Unspecified
+          end
         | "close_struct_zero" ->
           let cond = mk_all_eq charType elems (ctxt#mk_intlit 0) in
           if not (ctxt#query cond) then assert_false h env l ("Could not prove condition " ^ ctxt#pprint cond) None;
@@ -693,18 +737,22 @@ module VerifyProgram(VerifyProgramArgs: VERIFY_PROGRAM_ARGS) = struct
       let (w, tp) = check_expr (pn,ilist) tparams tenv e in
       let sn, targs = match tp with PtrType (StructType (sn, targs)) -> sn, targs | _ -> static_error l "The argument of open_struct must be of type pointer-to-struct." None in
       eval_h h env w $. fun h env pointerTerm ->
-      consume_c_object_core_core l real_unit_pat pointerTerm (StructType (sn, targs)) h env true true $. fun _ h _ ->
-      assume_has_type l env pointerTerm (StructType (sn, targs)) $. fun () ->
-      let cs = get_unique_var_symb "cs" (list_type (option_type charType)) in
-      let Some (_, _, _, _, length_symb) = try_assoc' Ghost (pn,ilist) "length" purefuncmap in
+      consume_c_object_core_core l real_unit_pat pointerTerm (StructType (sn, targs)) h env true true @@ fun _ h (Some struct_value) ->
+      assume_has_type l env pointerTerm (StructType (sn, targs)) @@ fun () ->
+      let bytes_of_struct_term = 
+        let bytes_of_symb = get_pure_func_symb (match dialect with Some Rust -> "u8s__of" | _ -> "chars__of") in
+        let terms = [typeid_of_core l env (StructType (sn, targs)); struct_value] in
+        mk_app bytes_of_symb terms 
+      in
+      let length_symb = get_pure_func_symb "length" in
       let size = struct_size l env sn targs in
-      assume (ctxt#mk_eq (mk_app length_symb [cs]) size) $. fun () ->
+      assume (ctxt#mk_eq (mk_app length_symb [bytes_of_struct_term]) size) $. fun () ->
       let chunk =
         match dialect with
           Some Rust ->
-          Chunk ((array__symb (), true), [u8Type], real_unit, [pointerTerm; size; cs], None)
+          Chunk ((array__symb (), true), [u8Type], real_unit, [pointerTerm; size; bytes_of_struct_term], None)
         | _ ->
-          Chunk ((chars__pred_symb (), true), [], real_unit, [pointerTerm; size; cs], None)
+          Chunk ((chars__pred_symb (), true), [], real_unit, [pointerTerm; size; bytes_of_struct_term], None)
       in
       cont (chunk::h) env
     | ExprStmt (CallExpr (l, "produce_type_interp", targs, indices, args, Static)) when dialect = Some Rust ->
@@ -997,7 +1045,7 @@ module VerifyProgram(VerifyProgramArgs: VERIFY_PROGRAM_ARGS) = struct
                 let rec iter h env vs bs =
                   match bs with
                     [] ->
-                    let (_, csym, _, _) = List.assoc sn struct_accessor_map in
+                    let (_, csym, _, _, _) = List.assoc sn struct_accessor_map in
                     cont h env (ctxt#mk_app csym (List.rev vs))
                   | ((f, (_, _, tp, _, _)), (f_opt, e))::bs ->
                     begin match f_opt with
@@ -2901,12 +2949,14 @@ module VerifyProgram(VerifyProgramArgs: VERIFY_PROGRAM_ARGS) = struct
         end
         ps;
       ctxt#begin_formal;
-      let xs = Array.init (List.length ps) (fun j -> ctxt#mk_bound j (typenode_of_type (snd (List.nth ps j)))) in
-      let xs = Array.to_list xs in
-      let Some(env) = zip (List.map fst ps) xs in
+      let typeid_tparams = tparams' |> List.filter tparam_carries_typeid in
+      let typeid_env = typeid_tparams |> List.map @@ fun x -> (x ^ "_typeid", ctxt#type_inductive) in 
+      let ps_env = ps |> List.map @@ fun (x, tp) -> (x, typenode_of_type tp) in
+      let tn_env = typeid_env @ ps_env in
+      let env = tn_env |> List.mapi @@ fun i (x, tn) -> (x, ctxt#mk_bound i tn) in
       let t_pre = eval None env pre in
       let t_post = eval None env post in
-      let tps = (List.map (fun (x, t) -> (typenode_of_type t)) ps) in
+      let tps = List.map snd tn_env in
       let trigger = (
       match trigger with
         None -> []

src/verifast1.ml

@@ -909,6 +909,7 @@ module VerifyProgram1(VerifyProgramArgs: VERIFY_PROGRAM_ARGS) = struct
       * symbol                 (* constructor function *)
       * (string * symbol) list (* getter function for each field *)
       * (string * symbol) list (* setter function for each field *)
+      * symbol                 (* constructor.opt function *)
     type malloc_block_pred_info =
         string (* predicate name *)
       * pred_fam_info
@@ -3300,23 +3301,30 @@ module VerifyProgram1(VerifyProgramArgs: VERIFY_PROGRAM_ARGS) = struct
         | None -> []
         | Some (_, fds, _) ->
           let cname = "mk_" ^ sn in
-          let field_types = fds |> List.map (fun (f, (_, _, t, _, _)) -> (f, t)) in
-          let fieldnames = List.map fst field_types in
+          let field_gh_types = fds |> List.map (fun (f, (_, gh, t, _, _)) -> (f, gh, t)) in
+          let field_names = List.map (fun (f, _, _) -> f) field_gh_types in
           let tt = StructType (sn, tparams_as_targs tparams) in
           let subtype = InductiveSubtype.alloc () in
-          let (csym, _) = mk_func_symbol cname (List.map (fun (x, t) -> provertype_of_type t) field_types) ProverInductive (Proverapi.Ctor (CtorByOrdinal (subtype, 0))) in
-          let getters = field_types |> List.map (fun (f, t) -> (f, make_getter sn tt csym subtype fieldnames f t)) in
-          let setters = field_types |> List.map (fun (f, t) -> (f, make_setter sn tt csym subtype getters fieldnames f t)) in
+          let subtype_opt = InductiveSubtype.alloc () in
+          let (csym, _) = mk_func_symbol cname (List.map (fun (x, _, t) -> provertype_of_type t) field_gh_types) ProverInductive (Proverapi.Ctor (CtorByOrdinal (subtype, 0))) in
+          let (csym_opt, _) = mk_func_symbol (cname ^ ".opt") (field_gh_types |> 
+            List.map (function 
+              | (f, Ghost, t) -> provertype_of_type t
+              | (f, Real, t) -> provertype_of_type (InductiveType ("option", [t])))) 
+            ProverInductive (Proverapi.Ctor (CtorByOrdinal (subtype_opt, 0))) 
+          in
+          let getters = field_gh_types |> List.map (fun (f, _, t) -> (f, make_getter sn tt csym subtype field_names f t)) in
+          let setters = field_gh_types |> List.map (fun (f, _, t) -> (f, make_setter sn tt csym subtype getters field_names f t)) in
           (* Axiom: forall s, mk_s (get_f1 s) ... (get_fN s) == s *)
-          if field_types <> [] then begin
+          if field_gh_types <> [] then begin
             ctxt#begin_formal;
             let s = ctxt#mk_bound 0 ctxt#type_inductive in
             let mk_term = ctxt#mk_app csym (List.map (fun (_, getter) -> ctxt#mk_app getter [s]) getters) in
             let fact = ctxt#mk_eq mk_term s in
             ctxt#end_formal;
             ctxt#assume_forall (sn ^ "_injectiveness") [mk_term] [ctxt#type_inductive] fact
           end;
-          [(sn, (l, csym, getters, setters))]
+          [(sn, (l, csym, getters, setters, csym_opt))]
         end
     )
 
@@ -8067,7 +8075,7 @@ let check_if_list_is_defined () =
           prover_convert_term v tp' tp
         end
       in
-      let (_, csym, _, _) = List.assoc sn struct_accessor_map in
+      let (_, csym, _, _, _) = List.assoc sn struct_accessor_map in
       cont state (ctxt#mk_app csym vs_boxed)
     | TruncatingExpr (l, CastExpr (lc, ManifestTypeExpr (_, t), e)) ->
       begin
@@ -8296,7 +8304,7 @@ let check_if_list_is_defined () =
     | WSelect(l, e, fparent, tparams, fname, frange, targs) ->
       let tpenv = List.combine tparams targs in
       let frange' = instantiate_type tpenv frange in
-      let (_, _, getters, _) = List.assoc fparent struct_accessor_map in
+      let (_, _, getters, _, _) = List.assoc fparent struct_accessor_map in
       let getter = List.assoc fname getters in
       ev state e $. fun state v ->
       cont state (prover_convert_term (ctxt#mk_app getter [v]) frange frange')