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 z3 and its dependencies 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 should be in : /homes/your_user_name/.m2/repository/org/sosy-lab/java-smt/1.0.1

Steps to add Z3 on Windows

1. Download the z3 binaries from here https://github.com/Z3Prover/z3/releases

2. Copy the following files to C:\Documents and Settings\your_user_name.m2\repository\org\sosy-lab\java-smt\native\x86_64-windows

   • libz3.dll
   • libz3java.dll
   • Microsoft.z3.dll

3. Temporary fix (Java-SMT has a bug and requires loading of z3.dll and z3java.dll which is unnecessary)

   • rename Microsoft.z3.dll to z3.dll
   • copy libz3java.dll and name it z3java.dll

In the end you should have the following files in your_path_to_macven_repositories.m2\repository\org\sosy-lab\java-smt\native\x86_64-windows
* libz3.dll * libz3java.dll * z3.dll * z3java.dll 4. Add the com.microsoft.z3.jar (from the Z3 binaries you downloaded earlier in step 1) to the folder where java-smt.jar is. For example, it should be in: C:\Documents and Settings\your_user_name.m2\repository\org\sosy-lab\java-smt\1.0.1

5. To use java-smt with z3 from eclipse, add the path to the z3 related dlls to the java.library.path.

You can do that by choosing from Eclipse Run Configurations -> Go to Arguments tab -> add VM arguments. Add:

-Djava.library.path="C:\Documents and Settings\your_user_name\.m2\repository\org\sosy-lab\java-smt\native\x86_64-windows;${env_var:PATH}"

Annotations

---

Annotations are 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

---

Assertions are 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;  

• Assertions:

  • 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;

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

TODO:

---

• Support only limited expressions in constraints (A && B )
• Currently we parse the assertion nodes twice (should fix that)
• Required changes to Assertion Grammar
  • add not
  • add true and false constants
• Give warning when the type domain is not supported (Currently we only support assertions on Int)
• Introduce Locality The protocol below should not be allowed

@[x<10]
msg(x:Int) from A to B; 
@[x<8]
msg(y:Int) from C to D; // Here the assertion does not refer to the annotated code

• Choice merging (it is a design choice)
• assertion on recursion
• Maybe move the syntactic check to the model checker. Consider the protocol below:

rec Loop {
choice at A {
msg(x:Int) from A to B; 
} or {
msg(z:Int) from A to B; // Here the assertion does not refer to the annotated code
}
}
msg(z) from A to C; // should be allowed. Currently it isn't. the syntactic checks detects that z is not in scope
}