adding some tests, very early beginnings of Pulse.Lib.C support library, etc.

Author: nikswamy

build.sh

@@ -24,6 +24,12 @@ if ! [[ -x "$HERE/external/pulse/out/lib/pulse/pulse.cmxs" ]]; then
   make -C $HERE/external/pulse -j$(nproc) ADMIT=1 FSTAR_EXE=$(realpath $HERE/external/FStar/bin/fstar.exe)
 fi
 
+
+if ! [[ -x "./include/pulse/_cache/Pulse.Lib.C.Int32.fst.checked" ]]; then
+  echo "Building Pulse.Lib.C libraries"
+  make -C $HERE/include/pulse -j$(nproc)
+fi
+
 if [[ -x "$CLANG_BIN/c2pulse" ]]; then
   echo "C2Pulse exists in $CLANG_BIN!"
   echo "Rebuilding existing project!"

include/pulse/Makefile

@@ -0,0 +1,5 @@
+
+PULSE_ROOT ?= ../../external/pulse
+FSTAR_EXE ?= ../../external/FStar/bin/fstar.exe
+
+include $(PULSE_ROOT)/mk/test.mk

include/pulse/Pulse.Lib.C.Int32.fst

@@ -0,0 +1,11 @@
+module Pulse.Lib.C.Int32
+open FStar.Int32
+module I32 = FStar.Int32
+
+let int32 = FStar.Int32.t
+let as_int (x: I32.t) : int = I32.v x
+let fits (op : int -> int -> int) (vx vy : int) : prop =
+  FStar.Int32.fits (op vx vy)
+let min_int32 = FStar.Int.min_int I32.n
+let max_int32 = FStar.Int.max_int I32.n
+let (+^) = FStar.Int32.add

include/pulse/fstar.include

@@ -0,0 +1 @@
+_cache

run.sh

@@ -10,6 +10,7 @@ C_STD="-std=c23"
 C2PULSE="$(realpath $HERE/external/llvm-project/build/bin/c2pulse)"
 FSTAR_BIN="$(realpath $HERE/external/FStar/bin/fstar.exe)"
 PULSE_DIR="$(realpath $HERE/external/pulse/out/lib/pulse)"
+PULSE_LIB_C_DIR="$(realpath $HERE/include/pulse)"
 
 # Check input
 if [ "$#" -lt 1 ]; then
@@ -96,5 +97,6 @@ done
 # Run fstar on all files at once
 exec "$FSTAR_BIN" \
   --include "$PULSE_DIR" \
+  --include "$PULSE_LIB_C_DIR" \
   --query_stats --z3version 4.13.3 \
   "${SRC_FILES[@]}" 

run_fstar.sh

@@ -4,6 +4,7 @@ set -euo pipefail
 HERE=$(dirname $0)
 FSTAR_BIN="$(realpath $HERE/external/FStar/bin/fstar.exe)"
 PULSE_DIR="$(realpath $HERE/external/pulse/out/lib/pulse)"
+AUX_LIBS="$(realpath $HERE/include/pulse)"
 
 if [ $# -lt 1 ]; then
   echo "Usage: $0 <source_file.fst> [additional F* args]"
@@ -13,4 +14,4 @@ fi
 SRC_FILE="$1"
 shift
 
-exec "$FSTAR_BIN" --include "$PULSE_DIR" --z3version 4.13.3 "$SRC_FILE" "$@"
+exec "$FSTAR_BIN" --include "$PULSE_DIR" --include "$AUX_LIBS" --z3version 4.13.3 "$SRC_FILE" "$@"

test/Cfg.fst.config.json

@@ -7,6 +7,7 @@
     "--z3version", "4.13.3"
   ],
   "include_dirs": [
-    "../external/pulse/out/lib/pulse"
+    "../external/pulse/out/lib/pulse",
+    "../include/pulse"
   ]
 }

…nspiler/c/general/pulse_tutorial_intro.c test/pulse_tutorial_intro.ctest-transpiler/c/general/pulse_tutorial_intro.c renamed to test/pulse_tutorial_intro.c test-transpiler/c/general/pulse_tutorial_intro.c renamed to test/pulse_tutorial_intro.c

@@ -1,29 +1,31 @@
 #include <stdint.h>
 #include <stdlib.h>
-#include "../pulse_macros.h"
+#include "../include/PulseMacros.h"
 
 REQUIRES("x |-> 'i")
 REQUIRES("pure FStar.Int32.(fits (v 'i + 1))")
-ENSURES("x |-> ('i + 1)")
+ENSURES("exists* j. (x |-> j) ** pure FStar.Int32.(v 'i + 1 == v j)")
 void incr (int *x)
 {
     *x = *x + 1;
 }
 
-ERASED_ARG(i)
+ERASED_ARG(#i:_)
 REQUIRES(x |-> i)
 REQUIRES(pure FStar.Int32.(fits (v i + 1)))
-ENSURES(x |-> (i + 1))
+ENSURES("exists* j. (x |-> j) ** pure FStar.Int32.(v i + 1 == v j)")
 void incr_explicit_i (int *x)
 {
     *x = *x + 1;
 }
 
-ERASED_ARG(i)
-ERASED_ARG(j)
-REQUIRES(x |-> i ** y |-> j)
+ERASED_ARG(#i:_)
+ERASED_ARG(#j:_)
+REQUIRES(x |-> i)
+REQUIRES(y |-> j)
 REQUIRES(pure FStar.Int32.(fits (v i + 1)))
-ENSURES(x |-> (i + 1) ** y |-> j)
+ENSURES("exists* j. (x |-> j) ** pure FStar.Int32.(v i + 1 == v j)")
+ENSURES(y |-> j)
 void incr_frame(int *x, int *y)
 {
     incr(x);

…ranspiler/c/general/pulse_tutorial_ref.c test/pulse_tutorial_ref.ctest-transpiler/c/general/pulse_tutorial_ref.c renamed to test/pulse_tutorial_ref.c test-transpiler/c/general/pulse_tutorial_ref.c renamed to test/pulse_tutorial_ref.c

@@ -1,19 +1,19 @@
 #include <stdint.h>
 #include <stdlib.h>
-#include "../pulse_macros.h"
+#include "../include/PulseMacros.h"
 
 REQUIRES("r |-> 'v")
-RETURNS(v)
+RETURNS(v:Pulse.Lib.C.Int32.int32)
 ENSURES("r |-> 'v")
 ENSURES("pure (v == 'v)")
 int value_of(int *r)
 {
     return *r;
 }
 
-ERASED_ARG(w)
+ERASED_ARG(#w:erased _)
 REQUIRES(r |-> w)
-RETURNS(v)
+RETURNS(v:Pulse.Lib.C.Int32.int32)
 ENSURES(r |-> w)
 ENSURES(pure (v == w))
 int value_of_explicit(int *r)
@@ -35,44 +35,45 @@ void assign_alt(int *r, int v)
     *r = v;
 }
 
-ERASED_ARG(w)
+ERASED_ARG(#w:erased _)
 REQUIRES(r |-> w)
-REQUIRES(pure FStar.Int32.(fits (v w + n)))
-ENSURES(exists* ww. r |-> ww ** pure FStar.Int32.(v ww == v w + n))
+REQUIRES(pure Pulse.Lib.C.Int32.(fits (+) (as_int w) (as_int n)))
+ENSURES(exists* ww. (r |-> ww) ** pure Pulse.Lib.C.Int32.(as_int ww == as_int w + as_int n))
 void add(int *r, int n)
 {
     *r = *r + n;
 }
 
-ERASED_ARG(w : FStar.Int32.t { FStar.Int32.(fits (v w + n)) })
+ERASED_ARG(#w : erased _ { Pulse.Lib.C.Int32.(fits (+) (as_int w) (as_int n)) })
 REQUIRES(r |-> w)
-ENSURES(r |-> FStar.Int32.(w +^ n))
+ENSURES(r |-> Pulse.Lib.C.Int32.(w +^ n))
 void add_alt(int *r, int n)
 {
     *r = *r + n;
 }
 
-ERASED_ARG(w : FStar.Int32.t { FStar.Int32.fits(4 * v w) })
+ERASED_ARG(#w : erased _ { Pulse.Lib.C.Int32.(fits op_Multiply 4 (as_int w)) })
 REQUIRES(r |-> w)
-ENSURES(exists* ww. r |-> ww ** pure FStar.Int32.(v ww == 4 * v w))
+ENSURES(exists* ww. (r |-> ww) ** pure Pulse.Lib.C.Int32.(as_int ww == 4 `op_Multiply` as_int w))
 void quadruple(int *r)
 {
     add(r, *r);
     add(r, *r);
 }
 
-ERASED_ARG(w:FStar.Int32.t)
+
+ERASED_ARG(#w:erased _)
 ERASED_ARG(p:perm)
 REQUIRES(x |-> Frac p w)
-RETURNS(i)
+RETURNS(i:Pulse.Lib.C.Int32.int32)
 ENSURES(x |-> Frac p w)
 ENSURES(pure (i == w))
 int value_of_perm(int *x)
 {
     return *x;
 }
 
-ERASED_ARG(v)
+ERASED_ARG(#v:erased _)
 ERASED_ARG(p:perm)
 REQUIRES(x |-> Frac p v)
 ENSURES(x |-> Frac (p /. 2.0R) v)
@@ -82,8 +83,9 @@ void share_ref(int *x)
     LEMMA(share(x));
 }
 
-ERASED_ARG(v0)
-ERASED_ARG(v1)
+
+ERASED_ARG(#v0:erased _)
+ERASED_ARG(#v1:erased _)
 ERASED_ARG(p:perm)
 REQUIRES(x |-> Frac (p /. 2.0R) v0)
 REQUIRES(x |-> Frac (p /. 2.0R) v1)
@@ -94,7 +96,8 @@ void gather_ref(int *x)
     LEMMA(gather(x));
 }
 
-ERASED_ARG(v)
+
+ERASED_ARG(#v:erased _)
 ERASED_ARG(p:perm)
 REQUIRES(x |-> Frac p v)
 REQUIRES(pure (~(p <=. 1.0R)))
@@ -105,10 +108,10 @@ void max_perm (int *x)
     LEMMA(unreachable());
 }
 
-ERASED_ARG(v)
+ERASED_ARG(#v:erased _)
 ERASED_ARG(p:perm)
 REQUIRES(r |-> Frac p v)
-RETURNS(s)
+RETURNS(s: ref Pulse.Lib.C.Int32.int32)
 ENSURES(s |-> Frac (p /. 2.0R) v)
 ENSURES(s |-> Frac (p /. 2.0R) v)
 ENSURES(pure (s == r))
@@ -118,29 +121,33 @@ int* alias_ref(int *r)
     return r;
 }
 
-ERASED_ARG(vr)
+
+ERASED_ARG(#vr:erased _)
 REQUIRES(r |-> vr)
-ENSURES(exists* w. r |-> w ** pure FStar.Int32.(v w == v vr + 1))
+REQUIRES(pure Pulse.Lib.C.Int32.(fits (+) (as_int vr) 1))
+ENSURES(exists* w. (r |-> w) ** pure Pulse.Lib.C.Int32.(as_int w == as_int vr + 1))
 int incr (int *r)
 {
     *r = *r + 1;
 }
 
-
-RETURNS(i)
-ENSURES(pure (i == 1l))
+/**
+REQUIRES(emp)
+RETURNS(i:Pulse.Lib.C.Int32.int32)
+ENSURES(pure Pulse.Lib.C.Int32.(as_int i == 1))
 int one()
 {
     int i = 0;
     incr(&i);
     return i;
 }
 
+/*
 EXPECT_FAILURE(19)
 RETURNS(s)
 ENSURES(s |-> 0l)
 int* refs_are_scoped()
 {
     int s = 0;
     return &s;
-}
+}*/