To protect your credential, you can use the following command to clone the repo
git clone git://github.com/knotical/knotical.git
or download the single zip file from the URL https://github.com/knotical/knotical/archive/v1.0.zip
-
Install Docker. Follow the instructions on https://docs.docker.com/install/. You may need to run
docker
commands withsudo
or similar privileges. -
Build the Knotical image:
docker build -t knotical .
-
Run the Knotical image:
docker run -it knotical bash
NOTE: The following instructions have been tested on Ubuntu 18.04 LTS with opam
1.2.2. You may need to run apt-get
commands with the sudo
privilege.
-
Install Prerequisites:
apt-get clean apt-get update apt-get install -qy libppl-dev libmpfr-dev m4 subversion gawk lynx
-
Install
opam
:apt-get install opam opam init
You can follow the instructions on https://opam.ocaml.org/doc/Install.html to install the latest
opam
2.0.4. You may need to installgcc
,g++
, andmake
before doing that. -
Install OCaml via
opam
:opam switch 4.06.1 eval `opam config env`
-
Install Dependencies via
opam
:opam install oasis ocamlbuild opam install apron conf-ppl camllib safa batteries camlp4 core ocamlgraph eval `opam config env`
-
Install
Fixpoint
(http://pop-art.inrialpes.fr/people/bjeannet/bjeannet-forge/fixpoint/):svn checkout https://scm.gforge.inria.fr/anonscm/svn/bjeannet/pkg/fixpoint/ cd fixpoint/trunk/ cp Makefile.config.model Makefile.config make make install
-
Compile Knotical:
oasis setup make
-cmp
or-cmpLt
: Find the trace refinement relations of the two methods for equality (cmp
) or refinement (cmpLt
)-no-rem
: Specify the list of events/methods that cannot be removed or replaced-depth
: Specify the depth of proof search
-
For instance, the following command line runs the tool Knotical on the motivating example (
bench/01sendrecv.c
) to find trace refinement relations under which the first methodC2
refines the second methodC1
, given that the methodssend
,recv
, andconstructReply
aren't removed./knotical.native -cmpLt C2 C1 -no-rem send,recv,constructReply bench/01sendrecv.c
-
The result contains multiple refinement relations represented in the form of trees. A solution tree is complete (
C
) or partial (P
) in the sense that whether or not different restrictions in its refinement relations applied to the input methods, when taken together cover all behaviors of the first method (in case ofcmpLt
) or both (in case ofcmp
). For example, the following solution tree is one of the results returned by Knotical for the motivating example. It is a complete solution because there are refinement relations corresponding to all cases in the first methodC2
(marked by@1
).(C) d_30@2: |_ d_30@2 (C) b_12@1: |_ b_12@1 |_ (A) {I=1, J=1, K=1, M=1} GenAxiom {I=1} {I: ((L37 C9), () = log(b);)} -> Case d_30 {d: ((L14 C13), c > 0)} -> GenAxiom {J=1} {J: ((L14 C13), () = log(b);)} -> Case b_12 {b: ((L32 C18), auth > 0)} -> GenAxiom {K=1} {K: ((L19 C15), () = log(n);)} -> GenAxiom {M=1} {M: ((L30 C10), auth = check(b);)} -> (a_8.V_16.(c_15.M_57.C_11.S_10 + !c_15.I_33).X_9)*.!a_8 <= (a_22.V_31.J_34.(c_28.C_27.S_26.K_56 + !c_28).X_23)*.!a_22 |_ !b_12@1 (C) c_28@2: |_ c_28@2: No solutions |_ !c_28@2 |_ (A) {I=1, J=1, K=1} GenAxiom {I=1} {I: ((L37 C9), () = log(b);)} -> Case d_30 {d: ((L14 C13), c > 0)} -> GenAxiom {J=1} {J: ((L14 C13), () = log(b);)} -> Case !b_12 {b: ((L32 C18), auth > 0)} -> Case !c_28 {c: ((L16 C13), b > 0)} -> GenAxiom {K=1} {K: ((L30 C10), auth = check(b);)} -> (a_8.V_16.(c_15.K_61 + !c_15.I_33).X_9)*.!a_8 <= (a_22.V_31.J_34.X_23)*.!a_22 |_ !d_30@2 ...
The first refinement relation shows that when
log
are removed in both methods (expressed by the axiomsI=1
,J=1
, andK=1
) and the authorizationauth
inC2
is always successful (i.e., the case ofb_12
corresponding to the conditionauth > 0
) thenC2
refinesC1
.
-
To reproduce the entire experiment on the 37 benchmark programs in
bench
, runbin/runAll.sh
-
The experimental result is in the folder
results-YYYYMMDD-hhmmss
whereYYYYMMDD-hhmmss
is the timestamp when the script was run. The fileresults-YYYYMMDD-hhmmss/SUMMARY.html
represents the summary result (Table 1 in the paper) in HTML format. You can open the fileSUMMARY.html
using your preferred web browser. If you are running Knotical's Docker image, you can uselynx
to view the file within the terminal.lynx results-YYYYMMDD-hhmmss/SUMMARY.html
For example, SUMMARY.html is the experimental result running on a MacBook Pro with a 3.5 GHz Intel Core i7 CPU and 16GB RAM.
This work is supported by Office of Naval Research under Grant No.: N00014-17-1-2787.