pgoodman / pagai Goto Github PK
View Code? Open in Web Editor NEWThis project forked from julienhenry/pagai
License: Other
This project forked from julienhenry/pagai
License: Other
* INSTALLATION: PAGAI needs: - GMP and MPFR. On Debian systems, install packages: libmpfr-dev libgmp3-dev - CMake, for the compilation. On Debian systems, install packages: cmake (you may want to install cmake-gui too for a graphical configuration tool) - Yices, Z3, CUDD, LLVM, Apron and the PPL (can be automatically installed for you). See the top of external/Makefile for required versions of these tools. In particular, Pagai won't work if you don't have the exact version of LLVM. - curl or wget, if you want automatic dependencies installation. The simplest way to compile PAGAI is to run: ./autoinstall.sh from the toplevel. This will download and compile most dependencies for you (it takes time, and ~550Mb of disk space). PARALLEL_MAKE_OPTS=-j4 ./autoinstall.sh will compile dependencies trying to use 4 cores (adjust as needed). If you don't want the dependencies to be installed for you, run: cmake . make from the toplevel. Alternatively, one can use an out-of-tree build with: mkdir build ../autoinstall-out-of-tree.sh or, without the external dependency installation: mkdir build cd build cmake .. make Variables (path to libraries, build options, ...) can be set for each build with e.g. cmake -DSTATIC_LINK=ON . cmake -i . cmake-gui . For running Pagai, you should make sure your PATH variable contains the directory of the SMT solver you want to use (e.g. Z3, CVC4, etc.) On MacOS, please compile with clang and not g++: there are strange template instantiations errors with g++, leading to duplicate symbols when linking. * Optional APRON extensions PAGAI can use APRON linked with - the Parma Polyhedra Library http://bugseng.com/products/ppl/ (-DENABLE_PPL) - OptOptagons, from ETHZ https://github.com/eth-srl/OptOctagon (-DENABLE_OPT_OCT) * USAGE: - With a C input If you want to use Pagai with a C input, you first need to setup a pagai.conf file in the same directory as the Pagai executable. This conf file contains only one variable so far, named ResourceDir. This variable should be set to the path of your LLVM/Clang installation. In particular, make sure you set ResourceDir so that the path $(ResourceDir)/lib/clang/3.4/include/ exists and contains e.g. float.h. The pagai.conf file should have the form: "ResourceDir <dir>" example: --> cat pagai.conf ResourceDir /Users/julien/work/pagai/external/llvm - With a LLVM .bc input The pagai.conf file is only used for compiling C/C++ code into LLVM bitcode. If you directly give to Pagai a bitcode file, it will process it. Note that you will need to compile into bitcode with clang and the -g and -emit-llvm arguments. pagai -h should give you the list of arguments: Options: -i [ --input ] arg input -h [ --help ] Print help messages -I [ --include-path ] arg include path (same as -I for clang) -s [ --solver ] arg (=z3_api) * z3 * z3_qfnra * mathsat * smtinterpol * cvc3 * cvc4 * z3_api -d [ --domain ] arg (=pk) abstract domain * box (Apron boxes) * oct (Octagons) * pk (NewPolka strict polyhedra) * pkeq (NewPolka linear equalities) -t [ --technique ] arg (=lw+pf) technique * lw (Lookahead Widening, SAS'06) * g (Guided Static Analysis, SAS'07) * pf (Path Focusing, SAS'11) * lw+pf (SAS'12) * s (simple abstract interpretation) * dis (lw+pf, using disjunctive invariants) * pf_incr * incr --new-narrowing When the decreasing sequence fails (SAS12) --main arg label name of the entry point --no-undefined-check no undefined check --pointers pointers --optimize optimize --instcombining instcombining --loop-unroll unroll loops --skipnonlinear ignore non linear arithmetic --noinline do not inline functions -o [ --output ] arg C output --output-bc arg LLVM IR output --output-bc-v2 arg LLVM IR output (v2) --svcomp SV-Comp mode --wcet wcet mode --debug debug -c [ --compare ] arg compare list of techniques --comparedomains compare abstract domains --printformula print SMT formula --printall print all --quiet quiet mode --dump-ll dump analyzed ll file --force-old-output use old output --timeout arg timeout --log-smt write all the SMT requests into a log file --annotated arg name of the annotated C file --domain2 arg not for use --new-narrowing2 not for use * EXAMPLE --> ./pagai ../ex/wcet_bicycle2.c // ResourceDir is /Users/julien/work/pagai/external/llvm/lib/clang/3.4 // analysis: AIopt /* processing Function bicycle */ #include "../pagai_assert.h" void bicycle() { int /* reachable */ count=0, phase=0; for(int i=0; i<10000; // safe i++) { /* invariant: -2*count+phase+3*i = 0 14998-count+phase >= 0 1-phase >= 0 phase >= 0 count-2*phase >= 0 */ if (phase == 0) { // safe count += 2; phase = 1; } else if (phase == 1) { // safe count += 1; phase = 0; } } /* assert OK */ assert(count <= 15000); /* reachable */ }
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.