diff --git a/src/LogicIR/Backend/Z3.hs b/src/LogicIR/Backend/Z3.hs
index eed52c1d3c51cabad3873b7176bd343919995729..c57a27ef8478aa7f4707e4e80839f1490c69cc05 100644
--- a/src/LogicIR/Backend/Z3.hs
+++ b/src/LogicIR/Backend/Z3.hs
@@ -5,26 +5,20 @@ import Z3.Monad
import LogicIR.Expr
import LogicIR.Fold
-nExprToZ3Ast :: NExpr -> Z3 AST
-nExprToZ3Ast = foldNExpr nExprToZ3AstAlgebra
-
-nExprToZ3AstAlgebra :: NExprAlgebra (Z3 AST)
-nExprToZ3AstAlgebra = (fConst, fVar, fUnop, fBinop, fArray) where
- fConst = undefined
- fVar = undefined
- fUnop = undefined
- fBinop = undefined
- fArray = undefined
-
lExprToZ3Ast :: LExpr -> Z3 AST
lExprToZ3Ast = foldLExpr lExprToZ3AstAlgebra
lExprToZ3AstAlgebra :: LExprAlgebra (Z3 AST)
-lExprToZ3AstAlgebra = (fConst, fVar, fNot, fBinop, fComp, fQuant, fArray) where
- fConst = undefined
- fVar = undefined
- fNot = undefined
- fBinop = undefined
- fComp = undefined
- fQuant = undefined
- fArray = undefined
\ No newline at end of file
+lExprToZ3AstAlgebra = (flConst, flVar, flNot, flBinop, flComp, flQuant, flArray, fnConst, fnVar, fnUnop, fnBinop, fnArray) where
+ flConst = undefined
+ flVar = undefined
+ flNot = undefined
+ flBinop = undefined
+ flComp = undefined
+ flQuant = undefined
+ flArray = undefined
+ fnConst = undefined
+ fnVar = undefined
+ fnUnop = undefined
+ fnBinop = undefined
+ fnArray = undefined
\ No newline at end of file
diff --git a/src/LogicIR/Expr.hs b/src/LogicIR/Expr.hs
index b64cdfedebad9ed6d4fc805ba839de9f85c1880d..e33d57248115076a0c5c2e8ba696296f8bf1c896 100644
--- a/src/LogicIR/Expr.hs
+++ b/src/LogicIR/Expr.hs
@@ -1,5 +1,6 @@
module LogicIR.Expr where
+-- TODO: pretty printer
-- Based on my (Duncan's) previous work: https://github.com/mrexodia/wp/blob/master/Wp.hs
data Primitive = PBool
@@ -32,14 +33,6 @@ data NBinop = NAdd
| NXor
deriving (Show, Eq, Read)
--- Numeral expressions
-data NExpr = NConst Int -- Integer constant
- | NVar Var -- Variable
- | NUnop NUnop NExpr -- Unary operator
- | NBinop NExpr NBinop NExpr -- Binary operators
- | NArray Var NExpr -- Integer array access
- deriving (Show, Eq, Read)
-
-- Reference: https://en.wikipedia.org/wiki/First-order_logic#Logical_symbols
-- Logical operators
@@ -54,13 +47,16 @@ data QOp = QAll | QAny
deriving (Show, Eq, Read)
-- Comparison operators
-data COp = CEqual
- | CLess
- | CGreater
- | CLeq
- | CGeq
+data COp = CEqual -- a == b
+ | CNEqual -- a != b
+ | CLess -- a < b
+ | CGreater -- a > b
+ | CLeq -- a <= b
+ | CGeq -- a >= b
deriving (Show, Eq, Read)
+type NExpr = LExpr
+
-- Logical expressions
data LExpr = LConst Bool -- True/False
| LVar Var -- Variable
@@ -68,5 +64,11 @@ data LExpr = LConst Bool -- True/False
| LBinop LExpr LBinop LExpr -- Logical operator
| LComp NExpr COp NExpr -- Integer comparison
| LQuant QOp [Var] LExpr -- Logical quantifier
- | LArray Var NExpr -- Logical array access (TODO: remove?)
+ | LArray Var [NExpr] -- Logical array access (TODO: remove?)
+
+ | NConst Int -- Integer constant
+ | NVar Var -- Variable
+ | NUnop NUnop NExpr -- Unary operator
+ | NBinop NExpr NBinop NExpr -- Binary operators
+ | NArray Var [NExpr] -- Integer array access
deriving (Show, Eq, Read)
\ No newline at end of file
diff --git a/src/LogicIR/Fold.hs b/src/LogicIR/Fold.hs
index dc7a63c2e509a515b027dbf6be81b0e6819aeb9c..3aec005d6616cf900770a70bb9499da038e165ab 100644
--- a/src/LogicIR/Fold.hs
+++ b/src/LogicIR/Fold.hs
@@ -2,42 +2,34 @@ module LogicIR.Fold where
import LogicIR.Expr
--- Fold algrbra for numeral expressions
-type NExprAlgebra r = (Int -> r, -- NConst
- Var -> r, -- NVar
- NUnop -> r -> r, -- NUnop
- r -> NBinop -> r -> r, -- NBinop
- Var -> r -> r -- NArray
- )
-
--- Fold for numeral expressions
-foldNExpr :: NExprAlgebra r -> NExpr -> r
-foldNExpr (fConst, fVar, fUnop, fBinop, fArray) = fold where
- fold e = case e of
- NConst n -> fConst n
- NVar n -> fVar n
- NUnop o e -> fUnop o (fold e)
- NBinop a o b -> fBinop (fold a) o (fold b)
- NArray n e -> fArray n (fold e)
-
-- Fold algebra for logical expressions
type LExprAlgebra r = (Bool -> r, -- LConst
Var -> r, -- LVar
r -> r, -- LNot
r -> LBinop -> r -> r, -- LBinop
- NExpr -> COp -> NExpr -> r, -- LComp
+ r -> COp -> r -> r, -- LComp
QOp -> [Var] -> r -> r, -- LQuant
- Var -> NExpr -> r -- LArray
+ Var -> [NExpr] -> r, -- LArray
+ Int -> r, -- NConst
+ Var -> r, -- NVar
+ NUnop -> r -> r, -- NUnop
+ r -> NBinop -> r -> r, -- NBinop
+ Var -> [NExpr] -> r -- NArray
)
-- Fold for logical expressions
foldLExpr :: LExprAlgebra r -> LExpr -> r
-foldLExpr (fConst, fVar, fNot, fBinop, fComp, fQuant, fArray) = fold where
+foldLExpr (flConst, flVar, flNot, flBinop, flComp, flQuant, flArray, fnConst, fnVar, fnUnop, fnBinop, fnArray) = fold where
fold e = case e of
- LConst c -> fConst c
- LVar n -> fVar n
- LNot e -> fNot (fold e)
- LBinop a o b -> fBinop (fold a) o (fold b)
- LComp a o b -> fComp a o b
- LQuant o vs e -> fQuant o vs (fold e)
- LArray n e -> fArray n e
\ No newline at end of file
+ LConst c -> flConst c
+ LVar n -> flVar n
+ LNot e -> flNot (fold e)
+ LBinop a o b -> flBinop (fold a) o (fold b)
+ LComp a o b -> flComp (fold a) o (fold b)
+ LQuant o vs e -> flQuant o vs (fold e)
+ LArray n e -> flArray n e
+ NConst n -> fnConst n
+ NVar n -> fnVar n
+ NUnop o e -> fnUnop o (fold e)
+ NBinop a o b -> fnBinop (fold a) o (fold b)
+ NArray n e -> fnArray n e
\ No newline at end of file
diff --git a/src/LogicIR/Frontend/Java.hs b/src/LogicIR/Frontend/Java.hs
index 42c2fc1dd2fab64acb4fdeb955a9fd05c69b7f7a..42b65cced9960a316c7e4a09e3c526a8d9b209f3 100644
--- a/src/LogicIR/Frontend/Java.hs
+++ b/src/LogicIR/Frontend/Java.hs
@@ -1,19 +1,25 @@
module LogicIR.Frontend.Java (javaExpToLExpr) where
import Javawlp.Engine.Folds
+import Javawlp.Engine.HelperFunctions
import Language.Java.Syntax
+import Language.Java.Syntax.Types
import Language.Java.Parser
import Language.Java.Pretty
import LogicIR.Expr
+import Data.Typeable
-javaExpToLExpr :: Exp -> LExpr
+javaExpToLExpr :: Exp -> TypeEnv -> [TypeDecl] -> LExpr
javaExpToLExpr = foldExp javaExpToLExprAlgebra
-javaExpToLExprAlgebra :: ExpAlgebra LExpr
+javaExpToLExprAlgebra :: ExpAlgebra (TypeEnv -> [TypeDecl] -> LExpr)
javaExpToLExprAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQualInstanceCreation, fArrayCreate, fArrayCreateInit, fFieldAccess, fMethodInv, fArrayAccess, fExpName, fPostIncrement, fPostDecrement, fPreIncrement, fPreDecrement, fPrePlus, fPreMinus, fPreBitCompl, fPreNot, fCast, fBinOp, fInstanceOf, fCond, fAssign, fLambda, fMethodRef) where
- fLit = undefined
+ fLit lit _ _ = case lit of
+ Boolean b -> LConst b
+ Int n -> NConst (fromIntegral n) -- TODO: use Integer in LExpr?
+ _ -> error $ show $ lit
fClassLit = undefined
fThis = undefined
fThisClass = undefined
@@ -23,18 +29,54 @@ javaExpToLExprAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation,
fArrayCreateInit = undefined
fFieldAccess = undefined
fMethodInv = undefined
- fArrayAccess = undefined
- fExpName = undefined
+ fArrayAccess arrayIndex env decls = case arrayIndex of -- TODO: better type checking + multiple dimension arrays
+ ArrayIndex (ExpName name) [ExpName index] ->
+ let (arrayType, indexType) = (lookupType decls env name, lookupType decls env index) in
+ case arrayType of
+ (RefType (ArrayType (PrimType IntT))) ->
+ case indexType of
+ PrimType IntT -> NArray (Var (TPrim PInt) (prettyPrint name)) [NVar (Var (TPrim PInt) (prettyPrint index))]
+ _ -> error $ show (arrayIndex, indexType)
+ _ -> error $ show (arrayIndex, arrayType)
+ fExpName name env decls = let symbol = prettyPrint name in let t = lookupType decls env name in
+ -- If we're not dealing with library methods, we should be able to get the type from the type environment
+ case t of
+ PrimType BooleanT -> LVar (Var (TPrim PBool) symbol)
+ PrimType IntT -> NVar (Var (TPrim PInt) symbol)
+ t -> error ("Verifier: Type of " ++ prettyPrint name ++ " unknown or not implemented: " ++ show t)
fPostIncrement = undefined
fPostDecrement = undefined
fPreIncrement = undefined
fPreDecrement = undefined
- fPrePlus = undefined
- fPreMinus = undefined
+ fPrePlus e env decls = e env decls
+ fPreMinus e env decls = NUnop NNeg (e env decls)
fPreBitCompl = undefined
fPreNot = undefined
fCast = undefined
- fBinOp = undefined
+ fBinOp e1 op e2 env decls = let (a, b) = (e1 env decls, e2 env decls) in -- TODO: type checking
+ case op of
+ -- Integer
+ Mult -> NBinop a NMul b
+ Div -> NBinop a NDiv b
+ Rem -> NBinop a NRem b
+ Add -> NBinop a NAdd b
+ Sub -> NBinop a NSub b
+ LShift -> NBinop a NShl b
+ RShift -> NBinop a NShr b
+ RRShift -> undefined
+ And -> NBinop a NAnd b
+ Or -> NBinop a NOr b
+ Xor -> NBinop a NXor b
+ -- Logical
+ CAnd -> LBinop a LAnd b
+ COr -> LBinop a LOr b
+ -- Comparisons
+ LThan -> LComp a CLess b
+ GThan -> LComp a CGreater b
+ LThanE -> LComp a CLeq b
+ GThanE -> LComp a CGeq b
+ Equal -> LComp a CEqual b
+ NotEq -> LComp a CNEqual b
fInstanceOf = undefined
fCond = undefined
fAssign = undefined
diff --git a/src/SimpleFormulaChecker.hs b/src/SimpleFormulaChecker.hs
index 6c899b25371a591e80957df68fe037500d6ad7e3..0c91a8efaf678ecb278b5f706634195873aa153b 100644
--- a/src/SimpleFormulaChecker.hs
+++ b/src/SimpleFormulaChecker.hs
@@ -111,6 +111,7 @@ determineFormulaEq m1@(decls1, mbody1, env1) m2@(decls2, mbody2, env2) name = do
-- get preconditions
let (e1, e2) = (extractCond m1 name, extractCond m2 name)
putStrLn $ "e1:\n" ++ prettyPrint e1 ++ "\n\ne2:\n" ++ prettyPrint e2 ++ "\n"
+ putStrLn $ show $ javaExpToLExpr e1 env1 decls1
{--- get postconditions
let (post1, post2) = (extractCond m1 "post", extractCond m2 "post")
putStrLn $ "post1:\n" ++ prettyPrint post1 ++ "\npost2:\n" ++ prettyPrint post2 ++ "\n"-}
@@ -144,4 +145,6 @@ compareSpec method1 method2 = do
edslSrc = "javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java"
testEq = compareSpec (edslSrc, "swap_spec1") (edslSrc, "swap_spec1")
-testNeq = compareSpec (edslSrc, "swap_spec1") (edslSrc, "swap_spec2")
\ No newline at end of file
+testNeq = compareSpec (edslSrc, "swap_spec1") (edslSrc, "swap_spec2")
+
+blub = compareSpec (edslSrc, "simple1") (edslSrc, "simple1")
\ No newline at end of file
diff --git a/src/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java b/src/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java
index 39279a5e5dcea385a1354e19a0d79be2d1b65cd8..e9f2b96ae5cd1f2ecd9c1f3ce32949b558d32ae2 100644
--- a/src/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java
+++ b/src/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java
@@ -79,6 +79,22 @@ public class Main {
a[j] = temp;
}
+ public static void simple1(int[] a, int i, int j) {
+ pre(i >= 0 && j >= 0);
+ // introducing vars to remember old values
+ int oldai = a[i], oldaj = a[j];
+ swap(a, i, j);
+ post(a[j] == oldai && a[i] == oldaj);
+ }
+
+ public static void simple2(int[] a, int i, int j) {
+ pre(a.length > 0 && i >= 0 && j >= 0);
+ // introducing vars to remember old values
+ int oldai = a[i], oldaj = a[j];
+ swap(a, i, j);
+ post(a[j] == oldai && a[i] == oldaj);
+ }
+
public static void swap_spec1(int[] a, int i, int j) {
pre(a != null);
pre(a.length > 0);