Adding offsetof checks as static assertions when refining a C type

src/3d/GlobalEnv.fst

@@ -95,4 +95,9 @@ let resolve_probe_fn (g:global_env) (id:ident)
   = match H.try_find g.ge_probe_fn id.v with
     | Some {d_decl={v=ExternProbe id}} -> Some id
     | _ -> None
-
+
+let fields_of_type (g:global_env) (typename:ident)
+: ML (option (list field))
+= match H.try_find g.ge_h typename.v with
+  | Some ({d_decl={v=Record _ _ _ fields}}, _) -> Some fields
+  | _ -> None

src/3d/Options.fst

@@ -4,31 +4,9 @@ open FStar.All
 open FStar.ST
 module U8 = FStar.UInt8
 module OS = OS
-
+open Utils
 #push-options "--warn_error -272" //top-level effects are okay
 
-inline_for_extraction
-let valid_string
-  (valid: (string -> Tot bool))
-: Tot Type0
-= (s: string { valid s == true })
-
-let always_valid (_: string) : Tot bool = true
-
-let starts_with_capital (s: string) : Tot bool =
-  String.length s >= 1 &&
-  begin let first = String.sub s 0 1 in
-    String.compare first "A" >= 0 && String.compare first "Z" <= 0
-  end
-
-let ends_with (s:string) (suffix:string) : bool =
-  let l = String.length s in
-  let sl = String.length suffix in
-  if sl > l || sl = 0
-  then false
-  else let suffix' = String.sub s (l - sl) sl in
-       suffix = suffix'
-
 let check_config_file_name (fn:string) 
   : bool
   = let fn = OS.basename fn in
@@ -209,12 +187,6 @@ let set_implies (options: ref (list cmd_option)) (implies: list string) : ML uni
     )
     implies
 
-let string_starts_with (big small: string) : Tot bool =
-  let small_len = String.length small in
-  if String.length big < small_len
-  then false
-  else String.sub big 0 small_len = small
-
 let negate_string_gen (s: string) (negation: string) =
   if s `string_starts_with` negation
   then String.sub s (String.length negation) (String.length s - String.length negation)

src/3d/StaticAssertions.fst

@@ -24,15 +24,27 @@ type sizeof_assertion = {
   size : int
 }
 
+noeq
+type offsetof_assertion = {
+  type_name : ident;
+  field_name : ident;
+  offset : int
+}
+
+noeq
+type static_assert =
+| SizeOfAssertion of sizeof_assertion
+| OffsetOfAssertion of offsetof_assertion
+
 noeq
 type static_asserts = {
   includes : list string;
-  sizeof_assertions : list sizeof_assertion
+  assertions : list static_assert
 }
 
 let empty_static_asserts = {
   includes = [];
-  sizeof_assertions = []
+  assertions = []
 }
 
 let compute_static_asserts (benv:B.global_env)
@@ -43,36 +55,62 @@ let compute_static_asserts (benv:B.global_env)
     match r with
     | None -> empty_static_asserts
     | Some r -> 
-      let sizeof_assertions =
+      let static_assertions =
         r.type_map
-        |> List.map
+        |> List.collect
           (fun (i, jopt) ->
             let j =
               match jopt with
               | None -> i
               | Some j -> j
             in
+            let offsets = TypeSizes.field_offsets_of_type env j in
+            let offset_of_assertions =
+              match offsets with
+              | Inr msg ->
+                Ast.warning 
+                  (Printf.sprintf
+                    "No offsetof assertions for type %s because %s\ns"
+                    (ident_to_string j)
+                    msg)
+                  i.range;
+                []
+              | Inl offsets ->
+                offsets |>
+                List.collect
+                  (fun offset -> 
+                    if TypeSizes.is_alignment_field (fst offset)
+                    then []
+                    else [OffsetOfAssertion { 
+                            type_name = i;
+                            field_name = fst offset;
+                            offset = snd offset }])
+            in
             let t_j = with_dummy_range (Type_app j KindSpec []) in
-            match TypeSizes.size_of_typ env t_j with
-            | TypeSizes.Fixed n
-            | TypeSizes.WithVariableSuffix n ->
-             { type_name = i;
-               size = n }
-            | _ -> 
-              Ast.error 
-                (Printf.sprintf
-                  "Type %s is variable sized and cannot refine a C type %s"
-                  (ident_to_string j) (ident_to_string i))
-                i.range)
+            let sizeof_assertion =
+              match TypeSizes.size_of_typ env t_j with
+              | TypeSizes.Fixed n
+              | TypeSizes.WithVariableSuffix n ->
+                SizeOfAssertion {
+                  type_name = i;
+                  size = n }
+              | _ -> 
+                Ast.error 
+                  (Printf.sprintf
+                    "Type %s is variable sized and cannot refine a C type %s"
+                    (ident_to_string j) (ident_to_string i))
+                  i.range
+            in
+            sizeof_assertion::offset_of_assertions)
       in
       {
         includes = r.Ast.includes;
-        sizeof_assertions = sizeof_assertions
+        assertions = static_assertions
       }
 
 let no_static_asserts (sas: static_asserts) : Tot bool =
   Nil? sas.includes &&
-  Nil? sas.sizeof_assertions
+  Nil? sas.assertions
 
 let has_static_asserts (sas: static_asserts) : Tot bool =
   not (no_static_asserts sas)
@@ -84,10 +122,17 @@ let print_static_asserts (sas:static_asserts)
         |> List.map (fun i -> Printf.sprintf "#include \"%s\"" i)
         |> String.concat "\n"
     in
+    let print_static_assert (sa:static_assert) =
+      match sa with
+      | SizeOfAssertion sa ->
+        Printf.sprintf "C_ASSERT(sizeof(%s) == %d);" (ident_to_string sa.type_name) sa.size
+      | OffsetOfAssertion oa ->
+        Printf.sprintf "C_ASSERT(offsetof(%s, %s) == %d);" (ident_to_string oa.type_name) (ident_to_string oa.field_name) oa.offset
+    in
     let sizeof_assertions =
-        sas.sizeof_assertions
-        |> List.map (fun sa -> Printf.sprintf "C_ASSERT(sizeof(%s) == %d);" (ident_to_string sa.type_name) sa.size)
+        sas.assertions
+        |> List.map print_static_assert
         |> String.concat "\n"
     in
     Options.make_includes () ^
-    includes ^ "\n" ^ sizeof_assertions
+    includes ^ "\n#include <stddef.h>\n" ^ sizeof_assertions

src/3d/TypeSizes.fst

@@ -197,14 +197,15 @@ let size_and_alignment_of_atomic_field (env:env_t) (f:atomic_field)
     size, align
 
 #push-options "--warn_error -272"
+let alignment_prefix = Printf.sprintf "%salignment_padding" Ast.reserved_prefix
 let gen_alignment_ident
   : unit -> ML ident
   = let ctr : ref int = alloc 0 in
     fun () ->
       let next = !ctr in
       ctr := next + 1;
       with_range
-        (to_ident' (Printf.sprintf "%salignment_padding_%d" Ast.reserved_prefix next))
+        (to_ident' (Printf.sprintf "%s_%d" alignment_prefix next))
         dummy_range
 #pop-options
 
@@ -399,6 +400,38 @@ let rec size_and_alignment_of_field (env:env_t)
       let f = { f with v = SwitchCaseField swc field_name } in
       f, size, alignment
 
+let field_offsets_of_type (env:env_t) (typ:ident)
+: ML (either (list (ident & int)) string)
+= let ge = Binding.global_env_of_env (fst env) in
+  match GlobalEnv.fields_of_type ge typ with
+  | None ->
+    Inr <| Printf.sprintf "No fields for type %s" (ident_to_string typ)
+  | Some fields ->
+    let rec field_offsets (current_offset:int) (acc:list (ident & int)) (fields:list field)
+    : ML (either (list (ident & int)) string)
+    = match fields with
+      | [] -> Inl <| List.rev acc
+      | field :: fields ->
+        let _, size, _ = size_and_alignment_of_field env false typ field in
+        let id =
+          match field.v with
+          | AtomicField af -> af.v.field_ident
+          | RecordField _ id
+          | SwitchCaseField _ id -> id
+        in
+        match size with
+        | Fixed n ->
+          let next_offset = n + current_offset in
+          field_offsets next_offset ((id, current_offset) :: acc) fields
+
+        | WithVariableSuffix _
+        | Variable ->
+          Inl <| List.rev ((id, current_offset) :: acc)
+    in
+    field_offsets 0 [] fields
+
+let is_alignment_field (fieldname:ident) =
+  Utils.string_starts_with (ident_to_string fieldname) alignment_prefix
 
 let decl_size_with_alignment (env:env_t) (d:decl)
   : ML decl
@@ -433,12 +466,29 @@ let decl_size_with_alignment (env:env_t) (d:decl)
     | ExternFn _ _ _
     | ExternProbe _ -> d
 
+let idents_of_decl (d:decl) =
+  match d.d_decl.v with
+  | ModuleAbbrev i _
+  | Define i _ _ 
+  | TypeAbbrev _ i 
+  | Enum _ i _
+  | ExternFn i _ _
+  | ExternProbe i -> [i]
+  | Record names _ _ _
+  | CaseType names _ _
+  | OutputType { out_typ_names = names } 
+  | ExternType names -> [names.typedef_name; names.typedef_abbrev]
+
 let size_of_decls (genv:B.global_env) (senv:size_env) (ds:list decl) =
-  let env =
-    B.mk_env genv, senv in
-    // {senv with sizes = H.create 10} in
+  let env = B.mk_env genv, senv in
   let ds = List.map (decl_size_with_alignment env) ds in
+  let ge = B.global_env_of_env (fst env) in
+  ds |> List.iter (fun d ->
+  idents_of_decl d |> List.iter (fun i ->
+  match H.try_find ge.ge_h i.v with
+  | None -> ()
+  | Some (_, attrs) ->  H.insert ge.ge_h i.v (d, attrs)));
   ds
 
 let finish_module en mname e_and_p =
-  e_and_p |> snd |> List.iter (H.remove en)
+  e_and_p |> snd |> List.iter (H.remove en)

src/3d/TypeSizes.fsti

@@ -40,6 +40,12 @@ val size_of_typ (env:env_t) (t:typ)
 val value_of_const_expr (env:env_t) (e:expr)
   : ML (option (either bool (integer_type & int)))
 
+val field_offsets_of_type (env:env_t) (typ:ident)
+: ML (either (list (ident & int)) string)
+
+val is_alignment_field (fieldname:ident)
+: ML bool
+
 val size_of_decls (env:B.global_env) (senv:size_env) (d:list decl)
   : ML (list decl)
 

src/3d/Utils.fst

@@ -0,0 +1,29 @@
+module Utils
+inline_for_extraction
+let valid_string
+  (valid: (string -> Tot bool))
+: Tot Type0
+= (s: string { valid s == true })
+
+let always_valid (_: string) : Tot bool = true
+
+let starts_with_capital (s: string) : Tot bool =
+  String.length s >= 1 &&
+  begin let first = String.sub s 0 1 in
+    String.compare first "A" >= 0 && String.compare first "Z" <= 0
+  end
+
+let ends_with (s:string) (suffix:string) : bool =
+  let l = String.length s in
+  let sl = String.length suffix in
+  if sl > l || sl = 0
+  then false
+  else let suffix' = String.sub s (l - sl) sl in
+       suffix = suffix'
+
+let string_starts_with (big small: string) : Tot bool =
+  let small_len = String.length small in
+  if String.length big < small_len
+  then false
+  else String.sub big 0 small_len = small
+

src/3d/tests/modules/src/Foobar.h

@@ -1,4 +1,8 @@
+#include <stdint.h>
 #ifndef C_ASSERT
 #define C_ASSERT(e) typedef char __C_ASSERT__[(e)?1:-1]
 #endif
-typedef char CIRCLE[20];
+typedef struct _CIRCLE {
+    uint32_t p[4];
+    uint32_t radius;
+} CIRCLE;