diff --git a/Main.hs b/Main.hs
index 2ac2abc0299d4a9dd77714d3b79d414fe912057b..665ab8d0907ac8c87de746ed61db1958ed9cc47a 100644
--- a/Main.hs
+++ b/Main.hs
@@ -11,8 +11,8 @@ import HelperFunctions
-testFile = "arrays"
-
+testFile = "objects"
+postCond = "x == 2"
main :: IO ()
@@ -33,7 +33,7 @@ main = do
Left error -> print error
Right compUnit -> do
putStrLn "\r\n-----WLP-----"
- let pred = wlpWithEnv (getDecls compUnit) (getStaticVars compUnit) (getStmt compUnit) postCond
+ let pred = wlpWithEnv (getDecls compUnit) (getStaticVars compUnit) (getStmt compUnit) postCond'
putStrLn . prettyPrint $ pred
putStrLn "\r\n-----Correctness-----"
if unsafeIsTrue pred then putStrLn "WLP evaluates to true" else (if unsafeIsFalse pred then putStrLn "WLP evaluates to false" else putStrLn "undecidable")
@@ -61,7 +61,7 @@ getStaticVars compUnit = concatMap fromTypeDecls (getDecls compUnit) where
fromVarDecl t (VarDecl varId _) = (Name [getId varId], t)
-- The post-condition (for testing)
-postCond :: Exp
-postCond = case parser Language.Java.Parser.exp "x == 2" of
+postCond' :: Exp
+postCond' = case parser Language.Java.Parser.exp postCond 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 865f21952657828047967ddc28d18a2bd7f83bf0..3a47e8bfcdae6a04a79c36587206410a0c2d2c01 100644
--- a/Substitute.hs
+++ b/Substitute.hs
@@ -37,33 +37,31 @@ substVarExpAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQu
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
+ 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)
+ RefType t | lookupType (decls inh) (env inh) (Name [head 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))
+ | 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))
+ | 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)
+ _ -> ExpName (Name name)
fPostIncrement e inh = PostIncrement (e inh)
fPostDecrement e inh = PostDecrement (e inh)
fPreIncrement e inh = PreIncrement (e inh)
@@ -89,9 +87,15 @@ substVarExpAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQu
-- Gets the value from an array
arrayAccess :: Exp -> [Exp] -> Exp
arrayAccess a i = case a of
- ArrayCreate t exps dim -> getInitValue t
+ ArrayCreate t exps dim -> Cond (foldr (\(i, l) e -> e &* (BinOp i LThan l)) true (zip i exps)) (getInitValue t) (MethodInv (MethodCall (Name [Ident "ArrayIndexOutOfBoundsException"]) [])) -- Throw an exception if not within range, otherwise return the init value of the element
ArrayCreateInit t dim arrayInit -> getInitValue t
_ -> ArrayAccess (ArrayIndex a i)
+
+ -- for arguments xs and ys, gets all combinations of non-empty prefixes xs' of xs and ys' of ys
+ getCombs :: [a] -> [a] -> [([a], [a])]
+ getCombs xs ys = [(x, y) | x <- xs', y <- ys'] where
+ xs' = drop 1 (inits xs)
+ ys' = drop 1 (inits ys)
-- | 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
diff --git a/Tests/objects.java b/Tests/objects.java
index be26569a241cc50cc891a8e869a9b4486a1d6415..574c8467f2fa58d5691ea7e88168158558c04373 100644
--- a/Tests/objects.java
+++ b/Tests/objects.java
@@ -1,21 +1,25 @@
public class HelloWorld
{
static int c;
- static Circle circle1, circle2;
+ static Chain chain1, chain2;
public static void main(String[] args)
{
float x = 1;
+ Circle circle1, circle2;
circle1 = new Circle(0, 0);
circle2 = new Circle(0, 0);
- circle1 = circle2;
- circle1.center = 2;
- x = circle1.center;
+ chain1 = new Chain();
+ chain1.tail = chain2;
+ chain1.circle = circle1;
+ chain2.circle = circle2;
+ circle2.center = 2;
+
+ x = chain1.tail.circle.center;
}
- private static void someOtherFunction()
+ private static void someFunction()
{
- // increase c, because why not?
c = c + 1;
}
}
@@ -23,7 +27,7 @@ public class HelloWorld
// The circle class
public class Circle
{
- float center, radius;
+ public float center, radius;
public Circle(float center, float radius)
{
@@ -31,3 +35,11 @@ public class Circle
this.radius = radius;
}
}
+
+// A chain of circles
+public class Chain
+{
+ public Circle circle;
+ public Chain tail;
+}
+
diff --git a/WLP.hs b/WLP.hs
index d69006dbf968416af6c85af90e2c4c7fa13067a5..953502fd0f6efe93e214a1bd70573e3c796729bb 100644
--- a/WLP.hs
+++ b/WLP.hs
@@ -80,7 +80,10 @@ wlpStmtAlgebra = (fStmtBlock, fIfThen, fIfThenElse, fWhile, fBasicFor, fEnhanced
-- wlp of a var declaration that also assigns a value. Declaring without assignment assigns the default value
wlpDeclAssignment :: Type -> Inh -> VarDecl -> Exp -> Exp
- wlpDeclAssignment t inh (VarDecl (VarId ident) Nothing) = substVar (env inh) (decls inh) (NameLhs (Name [ident])) (getInitValue t) . acc inh
+ wlpDeclAssignment t inh (VarDecl (VarId ident) Nothing) = case t of
+ PrimType _ -> substVar (env inh) (decls inh) (NameLhs (Name [ident])) (getInitValue t) . acc inh
+ -- We don't initialize ref types to null, because we want to keep pointer information
+ RefType _ -> acc inh
wlpDeclAssignment t inh (VarDecl (VarId ident) (Just (InitExp e))) = substVar (env inh) (decls inh) (NameLhs (Name [ident])) e . acc inh
inv = true -- for simplicity, "True" is used as an invariant for now