From 173f0d0293d780fb8309d298fcfa678996243d62 Mon Sep 17 00:00:00 2001
From: koen <koenwermer@gmail.com>
Date: Fri, 2 Dec 2016 15:29:13 +0100
Subject: [PATCH] unrolling loops a finite amount of times (instead of using
invariants)
---
Settings.hs | 9 ++++++---
Tests/loops.java | 2 +-
WLP.hs | 12 ++++++------
3 files changed, 13 insertions(+), 10 deletions(-)
diff --git a/Settings.hs b/Settings.hs
index 00d654e..c8ba2e8 100644
--- a/Settings.hs
+++ b/Settings.hs
@@ -1,5 +1,8 @@
module Settings where
-testFile = "arrays"
-postCond = "a == b"
-invariant = "i <= 5"
\ No newline at end of file
+testFile, postCond :: String
+testFile = "loops"
+postCond = "x == 5"
+
+nrOfUnroll :: Int
+nrOfUnroll = 6
\ No newline at end of file
diff --git a/Tests/loops.java b/Tests/loops.java
index 1784c1d..4072c3e 100644
--- a/Tests/loops.java
+++ b/Tests/loops.java
@@ -7,7 +7,7 @@ public class C1
int i = 0;
- while(i < 5)
+ while(i < 6)
{
i++;
diff --git a/WLP.hs b/WLP.hs
index ecd505d..ab0cc72 100644
--- a/WLP.hs
+++ b/WLP.hs
@@ -37,7 +37,7 @@ wlpStmtAlgebra = (fStmtBlock, fIfThen, fIfThenElse, fWhile, fBasicFor, fEnhanced
fIfThenElse e s1 s2 inh = let e' = getExp (foldExp wlpExpAlgebra e) inh
in ((\q -> (e' &* fst (s1 inh) q) |* (neg e' &* fst (s2 inh) q)) . acc inh, env inh)
fWhile e s inh = let e' = getExp (foldExp wlpExpAlgebra e) inh
- in ((\q -> if unsafeIsTrue (((inv &* neg e') `imp` q) &* ((inv &* e') `imp` fst (s inh) inv) &* ((inv &* e') `imp` fst (s inh {br = const q}) true)) then inv else (neg e' &* q)) . acc inh, env inh)
+ in ((\q -> unrollLoop nrOfUnroll e' (fst (s (inh {br = const q}))) q) . acc inh, env inh)
fBasicFor init me incr s inh = let loop = fst (fWhile (fromMaybeGuard me) (\inh' -> s (inh {acc = fst (wlp' inh' (incrToStmt incr))})) inh) in wlp' (inh {acc = loop}) (initToStmt init)
fEnhancedFor = error "EnhancedFor"
fEmpty inh = (acc inh, env inh) -- Empty does nothing, but still passes control to the next statement
@@ -82,11 +82,11 @@ wlpStmtAlgebra = (fStmtBlock, fIfThen, fIfThenElse, fWhile, fBasicFor, fEnhanced
-- 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
- inv = case parser Language.Java.Parser.exp invariant of
- Right e -> e
- _ -> error "syntax error in invariant"
+
+ -- Unrolls a while-loop a finite amount of times
+ unrollLoop :: Int -> Exp -> (Exp -> Exp) -> Exp -> Exp
+ unrollLoop 0 g _ q = neg g `imp` q
+ unrollLoop n g body q = (neg g `imp` q) &* (g `imp` body (unrollLoop (n - 1) g body q))
-- Converts initialization code of a for loop to a statement
--
GitLab