FStarLang / pulse

The Pulse separation logic DSL for F*
Apache License 2.0
6 stars 7 forks source link

Extraction: mark everything CInline #188

Closed mtzguido closed 2 months ago

mtzguido commented 2 months ago

This makes generated C code much more compact by reusing the karamel inlining logic.

Example diff from ExtractionTest.c:

diff --git a/old.c b/new.c
index d70776d3b..6d18a1df4 100644
--- a/old.c
+++ b/new.c
@@ -20,8 +20,7 @@ uint32_t ExtractionTest_zero(void)

 void ExtractionTest_test_read_write(uint32_t *x)
 {
-  uint32_t n = *x;
-  *x = n + 0U;
+  *x = *x + 0U;
 }

 void ExtractionTest_test_write_10(uint32_t *x)
@@ -39,32 +38,23 @@ void ExtractionTest_test_inner_ghost_fun(void)
 void ExtractionTest_write10(uint32_t *x)
 {
   uint32_t ctr = 10U;
-  uint32_t ctr_1 = ctr;
-  bool cond = ctr_1 > 0U;
-  while (cond)
+  while (ctr > 0U)
   {
     *x = 2U;
     ExtractionTest_test_read_write(x);
     *x = 0U;
-    uint32_t ctr_2 = ctr;
-    ctr = ctr_2 - 1U;
-    uint32_t ctr_1 = ctr;
-    cond = ctr_1 > 0U;
+    ctr = ctr - 1U;
   }
 }

 void ExtractionTest_fill_array(uint32_t *x, size_t n, uint32_t v)
 {
   size_t i = (size_t)0U;
-  size_t i_1 = i;
-  bool cond = i_1 < n;
-  while (cond)
+  while (i < n)
   {
     size_t i_2 = i;
     x[i_2] = v;
     i = i_2 + (size_t)1U;
-    size_t i_1 = i;
-    cond = i_1 < n;
   }
 }

@@ -120,19 +110,15 @@ krml_checked_int_t ExtractionTest_fib(krml_checked_int_t x)
   else
   {
     krml_checked_int_t x1 = ExtractionTest_fib(Prims_op_Subtraction(x, (krml_checked_int_t)1));
-    krml_checked_int_t x2 = ExtractionTest_fib(Prims_op_Subtraction(x, (krml_checked_int_t)2));
-    krml_checked_int_t _bind_c = Prims_op_Addition(x1, x2);
-    krml_checked_int_t _bind_c0 = _bind_c;
-    krml_checked_int_t _bind_c1 = _bind_c0;
-    krml_checked_int_t _if_br = _bind_c1;
-    return _if_br;
+    return
+      Prims_op_Addition(x1,
+        ExtractionTest_fib(Prims_op_Subtraction(x, (krml_checked_int_t)2)));
   }
 }

 krml_checked_int_t ExtractionTest_fib2(krml_checked_int_t x)
 {
   krml_checked_int_t n = ExtractionTest_fib(x);
-  krml_checked_int_t m = ExtractionTest_fib(Prims_op_Addition(x, (krml_checked_int_t)1));
-  return Prims_op_Addition(m, n);
+  return Prims_op_Addition(ExtractionTest_fib(Prims_op_Addition(x, (krml_checked_int_t)1)), n);
 }