Merge branch 'master' into lef/fix-694-eurydice

Author: elefthei

.github/workflows/ci.yml

@@ -245,12 +245,72 @@ jobs:
           export CC=${{matrix.cc}}
           make -kj$(nproc) -C krmllib/dist/generic -f Makefile.basic
 
+  build-and-test-pulse:
+    runs-on: ubuntu-latest
+    needs: build-deps
+    steps:
+      - name: Setup ocaml
+        uses: ocaml/setup-ocaml@v3
+        with:
+           ocaml-compiler: 5.3.0
+
+      # Note, we prefer to restore the -fstar2 cache, but if it doesn't exist,
+      # we restore the latest normal one.
+      - name: Restore OPAM state
+        uses: actions/cache/restore@v4
+        with:
+          fail-on-cache-miss: true
+          path: _opam
+          key: opam-${{ runner.os }}-${{ runner.arch }}-fstar2-${{ github.run_id }}
+          restore-keys: |
+            opam-${{ runner.os }}-${{ runner.arch }}-fstar2-
+            opam-${{ runner.os }}-${{ runner.arch }}-
+
+      # Build F*, branch fstar2
+      - run: opam update
+      - run: opam pin -n fstar git+https://github.com/FStarLang/FStar#fstar2
+      - run: opam install fstar
+
+      # Save OPAM state, note fstar2- in key.
+      - name: Save OPAM state
+        uses: actions/cache/save@v4
+        with:
+          path: _opam
+          key: opam-${{ runner.os }}-${{ runner.arch }}-fstar2-${{ github.run_id }}
+
+      - name: Install Z3 with script
+        run: |
+          wget https://raw.githubusercontent.com/FStarLang/FStar/refs/heads/master/.scripts/get_fstar_z3.sh -O get_fstar_z3.sh
+          chmod +x get_fstar_z3.sh
+          ./get_fstar_z3.sh /usr/local/bin
+       # If these fail, stop right now.
+      - run: which z3-4.8.5
+      - run: which z3-4.13.3
+
+      - uses: actions/checkout@master
+        with:
+          path: karamel
+
+      - uses: actions/setup-node@v4
+        with:
+          node-version: 16
+
+      - run: echo "KRML_HOME=$(pwd)/karamel" >> $GITHUB_ENV
+
+      - name: Karamel CI (test-pulse)
+        working-directory: karamel
+        run: |
+          eval $(opam env)
+          export OCAMLRUNPARAM=b
+          make -kj$(nproc) test-pulse
+
   # A single no-op job to use for branch protection
   ciok:
     runs-on: ubuntu-latest
     if: ${{ cancelled() || contains(needs.*.result, 'cancelled') || contains(needs.*.result, 'failure') }}
     needs:
       - build-and-test
+      - build-and-test-pulse
       - build-krmllib
     steps:
       # Note: this only runs when a dependency fails. If they all succeed,

Makefile

@@ -56,6 +56,11 @@ clean:
 test: all
 	$(MAKE) -C test
 
+# This depends on minimal since fstar2 (with Pulse) is not expected
+# to be able to build krmllib.
+test-pulse: minimal
+	$(MAKE) -C test/pulse
+
 # Auto-detection
 pre:
 	@eval "$(FSTAR_OCAMLENV)" && \

test/pulse/.gitignore

@@ -0,0 +1 @@
+_output

test/pulse/ANF.expected.c

@@ -0,0 +1,20 @@
+/* krml header omitted for test repeatability */
+
+
+#include "ANF.h"
+
+extern krml_checked_int_t Prims_op_Addition(krml_checked_int_t x, krml_checked_int_t y);
+
+void ANF_test(void)
+{
+  krml_checked_int_t r = (krml_checked_int_t)0;
+  krml_checked_int_t __anf0 = r;
+  r = Prims_op_Addition(__anf0, (krml_checked_int_t)1);
+  krml_checked_int_t __anf01 = r;
+  r = Prims_op_Addition(__anf01, (krml_checked_int_t)1);
+  krml_checked_int_t __anf02 = r;
+  r = Prims_op_Addition(__anf02, (krml_checked_int_t)1);
+  krml_checked_int_t __anf03 = r;
+  r = Prims_op_Addition(__anf03, (krml_checked_int_t)1);
+}
+

test/pulse/ANF.fst

@@ -0,0 +1,13 @@
+module ANF
+
+#lang-pulse
+open Pulse
+
+fn test ()
+{
+  let mut r = 0;
+  r := !r + 1;
+  r := !r + 1;
+  r := !r + 1;
+  r := !r + 1;
+}

test/pulse/BangBang.expected.c

@@ -0,0 +1,23 @@
+/* krml header omitted for test repeatability */
+
+
+#include "BangBang.h"
+
+int32_t BangBang_modify_nested_ptr(int32_t **x)
+{
+  int32_t *__anf2 = *x;
+  int32_t *__anf01 = *x;
+  int32_t __anf1 = *__anf01;
+  *__anf2 = __anf1 + (int32_t)2;
+  int32_t *__anf03 = *x;
+  int32_t __anf11 = *__anf03;
+  return __anf11 + (int32_t)1;
+}
+
+void BangBang_decr_uint(void)
+{
+  uint32_t x = 1U;
+  uint32_t __anf0 = x;
+  x = __anf0 - 1U;
+}
+

test/pulse/BangBang.fst

@@ -0,0 +1,19 @@
+module BangBang
+open Pulse
+#lang-pulse
+
+fn modify_nested_ptr (x: ref (ref Int32.t)) (#y: erased (ref Int32.t)) (#z: erased Int32.t { Int32.v z < Int.max_int Int32.n - 3 })
+  preserves x |-> y
+  requires reveal y |-> z
+  returns z': Int32.t
+  ensures reveal y |-> Int32.add z 2l
+  ensures rewrites_to z' (Int32.add z 3l)
+{
+  (!x) := (!(!x)) `Int32.add` 2l;
+  ((!(!x)) `Int32.add` 1l)
+}
+
+fn decr_uint () {
+  let mut x: UInt32.t = 1ul;
+  x := !x `UInt32.sub` 1ul;
+}

test/pulse/Break.expected.c

@@ -0,0 +1,115 @@
+/* krml header omitted for test repeatability */
+
+
+#include "Break.h"
+
+void Break_simple_break(void)
+{
+  bool k = true;
+  bool _break = false;
+  bool cond;
+  if (_break)
+    cond = false;
+  else
+    cond = k;
+  while (cond)
+  {
+    _break = true;
+    bool ite;
+    if (_break)
+      ite = false;
+    else
+      ite = k;
+    cond = ite;
+  }
+}
+
+void Break_break_continue_and_return(uint8_t which)
+{
+  bool _return = false;
+  uint32_t i = 0U;
+  bool _break = false;
+  bool cond;
+  if (_break)
+    cond = false;
+  else if (_return)
+    cond = false;
+  else
+  {
+    uint32_t __anf0 = i;
+    cond = __anf0 < 1000U;
+  }
+  while (cond)
+  {
+    bool _continue = false;
+    if ((uint32_t)which == 0U)
+      _break = true;
+    bool _break1 = _break;
+    if (!_break1)
+    {
+      if ((uint32_t)which == 1U)
+        _continue = true;
+      bool _continue1 = _continue;
+      if (!_continue1)
+      {
+        if ((uint32_t)which == 2U)
+          _return = true;
+        bool _return1 = _return;
+        if (!_return1)
+        {
+          uint32_t __anf0 = i;
+          i = __anf0 + 1U;
+        }
+      }
+    }
+    bool ite;
+    if (_break)
+      ite = false;
+    else if (_return)
+      ite = false;
+    else
+    {
+      uint32_t __anf0 = i;
+      ite = __anf0 < 1000U;
+    }
+    cond = ite;
+  }
+}
+
+size_t Break_find_zero_with_break(int32_t *a, size_t sz)
+{
+  size_t i = (size_t)0U;
+  bool _break = false;
+  bool cond;
+  if (_break)
+    cond = false;
+  else
+  {
+    size_t __anf0 = i;
+    cond = __anf0 < sz;
+  }
+  while (cond)
+  {
+    size_t __anf01 = i;
+    int32_t __anf1 = a[__anf01];
+    if (__anf1 == (int32_t)0)
+      _break = true;
+    bool _break1 = _break;
+    if (!_break1)
+    {
+      size_t __anf02 = i;
+      i = __anf02 + (size_t)1U;
+    }
+    bool ite;
+    if (_break)
+      ite = false;
+    else
+    {
+      size_t __anf0 = i;
+      ite = __anf0 < sz;
+    }
+    cond = ite;
+  }
+  return i;
+}
+

test/pulse/Break.fst

@@ -0,0 +1,59 @@
+module Break
+open Pulse
+open Pulse.Lib.WithPure
+#lang-pulse
+
+fn simple_break ()
+{
+  let mut k = true;
+  while (!k)
+    invariant live k
+    ensures true
+  {
+    break;
+  }
+}
+
+fn break_continue_and_return (which: UInt8.t)
+{
+  let mut i = 0ul;
+  while (!i `UInt32.lt` 1000ul)
+    invariant live i
+    ensures true
+  {
+    if (which = 0uy) {
+      break;
+    };
+    if (which = 1uy) {
+      continue;
+    };
+    if (which = 2uy) {
+      return;
+    };
+    i := !i `UInt32.add` 1ul;
+  }
+}
+
+fn find_zero_with_break (a: array Int32.t) (sz: SizeT.t)
+  preserves pts_to a #'r 'va
+  requires with_pure (SizeT.v sz <= Seq.length 'va)
+  returns i: SizeT.t
+  ensures pure (SizeT.v i <= SizeT.v sz /\
+    (forall (j: nat). j < SizeT.v i ==> Seq.index 'va j <> 0l))
+  ensures pure (SizeT.v i < SizeT.v sz ==> Seq.index 'va (SizeT.v i) == 0l)
+{
+  let mut i: SizeT.t = 0sz;
+  while (!i `SizeT.lt` sz)
+    invariant live i
+    invariant pure (SizeT.v !i <= SizeT.v sz /\
+      (forall (j: nat). j < SizeT.v (!i) ==> Seq.index 'va j <> 0l))
+    ensures (SizeT.v !i < SizeT.v sz /\ a.(!i) = 0l)
+  {
+    if (a.(!i) = 0l) {
+      break;
+    };
+
+    i := !i `SizeT.add` 1sz;
+  };
+  !i
+}

test/pulse/Bug356.expected.c

@@ -0,0 +1,32 @@
+/* krml header omitted for test repeatability */
+
+
+#include "Bug356.h"
+
+uint32_t Bug356_test(bool b)
+{
+  if (b)
+    return 1U;
+  else
+  {
+    KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "");
+    KRML_HOST_EXIT(255U);
+  }
+}
+
+uint32_t Bug356_test_final_admit(bool b)
+{
+  if (b)
+    return 1U;
+  else
+  {
+    KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "");
+    KRML_HOST_EXIT(255U);
+  }
+}
+
+void Bug356_test_unit_admit(bool x)
+{
+  KRML_MAYBE_UNUSED_VAR(x);
+}
+