Skip to content

Latest commit

 

History

History
74 lines (59 loc) · 2.27 KB

README.md

File metadata and controls

74 lines (59 loc) · 2.27 KB
Raw

zorro

Integer bit hacks and architecture-independent compiler_rt in Zig optimized for 2s complement and verified in Z3

Code has 0BSD license, proofs have MIT license. The license of Z3 is inside the cloned folder z3.

Dependencies

To reduce maintenance cmake and ninja with python are required and a zig from master branch to use zig with integrated libclang as c and c++ compiler. Zig from master branch is available here for download, can be bootstrapped here or build with the instructions from the wiki.

WIP.

Structure

Folder prefixed with p for corresponding proofs.

  • crt for compiler_rt

Building

Run these commands, unless there is an error.

git clone --depth=1 https://github.com/Z3Prover/z3 z3
cd z3
mkdir -p build
cd build
# regular
CC='zig cc -fno-sanitize=all' CXX='zig c++ -fno-sanitize=all' cmake -GNinja ../
# if checking for UB
CC='zig cc' CXX='zig c++' cmake -GNinja ../
# checking for UB
ninja          # build z3 with libclang integrated in zig
cd ..

zig build      # build binary
# workaround of https://github.com/ziglang/zig/issues/10785
cd zig-out
./bin/runProofs
cd ..

Todos

  • building z3
  • building and linking c++ programs with z3 proofs
  • fix zig build to run the proofs (ziglang/zig#10785)
  • architecture-independent compiler_rt
  • verify compiler_rt
  • list of all integer bit-hacks (0BSD)
  • implement common bit-hacks (0BSD)
  • verify common bit-hacks (MIT)
  • link or explain common theories and techniques (check license that arxiv uses)

experiments

  • z3 c bindings used in zig
  • extract arithmetic from zig compiler of a fn block as stmlib2 string
  • generate edge cases for testing from z3 proofs

Ressources