From 2834589fb72695510b48d3b6e3b7c6bbeda6c642 Mon Sep 17 00:00:00 2001
From: koen <koenwermer@gmail.com>
Date: Sun, 13 Nov 2016 21:12:20 +0100
Subject: [PATCH] verification for objects and arrays added and a bunch of bugs
fixed
---
Main.hs | 6 ++--
Substitute.hs | 83 ++++++++++++++++++++++++++++++++--------------
Tests/arrays.java | 10 ++++++
Tests/objects.java | 8 ++---
Verifier.hs | 16 ++++++---
WLP.hs | 4 +--
6 files changed, 89 insertions(+), 38 deletions(-)
create mode 100644 Tests/arrays.java
diff --git a/Main.hs b/Main.hs
index 0731c73..2ac2abc 100644
--- a/Main.hs
+++ b/Main.hs
@@ -11,7 +11,7 @@ import HelperFunctions
-testFile = "objects"
+testFile = "arrays"
@@ -62,4 +62,6 @@ getStaticVars compUnit = concatMap fromTypeDecls (getDecls compUnit) where
-- The post-condition (for testing)
postCond :: Exp
-postCond = BinOp (ExpName (Name [Ident "x"])) Equal (Lit (Float 2))
\ No newline at end of file
+postCond = case parser Language.Java.Parser.exp "x == 2" of
+ Right e -> e
+ _ -> error "syntax error in post-condition"
\ No newline at end of file
diff --git a/Substitute.hs b/Substitute.hs
index 473b078..865f219 100644
--- a/Substitute.hs
+++ b/Substitute.hs
@@ -1,13 +1,21 @@
-module Substitute where
+module Substitute (substVar, desugarAssign) where
import Language.Java.Syntax
import Data.List
import Folds
import HelperFunctions
-
-substVarExpAlgebra :: ExpAlgebra ((Lhs, Exp, TypeEnv, [TypeDecl]) -> Exp)
+
+-- | A type for the inherited attribute
+data SubstInh = SubstInh { lhs :: Lhs, -- Left hand side of the assignment
+ rhs :: Exp, -- Right hand side
+ env :: TypeEnv,
+ decls :: [TypeDecl], -- Class declarations
+ arrayLookup :: Bool -- true iff the current expression is an array that we're trying to access
+ }
+
+substVarExpAlgebra :: ExpAlgebra (SubstInh -> Exp)
substVarExpAlgebra = (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 lit _ = Lit lit
fClassLit mt _ = ClassLit mt
@@ -17,33 +25,45 @@ substVarExpAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQu
fQualInstanceCreation e typeArgs ident args mBody inh = QualInstanceCreation (e inh) typeArgs ident args mBody
fArrayCreate t exps dim inh = ArrayCreate t (map ($ inh) exps) dim
fArrayCreateInit t dim arrayInit _ = ArrayCreateInit t dim arrayInit
- fFieldAccess fieldAccess (lhs, rhs, env, decls) = case lhs of
+ fFieldAccess fieldAccess inh = case lhs inh of
FieldLhs fieldAccess' -> case fieldAccess of
PrimaryFieldAccess e ident -> error "todo: fieldAccess substitution"
SuperFieldAccess ident -> error "todo: fieldAccess substitution"
ClassFieldAccess name ident -> error "todo: fieldAccess substitution"
_ -> FieldAccess fieldAccess
fMethodInv invocation _ = MethodInv invocation
- fArrayAccess (ArrayIndex a i) (lhs, rhs, env, decls) = let a' = substVar env decls lhs rhs a
- i' = map (substVar env decls lhs rhs) i in
- case lhs of
- ArrayLhs (ArrayIndex a'' i'') -> Cond (foldr (\(i1, i2) e -> e &* (i1 ==* i2)) (a' ==* a'') (zip i' i'')) rhs (ArrayAccess (ArrayIndex a' i'))
- _ -> ArrayAccess (ArrayIndex a' i')
- fExpName (Name name) (lhs, rhs, env, decls) = case lhs of
- NameLhs (Name name') -> case lookupType decls env (Name name') of
- PrimType _ | name' == name -> rhs
- | otherwise -> ExpName (Name name)
- RefType t -> let getFields e [] = e
- getFields e (f : fs) = getFields (FieldAccess (PrimaryFieldAccess e f)) fs
- in if [head name] == name' then getFields rhs (tail name) else Cond (ExpName (Name [head name]) ==* ExpName (Name name')) (getFields rhs (tail name)) (ExpName (Name name))
-
-
-
- -- | name' == name -> rhs
- -- | isPrefixOf name' name -> let getFields e [f] = FieldAccess (PrimaryFieldAccess e f)
- -- getFields e (f : fs) = getFields (FieldAccess (PrimaryFieldAccess e f)) fs
- -- in getFields rhs (drop (length name') name)
- -- | otherwise -> Cond (ExpName (Name [head name]) ==* ExpName (Name [head name'])) rhs (ExpName (Name name))
+ fArrayAccess (ArrayIndex a i) inh = let a' = foldExp substVarExpAlgebra a (inh {arrayLookup = True})
+ i' = map (flip (foldExp substVarExpAlgebra) inh) i in
+ case lhs inh of
+ ArrayLhs (ArrayIndex a'' i'') -> Cond (foldr (\(i1, i2) e -> e &* (i1 ==* i2)) (a' ==* a'') (zip i' i'')) (rhs inh) (arrayAccess a' i')
+ _ -> arrayAccess a' i'
+ fExpName (Name name) inh = case lhs inh of
+ NameLhs (Name lhsName) -> case lookupType (decls inh) (env inh) (Name [head lhsName]) of
+ PrimType _ | lhsName == name -> rhs inh
+ | otherwise -> ExpName (Name name)
+ RefType t -> case rhs inh of
+ ExpName (Name rhsName) | take (length lhsName) name == lhsName -> ExpName (Name (rhsName ++ drop (length lhsName) name))
+ -- accessing o1.x might affect o2.x if o1 and o2 point to the same object:
+ | name == head name : tail lhsName && length name > 1 -> Cond (ExpName (Name [head name]) ==* ExpName (Name [head lhsName])) (rhs inh) (ExpName (Name name))
+ -- the assignment doesn't affect this expression:
+ | otherwise -> ExpName (Name name)
+
+ -- we substitute instance creation only if we access a field, to not lose pointer information
+ -- example: {x = new obj} doesn't affect {x = y} but it does affect {x.a = y.a}
+ InstanceCreation _ _ _ _ | length lhsName < length name && take (length lhsName) name == lhsName -> getFields (decls inh) (rhs inh) (drop (length lhsName) name)
+ | length lhsName < length name && take (length lhsName) name == head name : tail lhsName -> Cond (ExpName (Name [head name]) ==* ExpName (Name [head lhsName])) (getFields (decls inh) (rhs inh) (drop (length lhsName) name)) (ExpName (Name name))
+ -- the assignment doesn't affect this expression:
+ | otherwise -> ExpName (Name name)
+
+ -- the same idea for arrays
+ ArrayCreate _ _ _ | not $ arrayLookup inh -> ExpName (Name name)
+ ArrayCreateInit _ _ _ | not $ arrayLookup inh -> ExpName (Name name)
+
+ _ | take (length lhsName) name == lhsName -> getFields (decls inh) (rhs inh) (drop (length lhsName) name)
+ | name == head name : tail lhsName -> Cond (ExpName (Name [head name]) ==* ExpName (Name [head lhsName])) (rhs inh) (ExpName (Name name))
+ -- the assignment doesn't affect this expression:
+ | otherwise -> ExpName (Name name)
+ _ -> ExpName (Name name)
fPostIncrement e inh = PostIncrement (e inh)
fPostDecrement e inh = PostDecrement (e inh)
fPreIncrement e inh = PreIncrement (e inh)
@@ -59,6 +79,19 @@ substVarExpAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQu
fAssign lhs assOp e inh = Assign lhs assOp (e inh)
fLambda lParams lExp _ = Lambda lParams lExp
fMethodRef className methodName _ = MethodRef className methodName
+
+ -- Recursively accesses a field of an expression
+ getFields :: [TypeDecl] -> Exp -> [Ident] -> Exp
+ getFields decls e [] = e
+ getFields decls (InstanceCreation _ t _ _) (f:fs) = getFields decls (getInitValue (getFieldType decls (RefType (ClassRefType t)) (Name [f]))) fs
+ getFields decls e (f : fs) = getFields decls (FieldAccess (PrimaryFieldAccess e f)) fs
+
+ -- Gets the value from an array
+ arrayAccess :: Exp -> [Exp] -> Exp
+ arrayAccess a i = case a of
+ ArrayCreate t exps dim -> getInitValue t
+ ArrayCreateInit t dim arrayInit -> getInitValue t
+ _ -> ArrayAccess (ArrayIndex a i)
-- | Desugars to a basic assignment, returning the new righ hand side. For example: desugaring x += 3 returns the new rhs x + 3
desugarAssign :: Lhs -> AssignOp -> Exp -> Exp
@@ -82,4 +115,4 @@ desugarAssign lhs op e = case op of
-- | Substitutes all occurences of a specific free variable by an expression
substVar :: TypeEnv -> [TypeDecl] -> Lhs -> Exp -> Exp -> Exp
-substVar env decls lhs rhs e = foldExp substVarExpAlgebra e (lhs, rhs, env, decls)
\ No newline at end of file
+substVar env decls lhs rhs e = foldExp substVarExpAlgebra e (SubstInh lhs rhs env decls False)
\ No newline at end of file
diff --git a/Tests/arrays.java b/Tests/arrays.java
new file mode 100644
index 0000000..2924eef
--- /dev/null
+++ b/Tests/arrays.java
@@ -0,0 +1,10 @@
+public class Arrays
+{
+ public static void main(String[] args)
+ {
+ int x;
+ int[] a = new int[12];
+ a[5] = 2;
+ x = a[5];
+ }
+}
\ No newline at end of file
diff --git a/Tests/objects.java b/Tests/objects.java
index ecd594b..be26569 100644
--- a/Tests/objects.java
+++ b/Tests/objects.java
@@ -6,10 +6,10 @@ public class HelloWorld
public static void main(String[] args)
{
float x = 1;
- circle1 = new Circle(2, 2);
- circle2 = new Circle(2, 2);
- circle2 = circle1;
- circle2.center = 3;
+ circle1 = new Circle(0, 0);
+ circle2 = new Circle(0, 0);
+ circle1 = circle2;
+ circle1.center = 2;
x = circle1.center;
}
diff --git a/Verifier.hs b/Verifier.hs
index ed5aa98..5d5c575 100644
--- a/Verifier.hs
+++ b/Verifier.hs
@@ -65,14 +65,19 @@ expAssertAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQual
fClassLit = undefined
fThis = undefined
fThisClass = undefined
- fInstanceCreation _ _ _ _ = mkInteger 2-- TODO
+ fInstanceCreation = undefined
fQualInstanceCreation = undefined
fArrayCreate = undefined
fArrayCreateInit = undefined
- fFieldAccess fieldAccess = mkInteger 2-- TODO
+ fFieldAccess fieldAccess = case fieldAccess of
+ 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 = undefined
- fArrayAccess _ = mkInteger 2-- TODO
- fExpName name = mkStringSymbol (prettyPrint name) >>= mkIntVar
+ fArrayAccess _ = undefined
+ fExpName name = stringToBv (prettyPrint name)
fPostIncrement = undefined
fPostDecrement = undefined
fPreIncrement = undefined
@@ -168,8 +173,9 @@ expAssertAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQual
astg <- g
assert astg
result <- check
+ solverReset
case result of
- Sat -> e1
+ Sat -> e1
Unsat -> e2
_ -> error "can't evaluate if-condition"
fAssign = undefined
diff --git a/WLP.hs b/WLP.hs
index 0344abf..d69006d 100644
--- a/WLP.hs
+++ b/WLP.hs
@@ -133,12 +133,12 @@ wlpExpAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQualIns
fClassLit = undefined
fThis = undefined
fThisClass = undefined
- fInstanceCreation typeArgs t args mBody inh = (InstanceCreation typeArgs t args mBody, (acc inh, env inh)) --let p = getIncrPointer heapPointer in (ExpName (Name [Ident (show p)]), (substVar (env inh) (decls inh) (ArrayLhs (ArrayIndex heap [Lit (Int p)])) (makeObjectArray (decls inh) t args mBody) . acc inh, env inh)) -- TODO: assign default values to fields. basically the WLP of: heap[p] = new object[#fields]
+ fInstanceCreation typeArgs t args mBody inh = (InstanceCreation typeArgs t args mBody, (acc inh, env inh))
fQualInstanceCreation e typeArgs t args mBody inh = (QualInstanceCreation (getExp e inh) typeArgs t args mBody, (getTrans e inh, env inh))
fArrayCreate t dimLengths dim inh = (ArrayCreate t (map (flip getExp inh) dimLengths) dim, (acc inh, env inh))
fArrayCreateInit t dim init inh = (ArrayCreateInit t dim init, (acc inh, env inh))
fFieldAccess fieldAccess inh = case fieldAccess of
- PrimaryFieldAccess e (Ident field) -> (ArrayAccess (ArrayIndex (getExp (foldExp wlpExpAlgebra e) inh) [Lit (String field)]), (acc inh, env inh)) -- Objects are modelled as arrays
+ PrimaryFieldAccess e (Ident field) -> (ArrayAccess (ArrayIndex (getExp (foldExp wlpExpAlgebra e) inh) [Lit (String field)]), (acc inh, env inh))
_ -> error "fieldaccess"
fMethodInv = error "method call"
fArrayAccess arrayIndex inh = (ArrayAccess arrayIndex, (acc inh, env inh))
--
GitLab