From 6d00321e84feba40ff26f74e019f936ab077ac2f Mon Sep 17 00:00:00 2001
From: Filipe Marques <filipe.s.marques@tecnico.ulisboa.pt>
Date: Thu, 18 Apr 2024 16:52:13 +0100
Subject: [PATCH] Fixes redundant os constraints and add more CI

---
 .github/workflows/build.yml        |  2 ++
 .github/workflows/lower-bounds.yml | 46 ++++++++++++++++++++++++++++++
 encoding.opam.template             |  5 ----
 lib/eval.ml                        | 28 ++++++++++++------
 smtml.opam                         |  5 ++++
 smtml.opam.template                |  5 ++++
 6 files changed, 78 insertions(+), 13 deletions(-)
 create mode 100644 .github/workflows/lower-bounds.yml
 delete mode 100644 encoding.opam.template
 create mode 100644 smtml.opam.template

diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index 46a7784c..19ad0c41 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -20,6 +20,8 @@ jobs:
           - "4.14"
           - "5.1"
     runs-on: ${{ matrix.os }}
+    env:
+      OPAMCONFIRMLEVEL: unsafe-yes # allow opam depext to yes package manager prompts
     steps:
       - name: Checkout
         uses: actions/checkout@v4
diff --git a/.github/workflows/lower-bounds.yml b/.github/workflows/lower-bounds.yml
new file mode 100644
index 00000000..81b223ac
--- /dev/null
+++ b/.github/workflows/lower-bounds.yml
@@ -0,0 +1,46 @@
+# Credit for this workflow:
+# https://sim642.eu/blog/2022/03/13/ocaml-dependencies-lower-bounds-ci/
+name: Lower bounds
+
+on:
+  push:
+    branches:
+      - main
+  pull_request:
+    branches:
+      - main
+
+jobs:
+  lower-bounds:
+    fail-fast: false
+    strategy:
+      matrix:
+        os:
+          - ubuntu-latest
+          - macos-latest
+        ocaml-compiler:
+          - "4.14"
+          - "5.1"
+    runs-on: ${{ matrix.os }}
+    env:
+      OPAMCONFIRMLEVEL: unsafe-yes # allow opam depext to yes package manager prompts
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v4
+      - name: Set up OCaml ${{ matrix.ocaml-compiler }}
+        uses: ocaml/setup-ocaml@v2
+        with:
+          ocaml-compiler: ${{ matrix.ocaml-compiler }}
+          dune-cache: true
+          allow-prerelease-opam: true
+      - name: Install dependencies
+        run: opam install . --deps-only --with-test
+      - name: Install opam-0install
+        run: opam install opam-0install
+      - name: Downgrade dependencies
+        run: opam install --unlock-base $(opam exec -- opam-0install --prefer-oldest --with-test smtml)
+      - name: Build
+        run: opam exec -- dune build @install
+      - name: Test
+        run: opam exec -- dune runtest
+
diff --git a/encoding.opam.template b/encoding.opam.template
deleted file mode 100644
index 2dd79882..00000000
--- a/encoding.opam.template
+++ /dev/null
@@ -1,5 +0,0 @@
-available: (arch = "x86_64" | arch = "arm64") & os != "win32" & arch != "x86_32"
-pin-depends: [
-  [ "colibri2.0.4.0" "git+https://git.frama-c.com/pub/colibrics.git#ae18d699b19e7967a81ccae6db454edfa968feae"]
-  [ "colibrilib.0.4.0" "git+https://git.frama-c.com/pub/colibrics.git#ae18d699b19e7967a81ccae6db454edfa968feae"]
-]
diff --git a/lib/eval.ml b/lib/eval.ml
index 9350975e..f9c00afb 100644
--- a/lib/eval.ml
+++ b/lib/eval.ml
@@ -286,15 +286,21 @@ module I32 = struct
     Int32.logor (shr_u x (Int32.of_int n)) (shl x (Int32.of_int (32 - n)))
   [@@inline]
 
+  let clz n =
+    let n = Ocaml_intrinsics.Int32.count_leading_zeros n in
+    Int32.of_int n
+
+  let ctz n =
+    let n = Ocaml_intrinsics.Int32.count_trailing_zeros n in
+    Int32.of_int n
+
   let unop (op : unop) (v : Value.t) : Value.t =
     let f =
       match op with
       | Neg -> Int32.neg
       | Not -> Int32.lognot
-      | Clz ->
-        fun n -> Int32.of_int (Ocaml_intrinsics.Int32.count_leading_zeros n)
-      | Ctz ->
-        fun n -> Int32.of_int (Ocaml_intrinsics.Int32.count_trailing_zeros n)
+      | Clz -> clz
+      | Ctz -> ctz
       | _ -> Log.err {|unop: Unsupported i32 operator "%a"|} Ty.pp_unop op
     in
     to_value (f (of_value 1 v))
@@ -379,15 +385,21 @@ module I64 = struct
     Int64.logor (shr_u x (Int64.of_int n)) (shl x (Int64.of_int (64 - n)))
   [@@inline]
 
+  let clz n =
+    let n = Ocaml_intrinsics.Int64.count_leading_zeros n in
+    Int64.of_int n
+
+  let ctz n =
+    let n = Ocaml_intrinsics.Int64.count_trailing_zeros n in
+    Int64.of_int n
+
   let unop (op : unop) (v : Value.t) : Value.t =
     let f =
       match op with
       | Neg -> Int64.neg
       | Not -> Int64.lognot
-      | Clz ->
-        fun n -> Int64.of_int (Ocaml_intrinsics.Int64.count_leading_zeros n)
-      | Ctz ->
-        fun n -> Int64.of_int (Ocaml_intrinsics.Int64.count_trailing_zeros n)
+      | Clz -> clz
+      | Ctz -> ctz
       | _ -> Log.err {|unop: Unsupported i64 operator "%a"|} Ty.pp_unop op
     in
     to_value (f (of_value 1 v))
diff --git a/smtml.opam b/smtml.opam
index 5aea77d1..5d1ce305 100644
--- a/smtml.opam
+++ b/smtml.opam
@@ -39,3 +39,8 @@ build: [
   ]
 ]
 dev-repo: "git+https://github.com/formalsec/smtml.git"
+available: arch != "arm32" & arch != "x86_32"
+pin-depends: [
+  ["colibri2.0.4.0" "git+https://git.frama-c.com/pub/colibrics.git#ae18d699b19e7967a81ccae6db454edfa968feae"]
+  ["colibrilib.0.4.0" "git+https://git.frama-c.com/pub/colibrics.git#ae18d699b19e7967a81ccae6db454edfa968feae"]
+]
diff --git a/smtml.opam.template b/smtml.opam.template
new file mode 100644
index 00000000..f215a25c
--- /dev/null
+++ b/smtml.opam.template
@@ -0,0 +1,5 @@
+available: arch != "arm32" & arch != "x86_32"
+pin-depends: [
+  ["colibri2.0.4.0" "git+https://git.frama-c.com/pub/colibrics.git#ae18d699b19e7967a81ccae6db454edfa968feae"]
+  ["colibrilib.0.4.0" "git+https://git.frama-c.com/pub/colibrics.git#ae18d699b19e7967a81ccae6db454edfa968feae"]
+]