From b2bf15c6814150935883597a1867d8740b0d3177 Mon Sep 17 00:00:00 2001
From: Bart Wijgers <bartwijgers@hotmail.com>
Date: Tue, 24 Sep 2019 13:27:41 +0200
Subject: [PATCH] Calculate program paths
This change allows us to calculate program paths from all programs (as
long as they don't contain any try-catch). Using this, we should be able
to calculate ALL wlps for the programs. However, the checks are not
complete for the whole program, as only program paths up to a certain
length are checked. Any further program paths might say that the program
is (in)correct and give a different result.
---
examples/abs | 6 ++
program-semantics.cabal | 1 +
src/Main.hs | 16 +++-
src/WLP/ProgramPath.hs | 161 ++++++++++++++++++++++++++++++++++++++++
4 files changed, 180 insertions(+), 4 deletions(-)
create mode 100644 examples/abs
create mode 100644 src/WLP/ProgramPath.hs
diff --git a/examples/abs b/examples/abs
new file mode 100644
index 0000000..85e39d7
--- /dev/null
+++ b/examples/abs
@@ -0,0 +1,6 @@
+abs ( x : int | y : int ) {
+ assume x > 0;
+ if x[ 0 ] < 0 then y := 0 else skip ;
+ assert y > 0
+}
+
diff --git a/program-semantics.cabal b/program-semantics.cabal
index 0b5b357..cff4c71 100644
--- a/program-semantics.cabal
+++ b/program-semantics.cabal
@@ -59,6 +59,7 @@ executable program-semantics
, WLP.LogicalExpression
, WLP.MathExpression
, WLP.WLPCalculator
+ , WLP.ProgramPath
-- LANGUAGE extensions used by modules in this package.
-- other-extensions:
diff --git a/src/Main.hs b/src/Main.hs
index 6a4888d..b48bf7a 100644
--- a/src/Main.hs
+++ b/src/Main.hs
@@ -8,6 +8,7 @@ import GCLLexer.Lexer
import System.Environment
import WLP.LogicalExpression
+import WLP.ProgramPath
import WLP.WLPCalculator
main :: IO ()
@@ -15,12 +16,19 @@ main = do
[fp] <- getArgs
file <- readFile fp
let tokens = lexer file
+ putStrLn "Tokens: "
+ putStrLn . show $ tokens
+
let parsed = parseGCL tokens
- putStrLn (show parsed)
case parsed of
- Left xs -> return ()
+ Left xs -> putStrLn "Could not parse program. Error:" >> print xs
Right program -> do
-- We gotta turn the AST into a logical formula based on the wlp
- let wlpFormula = foldProgram programToWLPAlgebra program
- putStrLn . show $ wlpFormula
+ let paths = getProgramPaths maxPathLength program
+
+ putStrLn "Program paths: "
+ sequence_ ((\p -> putStrLn $ show p) <$> paths)
+
+maxPathLength :: Int
+maxPathLength = 20
diff --git a/src/WLP/ProgramPath.hs b/src/WLP/ProgramPath.hs
new file mode 100644
index 0000000..f8e1d29
--- /dev/null
+++ b/src/WLP/ProgramPath.hs
@@ -0,0 +1,161 @@
+module WLP.ProgramPath
+ ( ProgramPath
+ , getProgramPaths
+ , PathLength
+ )
+where
+
+import GCLParser.GCLAlgebra
+import GCLParser.GCLDatatype
+
+-- Program paths and stuff
+-- The program paths are all just a single statement (using Seq), so we use that.
+type ProgramPath = Stmt
+type PathLength = Int
+
+-- | Gets all program paths from the program with the given max path length.
+-- Note that some statements might be expanded to multiple statements, and the
+-- path length is based on the length of the expanded statements. Additionally,
+-- some statements might be removed (like Skip).
+getProgramPaths :: PathLength -> Program -> [ProgramPath]
+getProgramPaths l p = foldProgram programPathAlgebra p l
+
+programPathAlgebra :: ProgramAlgebra PrimitiveType Type VarDeclaration (PathLength -> [ProgramPath]) Expr BinOp (PathLength -> [ProgramPath])
+programPathAlgebra =
+ ( program
+ , variableDeclaration
+ , ( ptInt
+ , ptBool
+ )
+ , ( ptype
+ , reftype
+ , arraytype
+ )
+ , ( skip
+ , assert
+ , assume
+ , assign
+ , aassign
+ , drefassign
+ , seq
+ , ifthenelse
+ , while
+ , block
+ , trycatch
+ )
+ , ( var
+ , liti
+ , litb
+ , litnull
+ , parens
+ , arrayelem
+ , opneg
+ , binopexpr
+ , forall
+ , sizeof
+ , repby
+ , cond
+ , newstore
+ , dereference
+ )
+ , ( and
+ , or
+ , implication
+ , lessthan
+ , lessthanequal
+ , greaterthan
+ , greaterthanequal
+ , equal
+ , minus
+ , plus
+ , multiply
+ , divide
+ , alias
+ )
+ )
+
+ where
+ program s i o stmt = stmt
+ variableDeclaration = VarDeclaration
+ ptInt = PTInt
+ ptBool = PTBool
+ ptype = PType
+ reftype = RefType
+ arraytype = AType
+ skip = \_ -> [Skip] -- Only for the moment, but should be removed later!
+ assert me = \_ -> [Assert me]
+ assume me = \_ -> [Assume me]
+ assign var e = \_ -> [Assign var e]
+ aassign var i v = \_ -> [AAssign var i v]
+ drefassign var v = \_ -> [DrefAssign var v]
+ seq s1 s2 = \l ->
+ let p1 = s1 l
+ p2 = s2 l
+ in filter ((<l) . pathLength) [Seq a b | a <- p1, b <- p2]
+ ifthenelse g s1 s2 = \l -> concat ((\t e -> [Seq (Assume g) t, Seq (Assume (OpNeg g)) e]) <$> s1 l <*> s2 l)
+ while g s = \l -> (unrollWhile g l s)
+ block decls s = \l -> [Block decls] <*> s l
+ trycatch = undefined -- TryCatch - Non-trivial, but optional.
+ var = Var
+ liti = LitI
+ litb = LitB
+ litnull = LitNull
+ parens = Parens
+ arrayelem = ArrayElem
+ opneg = OpNeg
+ binopexpr = BinopExpr
+ forall = Forall
+ sizeof = SizeOf
+ repby = RepBy
+ cond = Cond
+ newstore = NewStore
+ dereference = Dereference
+ and = And
+ or = Or
+ implication = Implication
+ lessthan = LessThan
+ lessthanequal = LessThanEqual
+ greaterthan = GreaterThan
+ greaterthanequal = GreaterThanEqual
+ equal = Equal
+ minus = Minus
+ plus = Plus
+ multiply = Multiply
+ divide = Divide
+ alias = Alias
+
+-- Note that this path should no longer contain ifs and whiles, but should be
+-- the unrolled variants of those statements.
+pathLength :: ProgramPath -> PathLength
+pathLength (Seq s1 s2) = pathLength s1 + pathLength s2
+pathLength _ = 1
+
+-- | Unrolls a while-statement into all possible program paths. The while-loop
+-- is defined by the given expression (the guard expression) and the body. The
+-- list of all program paths is infinite, and therefore the second argument
+-- (`PathLength`) is used to limit the allowed length of the path. The body is
+-- the third argument (`PathLength` -> [`ProgramPath`]). This comes from the type of
+-- the enclosing `programPathAlgebra`.
+-- Returns a [`Stmt`], which is a list of the program paths that can be
+-- traversed within this while-loop.
+unrollWhile :: Expr -> PathLength -> (PathLength -> [ProgramPath]) -> [ProgramPath]
+unrollWhile g ml s = uw' g ml s []
+ where
+ -- This function takes the guard expression, the max path length, and the
+ -- statement, as well as the list of previously found paths, and returns
+ -- the previously found paths prepended by a single iteration of the loop.
+ -- Note that calling this function with no paths returns the path where the
+ -- loop is never entered.
+ uw' g ml s []
+ = let xs = [Seq (Assume (OpNeg g)) Skip] in xs `seq` (xs ++ uw' g ml s xs)
+
+ uw' g ml s prev
+ = let xs = [ Seq (Assume g) (Seq s' p)
+ | s' <- s ml
+ , p <- prev
+ , pathLength p + pathLength s' < ml
+ ]
+ in seq xs $ case xs of
+ [] -> []
+ xs -> (xs ++ uw' g ml s xs)
+
--
GitLab