Home

Scribble Extensions: Annotated Payloads and 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/

   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).

   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; // OK 
msg(x) from B to C; 

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

• variables declarations cannot be repeated

msg(x:Int) from A to B; // NOT OK 
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)

@[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 in constraints (A && B )
• Currently we parse the assertion nodes twice (should fix that)

You can try more test cases here:

---

• extensions/annotations
• extensions/assertions

If you want to contribute

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 creating 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

Antlr Grammar for Assertions

Antlr file containing the assertions grammar is Assertion.g