C._zero_for_deref -> Pulse.Lib.Pervasives._zero_for_deref

Author: tahina-pro

lib/pulse/lib/Pulse.Lib.Pervasives.fst

@@ -179,3 +179,9 @@ instance duplicable_slprop_ref_pts_to x y : duplicable (slprop_ref_pts_to x y) =
 
 ghost fn dup_emp () : duplicable_f emp = { }
 instance duplicable_emp : duplicable emp = { dup_f = dup_emp }
+
+// An index to be used as argument to `Pulse.Lib.Array.Core.mask_read` (and derivatives) so that
+// b[_zero_for_deref] is turned into *b
+// Special treatment: marked to not be emitted to C
+// in CStarToC11.builtin_names
+let _zero_for_deref : FStar.UInt32.t = 0ul

mk/test.mk

@@ -104,7 +104,7 @@ $(OUTPUT_DIR)/$(subst .,_,%).krml:
 	$(call msg, "EXTRACT", $(basename $(notdir $@)))
 	$(FSTAR) $< --codegen krml --extract_module $(subst .fst.checked,,$(notdir $<))
 
-$(OUTPUT_DIR)/%.c: $(OUTPUT_DIR)/%.krml
+$(OUTPUT_DIR)/%.c: $(OUTPUT_DIR)/%.krml	$(OUTPUT_DIR)/Pulse_Lib_Pervasives.krml
 	$(call msg, "KRML", $(basename $(notdir $@)))
 	if ! which $(KRML_EXE); then echo "krml ($(KRML_EXE)) not found" >&2; false; fi
 	$(KRML_EXE) $(KRML_FLAGS) -skip-makefiles -header=$(PULSE_ROOT)/mk/krmlheader -bundle $*=* -skip-linking $+ -tmpdir $(OUTPUT_DIR)

share/pulse/examples/c/PulsePointStruct.fst

@@ -20,7 +20,6 @@ open Pulse.Lib.Pervasives
 open Pulse.C.Types
 
 module U32 = FStar.UInt32
-// module C = C // for _zero_for_deref
 
 
 fn swap (#v1 #v2: Ghost.erased U32.t) (r1 r2: ref (scalar U32.t))

src/extraction/ExtractPulse.fst

@@ -56,7 +56,7 @@ let head_and_args (e : mlexpr) : mlexpr & list mlexpr =
   in
   aux [] e
 
-let zero_for_deref = EQualified (["C"], "_zero_for_deref")
+let zero_for_deref = EQualified (["Pulse"; "Lib"; "Pervasives"], "_zero_for_deref")
 
 type goto_env_elem =
   | ReturnLabel

src/extraction/ExtractPulseC.fst

@@ -135,6 +135,8 @@ let my_types () = register_pre_translate_type begin fun env t ->
   | _ -> raise NotSupportedByKrmlExtension
 end
 
+let zero_for_deref = EQualified (["Pulse"; "Lib"; "Pervasives"], "_zero_for_deref")
+
 let my_exprs () = register_pre_translate_expr begin fun env e ->
   match e.expr with
   | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ _ (* typedef *) ])
@@ -197,7 +199,7 @@ let my_exprs () = register_pre_translate_expr begin fun env e ->
     ->
       EAddrOf (EField (
         TQualified (Option.must (lident_of_string struct_name)),
-        EBufRead (translate_expr env r, EQualified (["C"], "_zero_for_deref")),
+        EBufRead (translate_expr env r, zero_for_deref),
         field_name))
 
   | MLE_App ({expr=MLE_TApp ({expr=MLE_Name p}, (t :: _))},
@@ -212,17 +214,17 @@ let my_exprs () = register_pre_translate_expr begin fun env e ->
     ->
       EAddrOf (EField (
         translate_type env t,
-        EBufRead (translate_expr env r, EQualified (["C"], "_zero_for_deref")),
+        EBufRead (translate_expr env r, zero_for_deref),
         field_name))
 
   | MLE_App ({expr=MLE_TApp ({expr=MLE_Name p}, _)}, [_ (* value *) ; _ (* perm *) ; r])
     when string_of_mlpath p = "Pulse.C.Types.Scalar.read0" ->
-      EBufRead (translate_expr env r, EQualified (["C"], "_zero_for_deref"))
+      EBufRead (translate_expr env r, zero_for_deref)
 
   | MLE_App ({expr=MLE_TApp ({expr=MLE_Name p}, _)}, [_ (* value *); r; x])
     when string_of_mlpath p = "Pulse.C.Types.Scalar.write" ->
       EAssign (
-        EBufRead (translate_expr env r, EQualified (["C"], "_zero_for_deref")),
+        EBufRead (translate_expr env r, zero_for_deref),
         translate_expr env x)
 
   | MLE_App ({expr=MLE_TApp ({expr=MLE_Name p}, _)}, [
@@ -235,8 +237,8 @@ let my_exprs () = register_pre_translate_expr begin fun env e ->
     ])
     when string_of_mlpath p = "Pulse.C.Types.Base.copy" ->
       EAssign (
-        EBufRead (translate_expr env dst, EQualified (["C"], "_zero_for_deref")),
-        EBufRead (translate_expr env src, EQualified (["C"], "_zero_for_deref")))
+        EBufRead (translate_expr env dst, zero_for_deref),
+        EBufRead (translate_expr env src, zero_for_deref))
 
   | MLE_App ({expr=MLE_TApp ({expr=MLE_Name p}, _)}, [
       _ (* typedef *);
@@ -268,7 +270,7 @@ let my_exprs () = register_pre_translate_expr begin fun env e ->
     ])
     when string_of_mlpath p = "Pulse.C.Types.Array.array_ref_of_base" ->
       // this is not a true read, this is how Karamel models arrays decaying into pointers
-      EBufRead (translate_expr env r, EQualified (["C"], "_zero_for_deref"))
+      EBufRead (translate_expr env r, zero_for_deref)
 
   | MLE_App ({expr=MLE_TApp ({expr=MLE_Name p}, _)}, [
       _ (* typedef *);