From 10685d985da4f3c99b988aa44daee43695a3f1dc Mon Sep 17 00:00:00 2001
From: Vesal Vojdani <vesal.vojdani@gmail.com>
Date: Mon, 7 Nov 2022 11:17:36 +0000
Subject: [PATCH 01/15] update readme (22.04)

---
 README.md | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/README.md b/README.md
index a782603..37d7ddc 100644
--- a/README.md
+++ b/README.md
@@ -6,15 +6,15 @@ See also [http://www.cs.umd.edu/projects/PL/locksmith/].
 
 ## Build Instructions
 
-The following should work on a fresh installation of Ubuntu 20.04.
+The following should work on a fresh installation of Ubuntu 22.04.
 Clone this repository and run the following in the checked out directory:
 
 ```console
-sudo apt install gcc opam autoconf automake make gperf python indent emacs flex bison
+sudo apt install gcc opam autoconf automake make gperf python3 indent emacs flex bison
 git submodule update --init --recursive
 opam init -n
 opam switch create . 3.11.2
-eval $(opam env)
+eval $(opam env --switch=. --set-switch)
 ./configure
 make
 ```

From abd362a107b0d176ea983cfe9df1b2068894dc39 Mon Sep 17 00:00:00 2001
From: Vesal Vojdani <vesal.vojdani@gmail.com>
Date: Mon, 7 Nov 2022 13:39:09 +0000
Subject: [PATCH 02/15] Add github action.

---
 .github/workflows/build.yml              | 38 ++++++++++++++++++++++++
 scripts/build.sh                         | 14 +++++++++
 svcomp_dist.sh => scripts/svcomp_dist.sh |  0
 scripts/test.sh                          |  5 ++++
 4 files changed, 57 insertions(+)
 create mode 100644 .github/workflows/build.yml
 create mode 100755 scripts/build.sh
 rename svcomp_dist.sh => scripts/svcomp_dist.sh (100%)
 create mode 100755 scripts/test.sh

diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
new file mode 100644
index 0000000..ee72146
--- /dev/null
+++ b/.github/workflows/build.yml
@@ -0,0 +1,38 @@
+name: Build workflow
+
+on:
+  - pull_request
+  - push
+
+jobs:
+  build:
+    strategy:
+      fail-fast: false
+      matrix:
+        os:
+          - ubuntu-22.04
+        ocaml-compiler:
+          - 3.11.2
+
+    runs-on: ${{ matrix.os }}
+
+    steps:
+      - name: Checkout code
+        uses: actions/checkout@v3
+        with: 
+          submodules: recursive
+
+      - name: Use OCaml ${{ matrix.ocaml-compiler }}
+        uses: ocaml/setup-ocaml@v2
+        with:
+          ocaml-compiler: ${{ matrix.ocaml-compiler }}
+
+      - name: Install Ubuntu packages
+        run: sudo apt install -y gcc opam autoconf automake make gperf python3 indent emacs flex bison
+
+      - name: Build Locksmith
+      - run: ./scripts/build.sh
+
+      - name: Test
+        run: ./scripts/test.sh
+        
diff --git a/scripts/build.sh b/scripts/build.sh
new file mode 100755
index 0000000..686a090
--- /dev/null
+++ b/scripts/build.sh
@@ -0,0 +1,14 @@
+#!/usr/bin/env bash
+
+./configure
+if ! make; then
+  echo "Rebuild banshee"
+  cd banshee
+  make
+  git checkout -- .
+  git clean -df
+  make
+  echo "Now retry Locksmith"
+  cd ..
+  make
+fi
diff --git a/svcomp_dist.sh b/scripts/svcomp_dist.sh
similarity index 100%
rename from svcomp_dist.sh
rename to scripts/svcomp_dist.sh
diff --git a/scripts/test.sh b/scripts/test.sh
new file mode 100755
index 0000000..196b383
--- /dev/null
+++ b/scripts/test.sh
@@ -0,0 +1,5 @@
+#!/usr/bin/env bash
+
+./locksmith --list-guardedby simple.c 2> out.txt
+cat out.txt
+grep -q "protected by" out.txt

From dcbf62089151989589561522091fc96157090689 Mon Sep 17 00:00:00 2001
From: Vesal Vojdani <vesal.vojdani@gmail.com>
Date: Mon, 7 Nov 2022 13:42:02 +0000
Subject: [PATCH 03/15] fix typo in github action

---
 .github/workflows/build.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index ee72146..2163845 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -31,7 +31,7 @@ jobs:
         run: sudo apt install -y gcc opam autoconf automake make gperf python3 indent emacs flex bison
 
       - name: Build Locksmith
-      - run: ./scripts/build.sh
+        run: ./scripts/build.sh
 
       - name: Test
         run: ./scripts/test.sh

From 032a7a66fb1cb05cd7231518d94cec7d314b21b6 Mon Sep 17 00:00:00 2001
From: Vesal Vojdani <vesal.vojdani@gmail.com>
Date: Mon, 7 Nov 2022 16:09:58 +0200
Subject: [PATCH 04/15] Update build.yml

set opam-depext: false
---
 .github/workflows/build.yml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index 2163845..25aab1c 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -26,6 +26,7 @@ jobs:
         uses: ocaml/setup-ocaml@v2
         with:
           ocaml-compiler: ${{ matrix.ocaml-compiler }}
+          opam-depext: false
 
       - name: Install Ubuntu packages
         run: sudo apt install -y gcc opam autoconf automake make gperf python3 indent emacs flex bison

From c4a3d6eb19abce5780015aea6cdd6f2ef66a8eef Mon Sep 17 00:00:00 2001
From: Vesal Vojdani <vesal.vojdani@gmail.com>
Date: Mon, 7 Nov 2022 14:30:40 +0000
Subject: [PATCH 05/15] Install libfl-dev in build.yml workflow.

---
 .github/workflows/build.yml | 2 +-
 README.md                   | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index 25aab1c..5cd021c 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -29,7 +29,7 @@ jobs:
           opam-depext: false
 
       - name: Install Ubuntu packages
-        run: sudo apt install -y gcc opam autoconf automake make gperf python3 indent emacs flex bison
+        run: sudo apt install -y gcc opam autoconf automake make gperf python3 indent emacs flex libfl-dev bison
 
       - name: Build Locksmith
         run: ./scripts/build.sh
diff --git a/README.md b/README.md
index 37d7ddc..9424674 100644
--- a/README.md
+++ b/README.md
@@ -10,7 +10,7 @@ The following should work on a fresh installation of Ubuntu 22.04.
 Clone this repository and run the following in the checked out directory:
 
 ```console
-sudo apt install gcc opam autoconf automake make gperf python3 indent emacs flex bison
+sudo apt install gcc opam autoconf automake make gperf python3 indent emacs flex libfl-dev bison
 git submodule update --init --recursive
 opam init -n
 opam switch create . 3.11.2

From ddb6d5f3162b95ac2b86fc76f3059433381dd3c8 Mon Sep 17 00:00:00 2001
From: Vesal Vojdani <vesal.vojdani@gmail.com>
Date: Mon, 7 Nov 2022 16:38:39 +0200
Subject: [PATCH 06/15] Remove "opam" from workflow.

I wanted this to be identical to the readme...
---
 .github/workflows/build.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index 5cd021c..b9af631 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -29,7 +29,7 @@ jobs:
           opam-depext: false
 
       - name: Install Ubuntu packages
-        run: sudo apt install -y gcc opam autoconf automake make gperf python3 indent emacs flex libfl-dev bison
+        run: sudo apt install -y gcc autoconf automake make gperf python3 indent emacs flex libfl-dev bison
 
       - name: Build Locksmith
         run: ./scripts/build.sh

From f61677e87973e0e9c8f328068dc5cee8eda8dea5 Mon Sep 17 00:00:00 2001
From: Vesal Vojdani <vesal.vojdani@gmail.com>
Date: Mon, 7 Nov 2022 14:51:19 +0000
Subject: [PATCH 07/15] Set the opam env in build script.

---
 scripts/build.sh | 1 +
 1 file changed, 1 insertion(+)

diff --git a/scripts/build.sh b/scripts/build.sh
index 686a090..77d50d7 100755
--- a/scripts/build.sh
+++ b/scripts/build.sh
@@ -1,5 +1,6 @@
 #!/usr/bin/env bash
 
+eval $(opam config env)
 ./configure
 if ! make; then
   echo "Rebuild banshee"

From c4f3403dd6adeffd6a923c754123cf14dd9d28f4 Mon Sep 17 00:00:00 2001
From: Vesal Vojdani <vesal.vojdani@gmail.com>
Date: Mon, 7 Nov 2022 17:03:37 +0200
Subject: [PATCH 08/15] Add build badge to readme...

---
 README.md | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/README.md b/README.md
index 9424674..f21ee7e 100644
--- a/README.md
+++ b/README.md
@@ -1,5 +1,7 @@
 # locksmith
 
+![Build workflow](https://github.com/polyvios/locksmith/actions/workflows/build.yml/badge.svg)
+
 Locksmith is a static analysis tool that tries to find data races in multithreaded C programs. To do that, it implements a static version of the Lockset algorithm. A race occurs whenever two threads access a memory location without any synchronization, and one of the accesses is a write. Locksmith analyzes multithreaded programs that use locks (or mutexes) to protect accesses to shared locations, and tries to discover which, if any, locks protect each shared location. Whenever an access to a shared memory location is not protected by any lock, it potentially is a race.
 
 See also [http://www.cs.umd.edu/projects/PL/locksmith/].

From af88c51480b55178d1916f999768abd10ad9eb65 Mon Sep 17 00:00:00 2001
From: Vesal Vojdani <vesal.vojdani@gmail.com>
Date: Tue, 8 Nov 2022 14:48:32 +0000
Subject: [PATCH 09/15] Revert "feature type changed"

This reverts commit 67658e3bc52379677975dee929e2fe401a85a6fc.
---
 src/livevars.ml  | 2 +-
 src/livevars.mli | 2 +-
 src/rmalias.ml   | 3 +--
 src/rmalias.mli  | 2 +-
 4 files changed, 4 insertions(+), 5 deletions(-)

diff --git a/src/livevars.ml b/src/livevars.ml
index 4cf5ee1..65afc6d 100644
--- a/src/livevars.ml
+++ b/src/livevars.ml
@@ -194,7 +194,7 @@ class liveVarsFunVisitor : cilVisitor = object (self)
 end
 
 (* should be disabled by default, debug use only: *)
-let feature : Feature.t =
+let feature : featureDescr =
   { fd_name = "livevars";
     fd_enabled = ref false;
     fd_description = "live variable sets";
diff --git a/src/livevars.mli b/src/livevars.mli
index 24c9569..f8f85a4 100644
--- a/src/livevars.mli
+++ b/src/livevars.mli
@@ -36,5 +36,5 @@
  *)
 val getLiveSet : int -> Usedef.VS.t option
 val computeLiveness : Cil.fundec -> unit
-val feature : Feature.t
+val feature : Cil.featureDescr
 val options : (string * Arg.spec * string) list
diff --git a/src/rmalias.ml b/src/rmalias.ml
index 7240f43..4465cd6 100644
--- a/src/rmalias.ml
+++ b/src/rmalias.ml
@@ -68,7 +68,7 @@ end
 let removeAliasAttr = visitCilFile (new rmAliasVisitor (H.create 1) (H.create 1))
 
 (* should be disabled by default, debug use only: *)
-let feature : Feature.t =
+let feature : featureDescr =
   { fd_name = "rmalias";
     fd_enabled = ref false;
     fd_description = "remove \"alias\" attribute";
@@ -77,4 +77,3 @@ let feature : Feature.t =
     fd_post_check = false;
   }
  
-let () = Feature.register feature
diff --git a/src/rmalias.mli b/src/rmalias.mli
index 53ca967..1095fb0 100644
--- a/src/rmalias.mli
+++ b/src/rmalias.mli
@@ -46,4 +46,4 @@
 val removeAliasAttr : Cil.file -> unit
 
 (* Enables using as a cil module.  Disabled by default *)
-val feature : Feature.t
+val feature : Cil.featureDescr

From accb6b32adc6f72c0e78324cca44a719d7925617 Mon Sep 17 00:00:00 2001
From: Vesal Vojdani <vesal.vojdani@gmail.com>
Date: Tue, 8 Nov 2022 15:28:51 +0000
Subject: [PATCH 10/15] Use ocaml 4.03.0

---
 .github/workflows/build.yml |  2 +-
 README.md                   |  2 +-
 scripts/build.sh            | 14 ++------------
 3 files changed, 4 insertions(+), 14 deletions(-)

diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index b9af631..888e48b 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -12,7 +12,7 @@ jobs:
         os:
           - ubuntu-22.04
         ocaml-compiler:
-          - 3.11.2
+          - 4.03.0
 
     runs-on: ${{ matrix.os }}
 
diff --git a/README.md b/README.md
index f21ee7e..7809465 100644
--- a/README.md
+++ b/README.md
@@ -15,7 +15,7 @@ Clone this repository and run the following in the checked out directory:
 sudo apt install gcc opam autoconf automake make gperf python3 indent emacs flex libfl-dev bison
 git submodule update --init --recursive
 opam init -n
-opam switch create . 3.11.2
+opam switch create . 4.03.0
 eval $(opam env --switch=. --set-switch)
 ./configure
 make
diff --git a/scripts/build.sh b/scripts/build.sh
index 77d50d7..dbdf7e8 100755
--- a/scripts/build.sh
+++ b/scripts/build.sh
@@ -1,15 +1,5 @@
 #!/usr/bin/env bash
-
 eval $(opam config env)
+opam install -y camlp4
 ./configure
-if ! make; then
-  echo "Rebuild banshee"
-  cd banshee
-  make
-  git checkout -- .
-  git clean -df
-  make
-  echo "Now retry Locksmith"
-  cd ..
-  make
-fi
+make

From f0df5e34cb915d4280f9d424292d6c90281f1fcc Mon Sep 17 00:00:00 2001
From: Vesal Vojdani <vesal.vojdani@gmail.com>
Date: Tue, 8 Nov 2022 15:32:01 +0000
Subject: [PATCH 11/15] temporary hack to fix python script

---
 build_funptr_table.py | 80 +++++++++++++++++++++++++++++++++++++++++++
 scripts/build.sh      |  1 +
 2 files changed, 81 insertions(+)
 create mode 100755 build_funptr_table.py

diff --git a/build_funptr_table.py b/build_funptr_table.py
new file mode 100755
index 0000000..d2485a1
--- /dev/null
+++ b/build_funptr_table.py
@@ -0,0 +1,80 @@
+#!/usr/bin/python
+import sys
+import os
+import string
+
+def used_fn(name):
+    used_fns = ["_hash_table_insert","hash_table_insert", "_make_hash_table",
+                "make_hash_table","seed_fn_ptr_table","_seed_fn_ptr_table",
+                "fail","_fail","__fail","calloc","malloc"]
+    return (name in used_fns)
+
+def get_table(libraries):
+    result = []
+    nm = "nm"
+    nmargs = ""
+    for lib in libraries:
+        output = os.popen("%s %s %s" % (nm, nmargs, lib) )
+        for line in output.readlines():
+            entry = line.split();
+            if len(entry) == 3 and ("T" in entry[1]) and not "." in entry[2] and not used_fn(entry[2]):
+                if (entry[2][0] == "_"):
+                    result.append(entry[2][1:])
+                else:
+                    result.append(entry[2])
+    result.sort()
+    return result
+
+def print_preamble():
+    print("#include \"linkage.h\"")
+    print("EXTERN_C_BEGIN")
+    print("typedef void *region;")
+    print("typedef void *hash_table;")
+    print("typedef void (*fn_ptr)(void);")
+    print("hash_table make_hash_table(region r, unsigned long, void *, void *);")
+    print("int hash_table_insert(hash_table,void *,void *);")
+    print("hash_table fn_ptr_table = (void *)0;")
+
+def print_postamble():
+    print("EXTERN_C_END")
+
+def print_protos(table):
+    for entry in table:
+        print(("void %s(void);" % entry))
+
+def print_array(table):
+    print("fn_ptr fn_ptr_array[%d] = {" % len(table))
+    for entry in table:
+        print("%s," % entry)
+    print("};")
+
+def print_hash(table):
+    print("void seed_fn_ptr_table(region r)\n{")
+    print("fn_ptr_table= make_hash_table(r, %d, ptr_hash, ptr_eq);" % len(table))
+    count = 0
+    for entry in table:
+        print("hash_table_insert(fn_ptr_table,%s,(void *)%d);" % (entry, count))
+        count = count + 1
+    print("}\n")
+    print("const int num_fn_ptrs= %d;" % count)
+
+def print_usage_and_exit():
+    print("Usage: %s [file...]" % sys.argv[0])
+    sys.exit(0)
+
+# get all the header files in the current directory
+#def get_headers():
+#    output = os.popen("ls -1 *.h")
+#    return map((lambda x: x[:-1]), output.readlines())
+
+def print_c_file():
+    if (len(sys.argv) <= 1):
+        print_usage_and_exit()
+    table = get_table(sys.argv[1:])
+    print_preamble()
+    print_protos(table)
+    print_array(table)
+    print_hash(table)
+    print_postamble()
+
+print_c_file()
diff --git a/scripts/build.sh b/scripts/build.sh
index dbdf7e8..7d44ef7 100755
--- a/scripts/build.sh
+++ b/scripts/build.sh
@@ -1,4 +1,5 @@
 #!/usr/bin/env bash
+cp build_funptr_table.py banshee/bin/build_funptr_table.py
 eval $(opam config env)
 opam install -y camlp4
 ./configure

From 00ecf31a0f6d3a6938e30eed0469958e4dd28bc9 Mon Sep 17 00:00:00 2001
From: Vesal Vojdani <vesal.vojdani@gmail.com>
Date: Tue, 8 Nov 2022 15:59:56 +0000
Subject: [PATCH 12/15] Will move this ocaml4p outside script.

---
 scripts/build.sh | 1 -
 1 file changed, 1 deletion(-)

diff --git a/scripts/build.sh b/scripts/build.sh
index 7d44ef7..81848be 100755
--- a/scripts/build.sh
+++ b/scripts/build.sh
@@ -1,6 +1,5 @@
 #!/usr/bin/env bash
 cp build_funptr_table.py banshee/bin/build_funptr_table.py
 eval $(opam config env)
-opam install -y camlp4
 ./configure
 make

From ad1c29e6440ba3ff23bedf9d14109c6fff090df2 Mon Sep 17 00:00:00 2001
From: Vesal Vojdani <vesal.vojdani@gmail.com>
Date: Tue, 8 Nov 2022 16:07:51 +0000
Subject: [PATCH 13/15] Add camlp4 to workflow.

---
 .github/workflows/build.yml | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index 888e48b..fc8dec0 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -31,6 +31,9 @@ jobs:
       - name: Install Ubuntu packages
         run: sudo apt install -y gcc autoconf automake make gperf python3 indent emacs flex libfl-dev bison
 
+      - name: Install Opam packages
+        run: opam install -y camlp4 
+          
       - name: Build Locksmith
         run: ./scripts/build.sh
 

From ea12f256d13ceffa76fd3c297cca350b1c1ed5d8 Mon Sep 17 00:00:00 2001
From: Vesal Vojdani <vesal.vojdani@gmail.com>
Date: Tue, 8 Nov 2022 16:20:17 +0000
Subject: [PATCH 14/15] Test other ocaml versions.

---
 .github/workflows/build.yml | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index fc8dec0..9b73cf3 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -13,6 +13,8 @@ jobs:
           - ubuntu-22.04
         ocaml-compiler:
           - 4.03.0
+          - 4.04.2
+          - 4.05.0
 
     runs-on: ${{ matrix.os }}
 

From b10aade19bec99e5f3b7fe4fe8abaff3eedc2084 Mon Sep 17 00:00:00 2001
From: Vesal Vojdani <vesal.vojdani@gmail.com>
Date: Tue, 8 Nov 2022 17:38:39 +0000
Subject: [PATCH 15/15] Revert "Test other ocaml versions." Does not terminate!

This reverts commit ea12f256d13ceffa76fd3c297cca350b1c1ed5d8.
---
 .github/workflows/build.yml | 2 --
 1 file changed, 2 deletions(-)

diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index 9b73cf3..fc8dec0 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -13,8 +13,6 @@ jobs:
           - ubuntu-22.04
         ocaml-compiler:
           - 4.03.0
-          - 4.04.2
-          - 4.05.0
 
     runs-on: ${{ matrix.os }}