GitHub action

.github/workflows/build.yml

@@ -0,0 +1,42 @@
+name: Build workflow
+
+on:
+  - pull_request
+  - push
+
+jobs:
+  build:
+    strategy:
+      fail-fast: false
+      matrix:
+        os:
+          - ubuntu-22.04
+        ocaml-compiler:
+          - 4.03.0
+
+    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 }}
+          opam-depext: false
+
+      - 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
+
+      - name: Test
+        run: ./scripts/test.sh
+

README.md

@@ -1,20 +1,22 @@
 # 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/].
 
 ## 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 libfl-dev bison
 git submodule update --init --recursive
 opam init -n
-opam switch create . 3.11.2
-eval $(opam env)
+opam switch create . 4.03.0
+eval $(opam env --switch=. --set-switch)
 ./configure
 make
 ```

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()

scripts/build.sh

@@ -0,0 +1,5 @@
+#!/usr/bin/env bash
+cp build_funptr_table.py banshee/bin/build_funptr_table.py
+eval $(opam config env)
+./configure
+make

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

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";

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

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

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