Skip to content
Snippets Groups Projects
Commit 2834589f authored by koen's avatar koen
Browse files

verification for objects and arrays added and a bunch of bugs fixed

parent 4f03bd7e
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Main.hs
+ 4
− 2
View file @ 2834589f
......@@ -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
Substitute.hs
+ 58
− 25
View file @ 2834589f
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
Tests/arrays.java 0 → 100644
+ 10
− 0
View file @ 2834589f
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
Tests/objects.java
+ 4
− 4
View file @ 2834589f
......@@ -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;
}
......
Verifier.hs
+ 11
− 5
View file @ 2834589f
......@@ -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
......
WLP.hs
+ 2
− 2
View file @ 2834589f
......@@ -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))
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment