diff --git a/README.md b/README.md
index 5735af86489a70c07a1c572e2f6d83617eb690a1..32d46ed60e21de821d79fa1016c999babaf6b751 100644
--- a/README.md
+++ b/README.md
@@ -1,95 +1,173 @@
-# javawlp Library
-
-javawlp is a Haskell library that implements Dijkstra's weakest pre-condition transformer that targets the Java programming language.
-Given a statement *stmt* and a post-condition *q*, the transformer *wlp stmt q* calculates the weakest pre-condition for the statement
-to establish the post-condition q. Originally, the transformer is used in the context of a programming logic:
-to prove that a Hoare triple specification *{p} stmt {q}* is valid we can instead prove that the
-implication *p implies (wlp stmt q)* is valid. Over the years, predicate transformers are also used for other purposes,
-such as to aid software testing.
-
-The weakest pre-condition of loops and recursions is unfortunately in general uncomputable. javawlp takes the pragmatic approach
-to unroll loops and recursions some finite number of times (configurable). As such, verification through javawlp falls
-in the category bounded verification.
-
-Copyright (c) 2017, Utrecht University
-
-Authors: Koen Wermer, Wishnu Prasetya
-
-License: GPL
-
-### How to deploy
-
-TO DO: Provide a cabal file.
-
-javawlp is distributed as a Haskell library. The main functions exported by the library can be found in the module `Javawlp.API`.
-
-Example of use:
-
-```
-module Mymodule where
-import Javawlp.API
-test = do -- parse a Java source file; specify the path to the file:
- (tyenv,decls,methods) <- parseJava filepath
- configuration <- defaultConf
- -- specify a post-condition and calculate the wlp:
- p <- wlpMethod configuration tyenv decls (Ident methodname) (post_ "returnValue == 0")
- -- do something with the obtained wlp (p):
- putStrLn (prettyPrint p)
-```
-
-You can check the obtained pre-condition for its satisfiability and obtained the value assignment that
-satisfies it as shown below. This is for example useful to obtain a test case.
-
-```
-module Mymodule where
-import Javawlp.API
-import Z3.Monad
-import Javawlp.Engine.Verifier
-import Javawlp.Engine.HelperFunctions
-test = do -- this part is as in the previous example:
- (tyenv,decls,methods) <- parseJava filepath
- configuration <- defaultConf
- p <- wlpMethod configuration tyenv decls (Ident methodname) (post_ "returnValue == 0")
- -- now check p's satisfiability and print its model:
- let (result,model) = unsafeIsSatisfiable (extendEnv tyenv decls (Ident methodname)) decls p
- case result of
- Sat -> do
- let (Just m) = model
- s <- evalZ3 (modelToString m)
- putStrLn ("SATISFIABLE. Model: " ++ s)
- Unsat -> putStrLn "Not satisfiable."
- _ -> putStrLn "Unable to decide."
-```
-
-### Content
-
-- src: contains javawlp's source files.
-- papers: includes Wermer's original thesis.
-- examples: includes a set of small Java examples you can try as targets for the wlp transformer.
-
-### Dependency
-
-Haskell packages:
-
-- language-java
-- z3 (this is not the actual z3, but provides interface to z3)
-
-Other software:
-
-- You will need the actual z3
-
-### Pre-processing
-
-Some limitations in the current implementation requires the target source code to meet certain
-syntactical constraints; so some pre-processing is required before a source file can be exposed
-to javawlp.
-
-- Reference to an instance member x should be explicitly written as this.x
-
-### IMPRESS EDSL
-
-TODO: Write more information.
-
-#### LogicIR
-
-
\ No newline at end of file
+# IMPRESS EDSL
+
+We want to help students learn about formal program verification. One aspect of this is writing pre and post conditions for their programs. To help the students learn this we developed a tool that can compare two program specifications and can come up with a counter example if the two specifications don't match.
+
+One use case could be to integrate our tool in a submission system like [DOMjudge](https://www.domjudge.org). We then allow students to submit their programs and they get instant feedback on their work.
+
+## Java EDSL
+
+To get started we designed a simple embedded DSL that encapsulates all the expressions taught in the Software Testing & Verification (INFOB3STV) course. This includes:
+
+- Integer expressions (addition, subtraction, multiplication, etc.)
+- Boolean expressions (AND, OR, NOT)
+- Relational operators (bigger, smaller, equal, etc.)
+- Quantifications over integer domains
+- Array access
+
+### Example 1
+
+```java
+public static void swap_spec1(int[] a, int i, int j) {
+ // preconditions
+ pre(a != null);
+ pre(a.length > 0);
+ pre(i >= 0);
+ pre(j >= 0);
+
+ // introducing variables to remember old values
+ int oldai = a[i], oldaj = a[j];
+
+ // call the actual function implementation
+ swap(a, i, j);
+
+ // postconditions
+ post(a[j] == oldai);
+ post(a[i] == oldaj);
+}
+```
+
+This example uses simple arithmetic and shows that multiple pre/post conditions are allowed. Internally they will be appened in a conjunction, but this allows the student to work more easily.
+
+### Example 2
+
+```java
+public static void getMax_spec1(int[] a) {
+ // preconditions
+ pre(a != null);
+ pre(a.length > 0);
+
+ // call the actual function implementation
+ int retval = getMax(a);
+
+ // postconditions
+ post(exists(a, i -> a[i] == retval)); // A
+ post(forall(a, i -> a[i] <= retval)); // B
+}
+```
+
+This example uses the EDSL quantifier functions `exists` and `forall`. In addition to a meaning for the DSL, they also have runtime implementations that allows you to test conditions with concrete values.
+
+Postcondition A will be mapped to:
+
+
+
+Postcondition B will be mapped to:
+
+
+
+### Notes
+
+- Logical implication is currently not supported, but should be easy to add in the DSL is required.
+
+## LogicIR
+
+
+
+To facilitate further development, it was decided to use an intermediate representation for logical expressions. The frontend converts the Java EDSL to the IR and the backend uses IR to implement the comparison of two expressions.
+
+You can find the source code in `src/LogicIR/Expr.hs` TODO
+
+### LogicIR.Frontend
+
+Currently there is only one frontend for the Java EDSL, but this could quite easily be extended to other programming languages.
+
+### LogicIR.Backend.Z3
+
+One of the implemented backends is for the [Z3 Theorem Prover](https://github.com/Z3Prover/z3). The `LogicIR.Expr` is converted to a `Z3 AST`.
+
+To determine if two expressions (`P` and `Q`) are equal, we ask Z3 to prove `P != Q`. There are three possible results:
+
+1. `Sat` -> Z3 proved `P != Q`, which means the two formulas are *not* equivalent. The Z3 model contains the counter example to provide to the student.
+2. `Unsat` -> Z3 proved that `P != Q` does not hold, which means the two formulas are equivalent.
+3. `Undef` -> Z3 was unable to decide the satisfiablity of `P != Q`. In this case we have to resort to other methods like QuickCheck to determine if the two formulas are equivalent or not.
+
+#### Notes
+
+One of the assumptions we make is that both specifications are defined in functions that have the same variable and argument names. That way if we have an array `a` that is used in `P`, we know that if `Q` uses `a` that they refer to the same `a`. See [example 1](#example-1) where both specifications have to refer to the `retval`, `oldi` and `oldj` variables in order to allow Z3 to prove anything.
+
+Something to be wary of when reasoning about this is that we are not trying to prove that an individual specification is satisfiable. We are merely interested in proving that two specifications are equal or not. That said, if you ask Z3 if `ForAll(i, i > 0) != ForAll(i, i < 0)` is satisfiable it will give back `Unsat`, because the formula can be reduced to `False != False` which is false. In practice this should be an issue, because the specification that the student's is compared to will be correct.
+
+#### Null arrays
+
+Currently the expression `a != null` is not really supported because Z3 does not have the concept of null arrays. As a workaround, `null` is represented as an infinite array that maps every index to a constant value that is very unlikely to occur in real code. (TODO: write a counter example). A proposed idea is to represent arrays as a tuple `(IsNull, ArrayData)`, but this requires more semantic analysis of the actual expression to be used. (TODO: give an example, note: usually expressions involving null are short-circuit, unsure...).
+
+#### Array length
+
+Similar to null arrays, Z3 does not (appear to) have the concept of an array length. Currently we use a free variable `a.length` that should represent the array length, but constraints should be added on every `a[E]` in the form of `E >= 0 && E < a.length` to make sure Z3 outputs the `a.length` that corresponds to the array it modeled.
+
+#### Bit vectors
+
+> Modern CPUs and main-stream programming languages use arithmetic over fixed-size bit-vectors. The theory of bit-vectors allows modeling the precise semantics of unsigned and of signed two-complements arithmetic. There are a large number of supported functions and relations over bit-vectors.
+>
+> https://rise4fun.com/z3/tutorialcontent/guide#h25
+
+To implement the semantics of Java (and C#, C++, etc) we use Z3 bit vectors to represent integers. Things like overflow semantics are then handled correctly by Z3.
+
+#### Type checking and type limitations
+
+Currently the implementation only supports the following types:
+
+`int`, `bool`, `int[]`, `bool[]`
+
+Adding additional types (like various integer sizes, `float`) would require some kind of type analysis, which is possible, but would take a considerable amount of time to implement
+
+#### Z3 model parsing
+
+When comparing:
+
+```
+e1:
+exists(a, i -> a[i] == retval) && forall(a, i -> a[i] <= retval)
+
+e2:
+exists(a, i -> a[i] == retval) && forall(a, i -> a[i] < retval)
+```
+
+Z3 will report that `e1 != e2` with the model:
+
+```
+i!1 -> #x00000000
+a.length -> #x00000001
+a -> (_ as-array k!3)
+i!2 -> #x00000000
+retval -> #x00000000
+k!3 -> {
+ #x00000000
+}
+```
+
+This is rather unusable from a user perspective, it should report something like:
+
+```
+Counter example:
+
+a: [0]
+retval: 0
+```
+
+This is currently a work in progress. TODO
+
+#### Side effects
+
+Expressions like `i++ > 0 && i > 1` are not supported because they are considered out of scope for this project.
+
+#### Relevant resources
+
+- https://git.science.uu.nl/d.h.ogilvie2/javawlp/wikis/Resources-about-z3
+- https://git.science.uu.nl/d.h.ogilvie2/javawlp/wikis/home
+
+## TODO
+
+TODO: document usage of haskell code
+TODO: document haskell code itself better
+TODO: latex (https://www.overleaf.com/11599874kpwfhwctdqkr#/43883318/)
diff --git a/javawlp.md b/javawlp.md
new file mode 100644
index 0000000000000000000000000000000000000000..f3b2d3f1ac0bceb80b7045a01583999fd54f685c
--- /dev/null
+++ b/javawlp.md
@@ -0,0 +1,87 @@
+# javawlp Library
+
+javawlp is a Haskell library that implements Dijkstra's weakest pre-condition transformer that targets the Java programming language.
+Given a statement *stmt* and a post-condition *q*, the transformer *wlp stmt q* calculates the weakest pre-condition for the statement
+to establish the post-condition q. Originally, the transformer is used in the context of a programming logic:
+to prove that a Hoare triple specification *{p} stmt {q}* is valid we can instead prove that the
+implication *p implies (wlp stmt q)* is valid. Over the years, predicate transformers are also used for other purposes,
+such as to aid software testing.
+
+The weakest pre-condition of loops and recursions is unfortunately in general uncomputable. javawlp takes the pragmatic approach
+to unroll loops and recursions some finite number of times (configurable). As such, verification through javawlp falls
+in the category bounded verification.
+
+Copyright (c) 2017, Utrecht University
+
+Authors: Koen Wermer, Wishnu Prasetya
+
+License: GPL
+
+### How to deploy
+
+TO DO: Provide a cabal file.
+
+javawlp is distributed as a Haskell library. The main functions exported by the library can be found in the module `Javawlp.API`.
+
+Example of use:
+
+```
+module Mymodule where
+import Javawlp.API
+test = do -- parse a Java source file; specify the path to the file:
+ (tyenv,decls,methods) <- parseJava filepath
+ configuration <- defaultConf
+ -- specify a post-condition and calculate the wlp:
+ p <- wlpMethod configuration tyenv decls (Ident methodname) (post_ "returnValue == 0")
+ -- do something with the obtained wlp (p):
+ putStrLn (prettyPrint p)
+```
+
+You can check the obtained pre-condition for its satisfiability and obtained the value assignment that
+satisfies it as shown below. This is for example useful to obtain a test case.
+
+```
+module Mymodule where
+import Javawlp.API
+import Z3.Monad
+import Javawlp.Engine.Verifier
+import Javawlp.Engine.HelperFunctions
+test = do -- this part is as in the previous example:
+ (tyenv,decls,methods) <- parseJava filepath
+ configuration <- defaultConf
+ p <- wlpMethod configuration tyenv decls (Ident methodname) (post_ "returnValue == 0")
+ -- now check p's satisfiability and print its model:
+ let (result,model) = unsafeIsSatisfiable (extendEnv tyenv decls (Ident methodname)) decls p
+ case result of
+ Sat -> do
+ let (Just m) = model
+ s <- evalZ3 (modelToString m)
+ putStrLn ("SATISFIABLE. Model: " ++ s)
+ Unsat -> putStrLn "Not satisfiable."
+ _ -> putStrLn "Unable to decide."
+```
+
+### Content
+
+- src: contains javawlp's source files.
+- papers: includes Wermer's original thesis.
+- examples: includes a set of small Java examples you can try as targets for the wlp transformer.
+
+### Dependency
+
+Haskell packages:
+
+- language-java
+- z3 (this is not the actual z3, but provides interface to z3)
+
+Other software:
+
+- You will need the actual z3
+
+### Pre-processing
+
+Some limitations in the current implementation requires the target source code to meet certain
+syntactical constraints; so some pre-processing is required before a source file can be exposed
+to javawlp.
+
+- Reference to an instance member x should be explicitly written as this.x
\ No newline at end of file
diff --git a/src/LogicIR/Backend/Pretty.hs b/src/LogicIR/Backend/Pretty.hs
index 019bb2acb1b994166c5349d17f4ed3794c2b9962..cf793e97751116300ed2c42c641caf73d0d1fc0c 100644
--- a/src/LogicIR/Backend/Pretty.hs
+++ b/src/LogicIR/Backend/Pretty.hs
@@ -1,3 +1,5 @@
+-- Very crude pretty printer for debugging, should not be used in production!
+
module LogicIR.Backend.Pretty (prettyLExpr) where
import Data.List
diff --git a/src/LogicIR/Backend/Z3.hs b/src/LogicIR/Backend/Z3.hs
index 93b5c9e3ea77532c139958d91cdbc24a72d6e48d..fe4cd9f648eb735372d7c90b005f4fca20196153 100644
--- a/src/LogicIR/Backend/Z3.hs
+++ b/src/LogicIR/Backend/Z3.hs
@@ -22,7 +22,7 @@ lExprToZ3AstAlgebra = (flConst, flVar, flNot, flBinop, flComp, flQuant, flArray,
TArray (TPrim PBool) -> do intSort <- mkBvSort 32
arraySort <- mkBoolSort >>= mkArraySort intSort
mkVar symbol arraySort
- _ -> error $ show n
+ _ -> error $ "unsupported type: " ++ show n
flNot a = a >>= mkNot
flBinop a' o b' = do a <- a'
b <- b'
@@ -45,12 +45,12 @@ lExprToZ3AstAlgebra = (flConst, flVar, flNot, flBinop, flComp, flQuant, flArray,
case o of
QAll -> mkForallConst [] [vApp] a
QAny -> mkExistsConst [] [vApp] a
- _ -> error $ show (o, v)
+ _ -> error $ "unsupported quantifier domain type: " show (o, v)
flArray v a' = do v <- flVar v
a <- a'
mkSelect v a
flNil = do intSort <- mkBvSort 32
- zero <- mkBitvector 32 0 -- (isNull, data, length) TODO
+ zero <- mkBitvector 32 0 -- (isNull, data, length) TODO: support proper null types
mkConstArray intSort zero
fnConst n = mkBitvector 32 (fromIntegral n)
fnUnop o a' = do a <- a'
@@ -74,4 +74,4 @@ lExprToZ3AstAlgebra = (flConst, flVar, flNot, flBinop, flComp, flQuant, flArray,
a <- a'
b <- b'
mkIte c a b
- fnLen (Var (TArray (TPrim _)) n) = mkStringSymbol (n ++ ".length") >>= flip mkBvVar 32
+ fnLen (Var (TArray (TPrim _)) n) = mkStringSymbol (n ++ ".length") >>= flip mkBvVar 32 -- TODO: support proper array lengths
diff --git a/src/LogicIR/Expr.hs b/src/LogicIR/Expr.hs
index 605a48ff67a9821ce460e9e03489487f6f6bfef3..0d0f589e2455b9d189a732b73b90668e7d68d5f5 100644
--- a/src/LogicIR/Expr.hs
+++ b/src/LogicIR/Expr.hs
@@ -1,12 +1,13 @@
module LogicIR.Expr where
--- TODO: pretty printer
--- Based on my (Duncan's) previous work: https://github.com/mrexodia/wp/blob/master/Wp.hs
+-- Based on previous work: https://github.com/mrexodia/wp/blob/master/Wp.hs
+-- The primitive types are bool and int32.
data Primitive = PBool
| PInt32
deriving (Show, Eq, Read)
+-- A Type can either be a primitive or an array of Type
data Type = TPrim Primitive
| TArray Type
deriving (Show, Eq, Read)
@@ -54,9 +55,10 @@ data COp = CEqual -- a == b
| CGeq -- a >= b
deriving (Show, Eq, Read)
+-- Logical and numeral expressions are the same type, but an alias is added for clarity.
type NExpr = LExpr
--- Logical expressions (TODO: clean up duplicates)
+-- Logical expressions
data LExpr = LConst Bool -- True/False
| LVar Var -- Variable
| LNot LExpr -- Logical negation/not
diff --git a/src/LogicIR/Frontend/Java.hs b/src/LogicIR/Frontend/Java.hs
index d2cbd8ebf0a81a60947d207a24b7b9a563eef404..f5c6072da64a54a6b36cb12c46a3dba40c47af7c 100644
--- a/src/LogicIR/Frontend/Java.hs
+++ b/src/LogicIR/Frontend/Java.hs
@@ -14,6 +14,7 @@ import Data.Typeable
javaExpToLExpr :: Exp -> TypeEnv -> [TypeDecl] -> LExpr
javaExpToLExpr = foldExp javaExpToLExprAlgebra
+-- Converts a name to a LogicIR.Var, it queries the type environment to find the correct type.
nameToVar :: Name -> TypeEnv -> [TypeDecl] -> Var
nameToVar name env decls = let (arrayType, symbol) = (lookupType decls env name, prettyPrint name) in
case arrayType of
@@ -34,13 +35,20 @@ javaExpToLExprAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation,
fThisClass = error "fThisClass not supported..."
fInstanceCreation = error "fInstanceCreation not supported..."
fQualInstanceCreation = error "fQualInstanceCreation not supported..."
- fArrayCreate = undefined
- fArrayCreateInit = undefined
- fFieldAccess = undefined
- fMethodInv inv env decls = case inv of -- TODO: very hardcoded EDSL + lambdas cannot be { return expr; }
+ fArrayCreate = error "fArrayCreate not supported..."
+ fArrayCreateInit = error "fArrayCreateInit not supported..."
+ fFieldAccess = undefined {-case fieldAccess of -- TODO: implement field accesses
+ PrimaryFieldAccess e id -> case e of
+ InstanceCreation _ t args _ -> undefined
+ _ -> undefined
+ SuperFieldAccess id -> mkStringSymbol (prettyPrint (Name [id])) >>= mkIntVar
+ ClassFieldAccess (Name name) id -> mkStringSymbol (prettyPrint (Name (name ++ [id]))) >>= mkIntVar -}
+ fMethodInv inv env decls = case inv of -- TODO: very hardcoded EDSL + lambdas cannot be { return expr; } + ranged
+ -- Java: forall(name, bound -> expr);
MethodCall (Name [Ident "forall"]) [ExpName name, Lambda (LambdaSingleParam (Ident bound)) (LambdaExpression expr)]
-> let (i, arr) = (Var (TPrim PInt32) bound, nameToVar name env decls) in
LQuant QAll i (LBinop (LBinop (LComp (LVar i) CGeq (NConst 0)) LAnd (LComp (LVar i) CLess (NLen arr))) LImpl (foldExp javaExpToLExprAlgebra expr env decls))
+ -- Java: exists(name, bound -> expr);
MethodCall (Name [Ident "exists"]) [ExpName name, Lambda (LambdaSingleParam (Ident bound)) (LambdaExpression expr)]
-> let (i, arr) = (Var (TPrim PInt32) bound, nameToVar name env decls) in
LQuant QAny i (LBinop (LBinop (LComp (LVar i) CGeq (NConst 0)) LAnd (LComp (LVar i) CLess (NLen arr))) LAnd (foldExp javaExpToLExprAlgebra expr env decls))
@@ -48,10 +56,10 @@ javaExpToLExprAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation,
-> error $ "Unimplemented fMethodInv: " ++ show inv
fArrayAccess arrayIndex env decls = case arrayIndex of -- TODO: type checking
ArrayIndex (ExpName name) [expr]
- -> LArray (nameToVar name env decls) (javaExpToLExpr expr env decls) -- (LVar (nameToVar index env decls))
+ -> LArray (nameToVar name env decls) (javaExpToLExpr expr env decls)
_
-> error $ "Multidimensional arrays are not supported: " ++ show (arrayIndex)
- fExpName name env decls = case name of -- TODO: type checking
+ fExpName name env decls = case name of -- TODO: type checking + check implicit `this.name`
Name [Ident a, Ident "length"] -> NLen $ nameToVar (Name [Ident a]) env decls
_ -> LVar $ nameToVar name env decls
fPostIncrement = error "fPostIncrement has side effects..."
@@ -62,7 +70,7 @@ javaExpToLExprAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation,
fPreMinus e env decls = NUnop NNeg (e env decls)
fPreBitCompl e env decls = NUnop NNot (e env decls)
fPreNot e env decls = LNot (e env decls)
- fCast = undefined -- TODO: perhaps support cast for some types?
+ fCast = error "fCast is not supported..." -- TODO: perhaps support cast for some types?
fBinOp e1 op e2 env decls = let (a, b) = (e1 env decls, e2 env decls) in -- TODO: type checking?
case op of
-- Integer
@@ -87,7 +95,7 @@ javaExpToLExprAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation,
GThanE -> LComp a CGeq b
Equal -> LComp a CEqual b
NotEq -> LComp a CNEqual b
- fInstanceOf = undefined
+ fInstanceOf = error "fInstanceOf is not supported..."
fCond c a b env decls = NIf (c env decls) (a env decls) (b env decls)
fAssign = error "fAssign has side effects..."
fLambda = error "fLambda should be handled by fMethodInv..."
diff --git a/src/SimpleFormulaChecker.hs b/src/SimpleFormulaChecker.hs
index 22d5505339dcc1e2f0f518da5416dc2c3219c663..455cd08fceceda63b4479eeb4a7218c7490731e1 100644
--- a/src/SimpleFormulaChecker.hs
+++ b/src/SimpleFormulaChecker.hs
@@ -4,6 +4,7 @@ import Language.Java.Syntax
import Language.Java.Parser
import Language.Java.Pretty
import Z3.Monad
+import Z3.Opts
import Data.Maybe
import Javawlp.Engine.Types
@@ -19,47 +20,7 @@ import Control.Monad.Trans (liftIO)
import Debug.Trace
-{-
-
-Hi Duncan, I have written this simple Haskell program that shows you how to use some parts of this
-Javawlp library for your purpose. The function "checkformula" below can be used to parse
-a Java class of the form:
-
- class C {
- boolean f1(x,y,z) { return e1 ; }
- boolean f2(... ) { return e2 ; }
- ...
- }
-
-There is an example of such a class in "examples/DuncanExample.java". For e demo, call:
-
- checkformula "../examples/DuncanExample.java" "f1"
- checkformula "../examples/DuncanExample.java" "f2"
- checkformula "../examples/DuncanExample.java" "f3"
-
-Each time, it will grab the formula in "return e" of the specified method, and will pass it to
-Z3 to be checked if the formula is satisfiable. If it is, satisfying instances of the formula's free
-variables will be printed.
-
-The starting point to see of to ask Z3 to check Java's formula is the fuunction "unsafeIsSatisfiable"
-in the module Verifier. This in turn calls "foldExp expAssertAlgebra expr" to translate expr to
-an representation for Z3.
-
-Some notes on the demo:
-
- ** To simplify the demo, the method-names must uniquely identify them.
-
- ** The used Java-parser library is a 3rd party. Unfortunately it is not that sophisticated.
- It seems to be blind to Java's operators' priorities.
- To parse e.g. x<0 || x>0 we have to explicityly brackets the sub-expressions: (x<0) || (x>0).
-
-
-Dependencies:
-
- * Haskell package: language-java
- * Haskell package: z3, which then also need z3 binary/lib
-
--}
+-- See README.md for more details.
type MethodDef = ([TypeDecl], Stmt, TypeEnv)
@@ -89,6 +50,7 @@ parseMethod (src, name) = do
Left parseError -> error (show parseError)
Right compUnit -> return compUnit
+-- Get a list of all calls to a method of a specific name from a method definition.
getMethodCalls :: MethodDef -> String -> [MethodInvocation]
getMethodCalls (_, StmtBlock (Block bs), _) name = catMaybes (map extractMethodInv bs)
where
@@ -96,20 +58,14 @@ getMethodCalls (_, StmtBlock (Block bs), _) name = catMaybes (map extractMethodI
extractMethodInv (BlockStmt (ExpStmt (MethodInv i@(MethodCall (Name [Ident n]) _)))) = if n == name then Just i else Nothing
extractMethodInv _ = Nothing
-combineExprs :: Op -> [Exp] -> Exp
-combineExprs o (e:[]) = e
-combineExprs o (e:es) = BinOp e o (combineExprs o es)
+-- [pre(a), pre(b), pre(c)] -> (a AND b AND c)
+extractExpr :: [MethodInvocation] -> Exp
+extractExpr call = combineExprs $ map (\(MethodCall (Name [Ident _]) [a]) -> a) call
+ where combineExprs :: [Exp] -> Exp
+ combineExprs (e:[]) = e
+ combineExprs (e:es) = BinOp e CAnd (combineExprs es)
-andExprs :: [Exp] -> Exp
-andExprs = combineExprs CAnd
-
-orExprs :: [Exp] -> Exp
-orExprs = combineExprs COr
-
-extractExpr :: Op -> [MethodInvocation] -> Exp
-extractExpr op call = combineExprs op $ map (\(MethodCall (Name [Ident _]) [a]) -> a) call
-
--- | Check if two formulas are equivalent
+-- Check if two Z3 AST's are equivalent
isEquivalent :: Z3 AST -> Z3 AST -> IO (Result, Maybe Model)
isEquivalent ast1' ast2' = evalZ3 z3
where
@@ -123,12 +79,10 @@ isEquivalent ast1' ast2' = evalZ3 z3
solverReset
return r
-showZ3AST :: Z3 AST -> IO String
-showZ3AST ast' = evalZ3 $ ast' >>= astToString
-
+-- Determine the equality of two method's pre/post conditions.
determineFormulaEq :: MethodDef -> MethodDef -> String -> IO ()
determineFormulaEq m1@(decls1, mbody1, env1) m2@(decls2, mbody2, env2) name = do
- -- get preconditions
+ -- get pre/post condition
let (e1, e2) = (extractCond m1 name, extractCond m2 name)
let (lexpr1, lexpr2) = (javaExpToLExpr e1 env1 decls1, javaExpToLExpr e2 env2 decls2)
let (ast1, ast2) = (lExprToZ3Ast lexpr1, lExprToZ3Ast lexpr2)
@@ -146,16 +100,21 @@ determineFormulaEq m1@(decls1, mbody1, env1) m2@(decls2, mbody2, env2) name = do
case result of
Unsat -> putStrLn "formulas are equivalent!"
Undef -> putStrLn "unable to decide the satisfiablity (TODO: use QuickCheck)"
- _ -> do
+ Sat -> do
putStrLn "formulas are NOT equivalent, model:"
case model of
- Just m -> do s <- evalZ3 (modelToString m)
+ Just m -> do env <- newItpEnv Nothing (Z3.Opts.opt ":pp.bv-literals" False)
+ s <- evalZ3WithEnv (modelToString m) env
putStr s
_ -> return ()
where
extractCond :: MethodDef -> String -> Exp
- extractCond m n = extractExpr CAnd (getMethodCalls m n)
+ extractCond m n = extractExpr (getMethodCalls m n)
+ showZ3AST :: Z3 AST -> IO String
+ showZ3AST ast' = evalZ3 $ ast' >>= astToString
+-- Function that compares both the pre and the post condition for two methods.
+-- It is assumed that both methods have the same environment (parameter names, class member names, etc).
compareSpec :: (FilePath, String) -> (FilePath, String) -> IO ()
compareSpec method1@(_, name1) method2@(_, name2) = do
-- load the methods