diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml new file mode 100644 index 0000000..fc8dec0 --- /dev/null +++ b/.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 + diff --git a/README.md b/README.md index a782603..7809465 100644 --- a/README.md +++ b/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 ``` 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 new file mode 100755 index 0000000..81848be --- /dev/null +++ b/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 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 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