Home

Scribble extended with annotated message payload with assertions.

Prerequisites:

• java-smt

You can install java-smt with maven.

• z3

Unfortunately, there is no maven support for Z3 so you have to install it manually: Here are the instructions from the java-smt site: https://github.com/sosy-lab/java-smt

Here are few tips on troubleshooting from my personal experience. I have tried it so far on iOS and Ubuntu:

Steps to add Z3 on iOS

1. Install from Z3 github:

2. use --java option for make script/python

3. create directory ‘native/x86_64-linux/’ inside the repository of java-smt, which should be smth like: /homes/username/.m2/repository/org/sosy-lab

4. Move the compiled files to native/x86_64-linux/

5. Set the dyl environment in Eclipse as part of your run configuration

Steps to add Z3 on Ubuntu:

1. Download the file from https://www.sosy-lab.org/ivy/org.sosy_lab/javasmt-solver-z3/

   1. You need to download:
   • com.microsoft.z3-z3-4.4.1-1394-gd12efb6.jar
   • libz3-z3-4.4.1-1394-gd12efb6.so
   • libz3java-z3-4.4.1-1394-gd12efb6.so

2. Rename the files as to omit the long numbers (see below). 2. In the end you should have the following files inside folder /homes/rn710/.m2/repository/org/sosy-lab/native/x86_64-linux

   • com.microsoft.z3.jar
   • libz3.so
   • libz3java.so

3. In the folder where the smt-jar is, put the z3 jar and rename it to: com.microsoft.z3.jar

The folder shuold be in : /homes/your_user_name/.m2/repository/org/sosy-lab/java-smt/1.0.1

Terminology, examples, and workflows:

---

• Annotations We call annotations message payloads with data types and variables: For example (x:Int) is an annotated payload in the protocol below: msg(x:Int) from A to B;

All new files related to Annotations are in scribble-core and are prefixed Annot.

Assertions We call assertions the constraints on messages interactions:
For example, @[x<y] is the assertion for the message exchange given below: @[x<y] msg(x:Int) from A to B;

All new files regarding Assertions are in the scribble-assertions module.

What are we checking: Annotations: only knows variables can be forwarded msg(x:Int) from A to B; msg(x) from B to C;

msg(x:Int) from A to B; msg(y) from B to C;

variables declarations cannot be repeated msg(x:Int) from A to B; msg(x:Int) from C to D;

Assertion: Assertion variables are always in scope The assertion constraints do not contradict each other (for the given constraints there is a solution such that all of them can be satisfied)

Example: constraints do not contradict each otehr @[x<10] msg(x:Int) from A to B; @[y>10 && y=x] msg(y:Int) from C to D;
for all variables of past constraints we can find a solution for a current constraint [x<10] MSG(x:Integer) from A to B; [x>y && y>6] MSG(y:Integer) from B to A;

TODO: Sometimes the SMT checker is not terminating (should give a timeout) Support only limited expressions (A && B ) Currently we parse the assertion nodes twice (should fix that)

You can try more test cases here: extensions/annotations extensions/assertions

Z3 checking: FormulaUtil.check() is the main function where the Z3 magic happens. It checks that a given formula A is deducible from another formula B by createing a Z3 formula that says that For all variables in B such that B is satisfiable there exist values for the variables in A such that A is also satisfiable

Assertions: Antlr file containing the assertions grammar is Assertion.g