Merge commit 'fa2690c8' into taramana_tot_serializer

src/3d/Ast.fst

@@ -508,8 +508,16 @@ and switch_case = expr & list case
 
 
 [@@ PpxDerivingYoJson ]
+noeq
+type probe_entrypoint = {
+  probe_ep_fn: ident;
+  probe_ep_length:expr;
+}
+
+[@@ PpxDerivingYoJson ]
+noeq
 type attribute =
-  | Entrypoint
+  | Entrypoint: (probe: option probe_entrypoint) -> attribute
   | Aligned
 
 /// Typedefs are given 2 names by convention and can be tagged as an
@@ -607,7 +615,16 @@ let prog = list decl & option type_refinement
 (** Entrypoint and export definitions *)
 
 let has_entrypoint (l:list attribute) : Tot bool =
-  Some? (List.Tot.tryFind (function Entrypoint -> true | _ -> false) l)
+  List.Tot.existsb Entrypoint? l
+
+let rec get_entrypoint_probes' (l: list attribute) (accu: list probe_entrypoint) : Tot (list probe_entrypoint) =
+  match l with
+  | [] -> List.Tot.rev accu
+  | Entrypoint (Some probe) :: q -> get_entrypoint_probes' q (probe :: accu)
+  | _ :: q -> get_entrypoint_probes' q accu
+
+let get_entrypoint_probes (l: list attribute) : Tot (list probe_entrypoint) =
+  get_entrypoint_probes' l []
 
 let is_entrypoint_or_export d = match d.d_decl.v with
   | Record names _ _ _

src/3d/Binding.fst

@@ -116,22 +116,26 @@ let format_identifier (e:env) (i:ident) : ML ident =
     error msg i.range
 
 let add_global (e:global_env) (i:ident) (d:decl) (t:either decl_attributes macro_signature) : ML unit =
-  let insert k v = H.insert e.ge_h k v in
+  let insert k v =
+    Options.debug_print_string
+      (Printf.sprintf "Inserting global: %s\n" (ident_to_string k));
+    H.insert e.ge_h k.v v
+  in
 
   check_shadow e.ge_h i d.d_decl.range;
   let env = mk_env e in
   let i' = format_identifier env i in
-  insert i.v (d, t);
-  insert i'.v (d, t);
+  insert i (d, t);
+  insert i' (d, t);
   match typedef_names d with
   | None -> ()
   | Some td ->
     if td.typedef_abbrev.v <> i.v
     then begin
       check_shadow e.ge_h td.typedef_abbrev d.d_decl.range;
       let abbrev = format_identifier env td.typedef_abbrev in
-      insert td.typedef_abbrev.v (d, t);
-      insert abbrev.v (d, t)
+      insert td.typedef_abbrev (d, t);
+      insert abbrev (d, t)
     end
 
 let add_local (e:env) (i:ident) (t:typ) : ML unit =
@@ -1703,6 +1707,62 @@ let rec check_output_field (ge:global_env) (fld:out_field) : ML unit =
 and check_output_fields (ge:global_env) (flds:list out_field) : ML unit =
   List.iter (check_output_field ge) flds
 
+let check_entrypoint_probe_length_type
+  (e: env)
+  (t: typ)
+: ML bool
+= if eq_typ e t tuint8
+  then true
+  else if eq_typ e t tuint16
+  then true
+  else eq_typ e t tuint32
+
+let is_sizeof_not_this (l: expr) : Tot bool =
+  match l.v with
+  | App SizeOf [{v=Identifier _}] ->
+      true
+  | _ -> false
+
+let check_entrypoint_probe_length
+  (e: global_env)
+  (l: expr)
+: ML expr
+= if
+    Constant? l.v ||
+    Identifier? l.v
+  then
+    let lenv = mk_env e in
+    let (l', t') = check_expr lenv l in
+    if check_entrypoint_probe_length_type lenv t'
+    then l'
+    else error ("entrypoint probe: expected UINT32, got " ^ print_typ t') l.range
+  else if is_sizeof_not_this l
+  then
+    let lenv = mk_env e in
+    let (l', t') = check_expr lenv l in
+    l'
+  else error ("entrypoint probe: expected a constant, #define'd identifier, or sizeof; got " ^ print_expr l) l.range
+
+let check_attribute
+  (e: global_env)
+  (a: attribute)
+: ML attribute
+= match a with
+  | Entrypoint (Some p) ->
+    Entrypoint (Some ({
+      p with probe_ep_length = check_entrypoint_probe_length e p.probe_ep_length
+    }))
+  | _ -> a
+
+let check_typedef_names
+  (e: global_env)
+  (tdnames: Ast.typedef_names)
+: ML Ast.typedef_names
+= {
+    tdnames with
+      typedef_attributes = List.map (check_attribute e) tdnames.typedef_attributes
+}
+
 let bind_decl (e:global_env) (d:decl) : ML decl =
   match d.d_decl.v with
   | ModuleAbbrev i m -> d
@@ -1774,9 +1834,11 @@ let bind_decl (e:global_env) (d:decl) : ML decl =
     d
 
   | Record tdnames params where fields ->
+    let tdnames = check_typedef_names e tdnames in
     elaborate_record_decl e tdnames params where fields d.d_decl.range d.d_decl.comments d.d_exported
 
   | CaseType tdnames params switch ->
+    let tdnames = check_typedef_names e tdnames in
     let env = { mk_env e with this=Some tdnames.typedef_name } in
     check_params env params;
     let switch = check_switch check_field env switch in

src/3d/Deps.fst

@@ -180,6 +180,15 @@ let scan_deps (fn:string) : ML scan_deps_t =
     | Some (Inr i) -> maybe_dep i
     | _ -> [] in
 
+  let deps_of_attribute (a:attribute) : ML (list string) = match a with
+    | Entrypoint (Some p) -> maybe_dep p.probe_ep_fn `List.Tot.append` deps_of_expr p.probe_ep_length
+    | _ -> []
+  in
+
+  let deps_of_typedef_names (td: typedef_names) : ML (list string) =
+    List.collect deps_of_attribute td.typedef_attributes
+  in
+
   let deps_of_decl (d:decl) : ML (list string) =
     match d.d_decl.v with
     | ModuleAbbrev i m ->
@@ -189,11 +198,13 @@ let scan_deps (fn:string) : ML scan_deps_t =
     | Define _ (Some t) _ -> deps_of_typ t
     | TypeAbbrev t _ -> deps_of_typ t
     | Enum _base_t _ l -> List.collect deps_of_enum_case l
-    | Record _ params wopt flds ->
+    | Record tdnames params wopt flds ->
+      (deps_of_typedef_names tdnames)@
       (deps_of_params params)@
       (deps_of_opt deps_of_expr wopt)@
       (List.collect deps_of_field flds)
-    | CaseType _ params sc ->
+    | CaseType tdnames params sc ->
+      (deps_of_typedef_names tdnames)@
       (deps_of_params params)@
       (deps_of_switch_case sc)
     | OutputType _

src/3d/Desugar.fst

@@ -378,11 +378,22 @@ and resolve_switch_case (env:qenv) (sc:switch_case) : ML switch_case = //case fi
   let e, l = sc in
   resolve_expr env e, List.map (resolve_case env) l
 
+let resolve_typedef_attribute (env: qenv) (a: attribute) : ML attribute =
+  match a with
+  | Entrypoint (Some p) ->
+    Entrypoint (Some ({
+      probe_ep_fn = resolve_ident env p.probe_ep_fn;
+      probe_ep_length = resolve_expr env p.probe_ep_length;
+    }))
+  | _ -> a
+
 let resolve_typedef_names (env:qenv) (td_names:typedef_names) : ML typedef_names =
-  { td_names with
+  {
     typedef_name = resolve_ident env td_names.typedef_name;
     typedef_abbrev = resolve_ident env td_names.typedef_abbrev;
-    typedef_ptr_abbrev = resolve_ident env td_names.typedef_ptr_abbrev }
+    typedef_ptr_abbrev = resolve_ident env td_names.typedef_ptr_abbrev;
+    typedef_attributes = List.map (resolve_typedef_attribute env) td_names.typedef_attributes;
+  }
 
 let resolve_enum_case (env:qenv) (ec:enum_case) : ML enum_case =
   match ec with

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/Simplify.fst

@@ -156,6 +156,37 @@ let rec simplify_out_fields (env:T.env_t) (flds:list out_field) : ML (list out_f
     | Out_field_anon flds is_union ->
       Out_field_anon (simplify_out_fields env flds) is_union) flds
 
+let check_probe_size_range (e: expr) : ML unit =
+  match e.v with
+  | Constant (Int t n) ->
+    if integer_type_leq t UInt32
+    then ()
+    else
+      error
+        (Printf.sprintf "entrypoint probe: computed sizeof(%s) == %d, exceeds unsigned 32-bit integer range"
+          (print_expr e)
+          n
+        )
+      e.range
+  | App SizeOf _ -> error "check_probe_size_range: sizeof should have been eliminated already" e.range
+  | _ -> ()
+
+let simplify_attribute (env: T.env_t) (attr: attribute) : ML attribute =
+  match attr with
+  | Entrypoint (Some p) ->
+    let e' = simplify_expr env p.probe_ep_length in
+    check_probe_size_range e';
+    Entrypoint (Some ({
+      p with
+        probe_ep_length = e';
+    }))
+  | _ -> attr
+
+let simplify_typedef_names (env: T.env_t) (tdnames: typedef_names) : ML typedef_names =
+  { tdnames with
+      typedef_attributes = List.map (simplify_attribute env) tdnames.typedef_attributes;
+  }
+
 let simplify_decl (env:T.env_t) (d:decl) : ML decl =
   match d.d_decl.v with
   | ModuleAbbrev _ _ -> d
@@ -172,12 +203,14 @@ let simplify_decl (env:T.env_t) (d:decl) : ML decl =
     decl_with_v d (Enum t i cases)
 
   | Record tdnames params wopt fields ->
+    let tdnames = simplify_typedef_names env tdnames in
     let params = List.map (fun (t, i, q) -> simplify_typ env t, i, q) params in
     let fields = List.map (simplify_field env) fields in
     let wopt = match wopt with | None -> None | Some w -> Some (simplify_expr env w) in
     decl_with_v d (Record tdnames params wopt fields)
 
   | CaseType tdnames params switch ->
+    let tdnames = simplify_typedef_names env tdnames in
     let params = List.map (fun (t, i, q) -> simplify_typ env t, i, q) params in 
     let switch = simplify_switch_case env switch in
     decl_with_v d (CaseType tdnames params switch)