Use SMTLIB instead of Z3 bindings; remove Z3 lib dependency (#303)

* Tweak makefile

* Add makefile check to pre-commit hooks

* Install simple-smt lib

* Add SMTLIB implementation

* New SMT; fixes & enhancements

* Use new SMT interface

* Remove z3_encoding & Z3 dependency

* Install Z3 in CI

* Fix makefile blunder

* Add sexplib to deps

* Tweak makefile once more

* Tweak some test makefiles

* SMT: fix empty seq encoding

* SMT: Fix lvars_as_list_elements

* Tweak testJaVerT.sh

* Fix variable sanitisation for quantified formulae

* Update docs for SMT change

.github/workflows/ci.yml

@@ -20,6 +20,11 @@ jobs:
         operating-system: [macos-latest, ubuntu-latest]
     runs-on: ${{ matrix.operating-system }}
     steps:
+      - name: Setup Z3
+        id: z3
+        uses: cda-tum/setup-z3@v1
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
       - uses: actions/checkout@v4
       - uses: actions/setup-python@v4
         with:
@@ -81,6 +86,11 @@ jobs:
     runs-on: ${{ matrix.operating-system }}
     needs: build
     steps:
+      - name: Setup Z3
+        id: z3
+        uses: cda-tum/setup-z3@v1
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
       - uses: ocaml/setup-ocaml@v2
         with:
           ocaml-compiler: "ocaml-variants.5.2.0+options"
@@ -114,6 +124,11 @@ jobs:
     runs-on: ${{ matrix.operating-system }}
     needs: build
     steps:
+      - name: Setup Z3
+        id: z3
+        uses: cda-tum/setup-z3@v1
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
       - uses: ocaml/setup-ocaml@v2
         with:
           ocaml-compiler: "ocaml-variants.5.2.0+options"
@@ -134,7 +149,7 @@ jobs:
         run: "Gillian-JS/scripts/setup_environment.sh"
         working-directory: "Gillian"
       - name: Test JaVerT
-        run: "opam exec -- bash ./testJaVerT.sh"
+        run: "./testJaVerT.sh"
         working-directory: "Gillian/Gillian-JS/environment/"
       # - name: Test Amazon
       #   run: "make"
@@ -147,6 +162,11 @@ jobs:
     runs-on: ${{ matrix.operating-system }}
     needs: build
     steps:
+      - name: Setup Z3
+        id: z3
+        uses: cda-tum/setup-z3@v1
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
       - uses: ocaml/setup-ocaml@v2
         with:
           ocaml-compiler: "ocaml-variants.5.2.0+options"
@@ -180,6 +200,11 @@ jobs:
     runs-on: ${{ matrix.operating-system }}
     needs: build
     steps:
+      - name: Setup Z3
+        id: z3
+        uses: cda-tum/setup-z3@v1
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
       - uses: ocaml/setup-ocaml@v2
         with:
           ocaml-compiler: "ocaml-variants.5.2.0+options"
@@ -209,6 +234,11 @@ jobs:
     runs-on: ${{ matrix.operating-system }}
     needs: build
     steps:
+      - name: Setup Z3
+        id: z3
+        uses: cda-tum/setup-z3@v1
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
       - uses: ocaml/setup-ocaml@v2
         with:
           ocaml-compiler: "ocaml-variants.5.2.0+options"
@@ -239,6 +269,11 @@ jobs:
   #   runs-on: ${{ matrix.operating-system }}
   #   needs: build
   #   steps:
+  #     - name: Setup Z3
+  #       id: z3
+  #       uses: cda-tum/setup-z3@v1
+  #       env:
+  #         GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
   #     - uses: ocaml/setup-ocaml@v2
   #       with:
   #         ocaml-compiler: "ocaml-variants.5.2.0+options"

Dockerfile

@@ -6,7 +6,7 @@ ARG DEBIAN_FRONTEND=noninteractive
 
 RUN sudo apt-get update
 
-RUN sudo apt-get install libgmp-dev pkg-config libsqlite3-dev python3 -y
+RUN sudo apt-get install libgmp-dev pkg-config libsqlite3-dev python3 z3 -y
 
 RUN mkdir /home/opam/app
 

Gillian-C/examples/amazon/Makefile

@@ -1,4 +1,8 @@
-VERIFY=opam exec -- gillian-c verify
+ifdef GITHUB_ACTIONS
+	VERIFY=opam exec -- gillian-c verify
+else
+	VERIFY=dune exec -- gillian-c verify
+endif
 
 default:
 	${VERIFY} \
@@ -42,4 +46,11 @@ byte-cursor-ub:
 bugs: string-bug header-bug byte-cursor-ub
 
 clean:
-	rm -rf *.i *.deps
+	rm -rf *.i *.deps
+
+t:
+	${VERIFY} \
+		header.c edk.c array_list.c ec.c byte_buf.c \
+		hash_table.c string.c allocator.c \
+		error.c base.c \
+		--fstruct-passing --no-lemma-proof --proc aws_cryptosdk_hdr_parse -l disabled --dump-smt

Gillian-C/examples/amazon_bi/Makefile

@@ -1,5 +1,5 @@
 ifdef GITHUB_ACTIONS
-	ACT=gillian-c act
+	ACT=opam exec -- gillian-c act
 else
 	ACT=dune exec -- gillian-c act
 endif

Gillian-JS/scripts/testJaVerT.sh

@@ -2,24 +2,18 @@
 
 set -e
 
-if [[ -z "${GITHUB_ACTIONS}" ]]; then
-	echo "Building test environment..."
-	esy x true > /dev/null 2>&1
-	esy exec-env > exec.env
-	source exec.env
+if [[ "${GITHUB_ACTIONS}" ]]; then
+	VERIFY="opam exec -- gillian-js verify"
+else
+  VERIFY="dune exec -- gillian-js verify"
 fi
+
 # Bash array format: ("one" "two" "three")
 # JS Files to test
 declare -a jsfiles=("BST" "PriQ" "SLL" "DLL" "Sort")
 
 FINAL_RETURN=0
 
-if [[ $1 == "fast" ]]; then
-	params="-nochecks -nooutput"
-else
-	params=""
-fi
-
 foldername=${PWD##*/}
 if [ "$foldername" != "environment" ]
 then
@@ -33,10 +27,10 @@ do
   sleep 1
 	echo "Verifying: $f.js"
 	if [[ $1 == "count" ]]; then
-		gillian-js verify Examples/JaVerT/$f.js -l disabled --stats --no-lemma-proof
+		$VERIFY Examples/JaVerT/$f.js -l disabled --stats --no-lemma-proof
 		rc=$?
 	else
-		gillian-js verify Examples/JaVerT/$f.js -l disabled --no-lemma-proof
+		$VERIFY Examples/JaVerT/$f.js -l disabled --no-lemma-proof
 		rc=$?
 	fi
 	if [[ $rc != 0 ]]; then FINAL_RETURN=1; fi

GillianCore/command_line/common_args.ml

@@ -134,7 +134,7 @@ module Make (PC : ParserAndCompiler.S) = struct
     Arg.(value & flag & info [ "pbn"; "print-by-need" ] ~doc)
 
   let dump_smt =
-    let doc = "Dump every smt query sent to z3" in
+    let doc = "Dump every smt query sent to the solver" in
     Arg.(value & flag & info [ "dump-smt" ] ~doc)
 
   let use (term : (unit -> unit) Term.t) : unit Term.t =

GillianCore/engine/FOLogic/FOSolver.ml

@@ -39,7 +39,7 @@ let simplify_pfs_and_gamma
 let check_satisfiability_with_model (fs : Formula.t list) (gamma : Type_env.t) :
     SESubst.t option =
   let fs, gamma, subst = simplify_pfs_and_gamma fs gamma in
-  let model = Z3_encoding.check_sat_core fs (Type_env.as_hashtbl gamma) in
+  let model = Smt.check_sat fs (Type_env.as_hashtbl gamma) in
   let lvars =
     List.fold_left
       (fun ac vs ->
@@ -50,22 +50,20 @@ let check_satisfiability_with_model (fs : Formula.t list) (gamma : Type_env.t) :
       Expr.Set.empty
       (List.map Formula.lvars (Formula.Set.elements fs))
   in
-  let z3_vars = Expr.Set.diff lvars (SESubst.domain subst None) in
+  let smt_vars = Expr.Set.diff lvars (SESubst.domain subst None) in
   L.(
     verbose (fun m ->
         m "OBTAINED VARS: %s\n"
           (String.concat ", "
              (List.map
                 (fun e -> Format.asprintf "%a" Expr.pp e)
-                (Expr.Set.elements z3_vars)))));
+                (Expr.Set.elements smt_vars)))));
   let update x e = SESubst.put subst (LVar x) e in
   match model with
   | None -> None
   | Some model -> (
       try
-        Z3_encoding.lift_z3_model model
-          (Type_env.as_hashtbl gamma)
-          update z3_vars;
+        Smt.lift_model model (Type_env.as_hashtbl gamma) update smt_vars;
         Some subst
       with _ -> None)
 
@@ -83,7 +81,7 @@ let check_satisfiability
   if Formula.Set.is_empty fs then true
   else if Formula.Set.mem False fs then false
   else
-    let result = Z3_encoding.check_sat fs (Type_env.as_hashtbl gamma) in
+    let result = Smt.is_sat fs (Type_env.as_hashtbl gamma) in
     (* if time <> "" then
        Utils.Statistics.update_statistics ("FOS: CheckSat: " ^ time)
          (Sys.time () -. t); *)
@@ -198,20 +196,21 @@ let check_entailment
       let formulae = PFS.of_list (right_f :: (left_fs @ [] (* axioms *))) in
       let _ = Simplifications.simplify_pfs_and_gamma formulae gamma_left in
 
-      let ret, model =
-        Z3_encoding.check_sat_with_model
+      let model =
+        Smt.check_sat
           (Formula.Set.of_list (PFS.to_list formulae))
           (Type_env.as_hashtbl gamma_left)
       in
-      L.(verbose (fun m -> m "Entailment returned %b" (not ret)));
-      if ret then
-        L.tmi (fun m ->
-            m "Here's the model: %a"
-              (Fmt.Dump.option (Fmt.of_to_string Z3.Model.to_string))
-              model);
+      let ret = Option.is_none model in
+      L.(verbose (fun m -> m "Entailment returned %b" ret));
+      let () =
+        model
+        |> Option.iter (fun model ->
+               L.tmi (fun m -> m "Here's the model:\n%a" Smt.pp_sexp model))
+      in
       (* Utils.Statistics.update_statistics "FOS: CheckEntailment"
          (Sys.time () -. t); *)
-      not ret
+      ret
 
 let is_equal ~pfs ~gamma e1 e2 =
   (* let t = Sys.time () in *)

GillianCore/engine/dune

@@ -5,7 +5,7 @@
  (public_name gillian.engine)
  (libraries
   utils
-  z3_encoding
+  smt
   menhirLib
   fmt
   cmdliner

GillianCore/monadic/delayed.ml

@@ -55,7 +55,7 @@ let branch_on
             in
             then_branches @ else_branches
           else then_branches
-      with Z3_encoding.Z3Unknown ->
+      with Smt.SMT_unknown ->
         Fmt.pr "TIMED OUT ON: %a" Formula.pp guard;
         vanish () ~curr_pc)
 

GillianCore/monadic/dune

@@ -2,6 +2,6 @@
  (name monadic)
  (public_name gillian.monadic)
  (flags -open Utils.Prelude)
- (libraries gil_syntax engine utils fmt logging)
+ (libraries gil_syntax engine utils fmt logging smt)
  (preprocess
   (pps ppx_deriving.std ppx_deriving_yojson)))

GillianCore/smt/dune

@@ -0,0 +1,7 @@
+(library
+ (name smt)
+ (public_name gillian.smt)
+ (libraries gil_syntax utils simple_smt sexplib)
+ (preprocess
+  (pps ppx_deriving.std))
+ (flags :standard -open Utils.Prelude))