Add state transformers! (#324)

* Add state transformers !

* Update `dune`, export Gillian-JS

* Fix dune-project

* Remove Formula

* Remove `gillian-js-libs`, expose w `gillian-js`

* Fix dune

* Oops

* Test

* Test

* Update Makefile

Gillian-C/lib/dune

@@ -6,8 +6,8 @@
  (modules annot_lexer))
 
 (library
- (package gillian-c)
  (name cgil_lib)
+ (public_name gillian-c.cgil_lib)
  (libraries
   gillian
   gillian.alcotest-runner

Gillian-JS/JS_Parser/src/dune

@@ -1,3 +1,4 @@
 (library
  (name JS_Parser)
+ (public_name gillian-js.JS_Parser)
  (libraries str flow_parser fpath))

Gillian-JS/lib/Compiler/dune

@@ -1,5 +1,6 @@
 (library
  (name js2jsil_lib)
+ (public_name gillian-js.js2jsil_lib)
  (flags :standard -open Gillian.Utils)
  (libraries jsil_syntax jslogic parsing javert_utils str dune-site))
 

Gillian-JS/lib/JSIL/dune

@@ -1,5 +1,6 @@
 (library
  (name jsil_syntax)
+ (public_name gillian-js.jsil_syntax)
  (libraries gillian)
  (preprocess
   (pps ppx_deriving.std ppx_deriving_yojson))

Gillian-JS/lib/JSLogic/dune

@@ -1,4 +1,5 @@
 (library
  (name jslogic)
+ (public_name gillian-js.jslogic)
  (libraries gillian jsil_syntax JS_Parser javert_utils)
  (flags :standard -open Utils -open Gillian.Utils))

Gillian-JS/lib/Parsing/dune

@@ -7,4 +7,5 @@
 
 (library
  (name parsing)
+ (public_name gillian-js.parsing)
  (libraries gillian jsil_syntax jslogic javert_utils str))

Gillian-JS/lib/Semantics/dune

@@ -1,5 +1,6 @@
 (library
  (name semantics)
+ (public_name gillian-js.semantics)
  (libraries gillian jsil_syntax javert_utils js2jsil_lib str)
  (preprocess
   (pps ppx_deriving.std ppx_deriving_yojson))

Gillian-JS/lib/utils/dune

@@ -1,5 +1,6 @@
 (library
  (name javert_utils)
+ (public_name gillian-js.javert_utils)
  (libraries gillian dune-site))
 
 (generate_sites_module

GillianCore/lib/dune

@@ -9,6 +9,7 @@
   command_line
   bulk
   ;gillian_bulk_rely
+  parserAndCompiler
   logging
   incrementalAnalysis
   monadic

GillianCore/lib/gillian.ml

@@ -5,7 +5,7 @@ module Gil_syntax = struct
 end
 
 (** The GIL parser
-    
+
   This is parametric over target languages, via the [Annot] module parameter. *)
 module Gil_parsing = struct
   (** @inline *)
@@ -38,6 +38,7 @@ end
 
 module Bulk = Bulk
 module Monadic = Monadic
+module ParserAndCompiler = ParserAndCompiler
 
 (** Modules for the debugger and related TL-lifting *)
 module Debugger = struct

Makefile

@@ -9,7 +9,7 @@ fmt:
 	opam exec -- dune fmt
 
 deps:
-	opam exec -- dune build gillian.opam wisl.opam gillian-js.opam gillian-c.opam gillian-c2.opam
+	opam exec -- dune build gillian.opam wisl.opam gillian-js.opam gillian-c.opam gillian-c2.opam transformers.opam
 	opam install . -y --deps-only
 
 init-dev:
@@ -21,7 +21,7 @@ init-ci:
 	opam install $(shell echo ${BUILD_PACKAGES} | tr ',' ' ') -y
 
 uninstall:
-	opam remove gillian gillian-c gillian-js wisl gillian-c2 -y
+	opam remove gillian gillian-c gillian-js wisl gillian-c2 transformers -y
 
 watch:
 	opam exec -- dune build --watch
@@ -59,4 +59,4 @@ sphinx:
 sphinx-watch:
 	sphinx-autobuild sphinx _docs/sphinx/
 
-.PHONY: init-dev watch docs build c-init-env wisl-init-env js-init-env docs odoc sphinx
+.PHONY: init-dev watch docs build c-init-env wisl-init-env js-init-env docs odoc sphinx

dune

@@ -4,6 +4,7 @@
  Gillian-JS
  Gillian-C
  Gillian-C2
+ transformers
  Gillian-Alcotest-Runner
  ppx_sat)
 

dune-project

@@ -103,3 +103,18 @@
    (= :version)))
  (synopsis
   "Gillian instantiation for Wisl, a small toy language for teaching and experimentation"))
+
+(package
+ (name transformers)
+ (sites
+  (share runtime))
+ (synopsis "Gillian instantiation using state model transformers, à la Iris")
+ (depends
+  (gillian
+   (= :version))
+  (gillian-c
+   (= :version))
+  (gillian-js
+   (= :version))
+  dune-site
+  printbox-text))

transformers.opam

@@ -0,0 +1,34 @@
+# This file is generated by dune, edit dune-project instead
+opam-version: "2.0"
+synopsis: "Gillian instantiation using state model transformers, à la Iris"
+maintainer: ["The Gillian Team"]
+authors: ["The Gillian Team"]
+license: "BSD-3-Clause"
+homepage: "https://github.com/GillianPlatform/Gillian"
+bug-reports: "https://github.com/GillianPlatform/Gillian/issues"
+depends: [
+  "dune" {>= "3.16"}
+  "gillian" {= version}
+  "gillian-c" {= version}
+  "gillian-js" {= version}
+  "dune-site"
+  "printbox-text"
+  "odoc" {with-doc}
+]
+build: [
+  ["dune" "subst"] {dev}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "--promote-install-files=false"
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+  ["dune" "install" "-p" name "--create-install-files" name]
+]
+dev-repo: "git+https://github.com/GillianPlatform/Gillian.git"

transformers/bin/dune

@@ -0,0 +1,4 @@
+(executable
+ (public_name transformers)
+ (package transformers)
+ (libraries prebuilt states gillian))

transformers/bin/example.gil

@@ -0,0 +1,175 @@
+(* A simple list algorithm, for a linear heap.
+   To verify this code, use the following transformer stack:
+   OpenPMap (IntegerIndex) (Freeable (Exclusive)) *)
+
+pred sll(+x, vs: List) :
+    (* empty list *)
+    (x == null) * (vs == {{  }}),
+    (* non-empty list *)
+    (x == #h) * (vs == l+ ({{ #v }}, #vs)) *
+    <ex>(#h; #v) * <ex>(#h i+ 1i; #next) *
+    sll(#next, #vs);
+
+spec alloc_node(v)
+    [[ v == #v ]]
+    [[ sll(ret, {{ #v }}) ]]
+    normal
+proc alloc_node(v) {
+    c1 := [alloc]();
+    c1 := l-nth(c1, 0i);
+    c2 := [alloc]();
+    c2 := l-nth(c2, 0i);
+    x := [store](c1, v);
+    x := [store](c2, null);
+    ret := c1;
+    return
+};
+
+spec append(h, v)
+    [[ (h == #h) * (v == #v) * sll(#h, #vs) ]]
+    [[ (ret == #h2) * sll(#h2, l+ (#vs, {{ #v }})) ]]
+    normal
+proc append(h, v) {
+    goto [h = null] then0 else0;
+
+then0:
+    ret := "alloc_node"(v);
+    goto end;
+
+else0:
+    next := [load](h i+ 1i);
+    next := l-nth(next, 1i);
+    h_new := "append"(next, v);
+    x := [store](h i+ 1i, h_new);
+    ret := h;
+
+end:
+    return
+};
+
+spec prepend(h, v)
+    [[ (h == #h) * (v == #v) * sll(#h, #vs) ]]
+    [[ (ret == #h2) * sll(#h2, l+ ({{ #v }}, #vs)) ]]
+    normal
+proc prepend(h, v) {
+    ret := "alloc_node"(v);
+    x := [store](ret i+ 1i, h);
+    return
+};
+
+spec length(h)
+    [[ (h == #h) * sll(#h, #vs) ]]
+    [[ (ret == (l-len #vs)) * sll(#h, #vs) ]]
+    normal
+proc length(h) {
+    goto [h = null] then0 else0;
+
+then0:
+    ret := 0i;
+    goto end;
+
+else0:
+    next := [load](h i+ 1i);
+    next := l-nth(next, 1i);
+    ret := "length"(next);
+    ret := ret i+ 1i;
+    goto end;
+
+end:
+    return
+};
+
+spec concat(h1, h2)
+    [[ (h1 == #h1) * (h2 == #h2) * sll(#h1, #vs1) * sll(#h2, #vs2) ]]
+    [[ (ret == #h3) * sll(#h3, l+ (#vs1, #vs2)) ]]
+    normal
+proc concat(h1, h2) {
+    goto [h1 = null] then0 else0;
+
+then0:
+    ret := h2;
+    goto end;
+
+else0:
+    next := [load](h1 i+ 1i);
+    next := l-nth(next, 1i);
+    h_new := "concat"(next, h2);
+    x := [store](h1 i+ 1i, h_new);
+    ret := h1;
+
+end:
+    return
+};
+
+pred sll_member(+vs : List, +v, r : Bool) :
+    (vs == {{  }}) * (r == false), (* empty list *)
+    (vs == l+ ({{  v  }}, #vs2)) *   (r == true) * sll_member(#vs2, v, #etc), (* found a match *)
+    (vs == l+ ({{ #v2 }}, #vs2)) * (!(v == #v2)) * sll_member(#vs2, v, r); (* no match yet *)
+
+spec member(h, v)
+    [[ (h == #h) * (v == #v) * sll(#h, #vs) * sll_member(#vs, #v, #r) ]]
+    [[ (ret == #r) * sll(#h, #vs) * sll_member(#vs, #v, #r) ]]
+    normal
+proc member(h, v) {
+    goto [h = null] then0 else0;
+
+then0:
+    ret := false;
+    goto end;
+
+else0:
+    h_val := [load](h);
+    h_val := l-nth(h_val, 1i);
+    goto [h_val = v] then1 else1;
+
+then1:
+    ret := true;
+    goto end;
+
+else1:
+    next := [load](h i+ 1i);
+    next := l-nth(next, 1i);
+    ret := "member"(next, v);
+    goto end;
+
+end:
+    return
+};
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+spec free_list(h)
+     [[ (h == #h) * sll(#h, #vs) ]]
+    [[ (ret == null) ]]
+    normal
+proc free_list(h) {
+    goto [h = null] then0 else0;
+
+then0:
+    ret := null;
+    goto end;
+
+else0:
+    next := [load](h i+ 1i);
+    next := l-nth(next, 1i);
+    x := "free_list"(next);
+    x := [free](h);
+    x := [free](h i+ 1i);
+    ret := null;
+
+end:
+    return
+};

transformers/bin/transformers.ml

@@ -0,0 +1,43 @@
+open Gillian
+open States
+(* Uncomment to import transformer shorthands
+   open Prebuilt.Utils *)
+
+(* Select prebuilt mode (or build one!) -- available state models are C, JS and WISL. *)
+module Prebuilt = Prebuilt.Lib.C_Base
+
+(* State model
+   For a linear heap, for example:
+   module MyMem = OpenPMap (IntegerIndex) (Freeable (Exclusive)) *)
+module MyMem = Prebuilt.MonadicSMemory
+
+(* Get modules *)
+module PC = Prebuilt.ParserAndCompiler
+module ExternalSemantics = Prebuilt.ExternalSemantics
+module InitData = Prebuilt.InitData
+
+(* For debugging actions / predicates, uncomment: *)
+(* module Debug = Debug.Make (MyMem)
+   let () = Debug.print_info () *)
+
+(* Convert custom state model -> Gillian state model *)
+module PatchedMem = MyMonadicSMemory.Make (MyMem) (Prebuilt.MyInitData)
+
+(* Gillian Instantiation *)
+(* For measuring performance, wrap this in PerfMeasurer.Make *)
+module SMemory = Gillian.Monadic.MonadicSMemory.Lift (PatchedMem)
+
+module Lifter
+    (Verifier : Gillian.Abstraction.Verifier.S
+                  with type annot = Gil_syntax.Annot.Basic.t) =
+  Gillian.Debugger.Lifter.Gil_lifter.Make (SMemory) (PC) (Verifier)
+
+module CLI =
+  Gillian.Command_line.Make (InitData) (Cmemory.Make (InitData)) (SMemory) (PC)
+    (ExternalSemantics)
+    (struct
+      let runners = []
+    end)
+    (Lifter)
+
+let () = CLI.main ()

transformers/lib/dune

@@ -0,0 +1,2 @@
+(library
+ (name transformers_lib))