Merge pull request #118 from project-everest/nik_3d_probe

Support for validating pointer-rich formats given a probe to check for pointer validity

EverParse.fst.config.json

@@ -0,0 +1,16 @@
+{
+    "fstar_exe": "fstar.exe",
+    "options": [
+      "--max_fuel", "0",
+      "--max_ifuel", "2",
+      "--initial_ifuel", "2"
+    ],
+    "include_dirs": [
+      "./src/lowparse", 
+      "${KRML_HOME}/krmllib",
+      "${KRML_HOME}/krmllib/obj",
+      "./src/3d",
+      "./src/3d/prelude"
+    ]
+  }
+

src/3d/Ast.fst

@@ -468,6 +468,14 @@ type field_array_t =
   | FieldString of (option expr)
   | FieldConsumeAll // [:consume-all]
 
+[@@ PpxDerivingYoJson ]
+noeq
+type probe_call = {
+  probe_fn:option ident;
+  probe_length:expr;
+  probe_dest:ident
+}
+
 [@@ PpxDerivingYoJson ]
 noeq
 type atomic_field' = {
@@ -477,7 +485,8 @@ type atomic_field' = {
   field_array_opt: field_array_t;
   field_constraint:option expr; //refinement constraint
   field_bitwidth:option field_bitwidth_t;  //bits used for the field; elaborate from Inl to Inr
-  field_action:option (action & bool); //boo indicates if the action depends on the field value
+  field_action:option (action & bool); //bool indicates if the action depends on the field value
+  field_probe:option probe_call; //set in case this field has to be probed then validated
 }
 
 and atomic_field = with_meta_t atomic_field'
@@ -565,6 +574,7 @@ type decl' =
   | OutputType : out_typ -> decl'
   | ExternType : typedef_names -> decl'
   | ExternFn   : ident -> typ -> list param -> decl'
+  | ExternProbe : ident -> decl'
 
 [@@ PpxDerivingYoJson ]
 noeq
@@ -780,6 +790,7 @@ let puint8 = mk_prim_t "PUINT8"
 let tuint16 = mk_prim_t "UINT16"
 let tuint32 = mk_prim_t "UINT32"
 let tuint64 = mk_prim_t "UINT64"
+let tcopybuffer = mk_prim_t "EVERPARSE_COPY_BUFFER_T"
 let tunknown = mk_prim_t "?"
 let unit_atomic_field rng = 
     let dummy_identifier = with_range (to_ident' "_empty_") rng in
@@ -790,7 +801,8 @@ let unit_atomic_field rng =
          field_array_opt=FieldScalar;
          field_constraint=None;
          field_bitwidth=None;
-         field_action=None
+         field_action=None;
+         field_probe=None
         } in
     with_range f rng
 
@@ -896,11 +908,13 @@ let subst_decl' (s:subst) (d:decl') : ML decl' =
     CaseType names (subst_params s params) (subst_switch_case s cases)
   | OutputType _
   | ExternType _
-  | ExternFn _ _ _ -> d
+  | ExternFn _ _ _ 
+  | ExternProbe _ -> d
 let subst_decl (s:subst) (d:decl) : ML decl = decl_with_v d (subst_decl' s d.d_decl.v)
 
 (*** Printing the source AST; for debugging only **)
-let print_constant (c:constant) =
+let print_constant (c:constant) =
+
   let print_tag = function
     | UInt8 -> "uy"
     | UInt16 -> "us"
@@ -1108,13 +1122,18 @@ and print_atomic_field (f:atomic_field) : ML string =
     | FieldConsumeAll -> Printf.sprintf "[:consume-all]"
   in
   let sf = f.v in
-    Printf.sprintf "%s%s %s%s%s%s;"
+    Printf.sprintf "%s%s %s%s%s%s%s;"
       (if sf.field_dependence then "dependent " else "")
       (print_typ sf.field_type)
       (print_ident sf.field_ident)
       (print_bitfield sf.field_bitwidth)
       (print_array sf.field_array_opt)
       (print_opt sf.field_constraint (fun e -> Printf.sprintf "{%s}" (print_expr e)))
+      (print_opt sf.field_probe
+        (fun p -> Printf.sprintf "probe %s (length=%s, destination=%s)"
+          (print_opt p.probe_fn print_ident)
+          (print_expr p.probe_length)
+          (print_ident p.probe_dest)))
 
 and print_switch_case (s:switch_case) : ML string =
   let head, cases = s in
@@ -1177,7 +1196,8 @@ let print_decl' (d:decl') : ML string =
                     (ident_to_string td.typedef_ptr_abbrev)
   | OutputType out_t -> "Printing for output types is TBD"
   | ExternType _ -> "Printing for extern types is TBD"
-  | ExternFn _ _ _ -> "Printing for extern functions is TBD"
+  | ExternFn _ _ _
+  | ExternProbe _ -> "Printing for extern functions is TBD"
 
 let print_decl (d:decl) : ML string =
   match d.d_decl.comments with
@@ -1269,11 +1289,11 @@ let decl'_prune_actions
   | OutputType _
   | ExternType _
   | ExternFn _ _ _
-  -> d
-  | Record names params where fields
-  -> Record names params where (record_prune_actions fields)
-  | CaseType names params cases
-  -> CaseType names params (switch_case_prune_actions cases)
+  | ExternProbe _ -> d
+  | Record names params where fields ->
+    Record names params where (record_prune_actions fields)
+  | CaseType names params cases ->
+    CaseType names params (switch_case_prune_actions cases)
 
 let decl_prune_actions
   (d: decl)