From 80ada9e8137a28ffdf0cc8222a533c513159917a Mon Sep 17 00:00:00 2001
From: Duncan Ogilvie <mr.exodia.tpodt@gmail.com>
Date: Sun, 5 Nov 2017 22:00:20 +0100
Subject: [PATCH] Implement array pretty printing and checking
---
src/ModelParser/Lexer.x | 2 +-
src/SimpleFormulaChecker.hs | 31 +++++++++++++++++++++++++++----
2 files changed, 28 insertions(+), 5 deletions(-)
diff --git a/src/ModelParser/Lexer.x b/src/ModelParser/Lexer.x
index 355f667..0a26bc8 100644
--- a/src/ModelParser/Lexer.x
+++ b/src/ModelParser/Lexer.x
@@ -28,7 +28,7 @@ tokens :-
"false" { \s -> Tbool False }
"#x"$value+ { \s -> Tvalue (parseHex s) }
$num+ { \s -> Tvalue (parseDec s) }
- $ident+ { \s -> Tident s }
+ $ident+ { \s -> Tident s }
{
data Token = Tarrow
diff --git a/src/SimpleFormulaChecker.hs b/src/SimpleFormulaChecker.hs
index 017b946..17dd79a 100644
--- a/src/SimpleFormulaChecker.hs
+++ b/src/SimpleFormulaChecker.hs
@@ -98,9 +98,33 @@ showRelevantModel model = do
prettyModelVal :: (String, ModelVal) -> String
prettyModelVal (k, BoolVal b) = k ++ " = " ++ if b then "true" else "false"
prettyModelVal (k, IntVal n) = k ++ " = " ++ show n
- prettyModelVal (k, ArrayFunc a) = k ++ " = " ++ show n -- TODO: lookup (k ++ "?length") and (k ++ "?null") and handle all cases
- where n = a -- TODO: properly try to convert to a list
- prettyModelVal (k, v) = error $ k ++ " = UNIMPLEMENTED " ++ show v
+ prettyModelVal (k, ArrayFunc a) = k ++ " = " ++ final ++ " " ++ show (aNull, aLength, arrKv, validArr, elseVal)
+ where (BoolVal aNull) = M.findWithDefault (BoolVal False) (k ++ "?null") modelClean
+ (IntVal aLength) = M.findWithDefault (IntVal (-1)) (k ++ "?length") modelClean
+ [InstElse elseVal] = filter (not . isInst) a
+ arrKv = sort (map (\(InstInt k v) -> (k, v)) (filter isInst a))
+ isInst (InstInt _ _) = True
+ isInst _ = False
+ validArr = isValidArray 0 arrKv
+ -- TODO: this does not appear to be correct yet
+ final = if aNull
+ then if (aLength /= -1) || (length arrKv /= 0)
+ then "1: INVALID"
+ else "2: null"
+ else if validArr
+ then if length arrKv == aLength
+ then "3: " ++ show (map snd arrKv)
+ else "4: INVALID"
+ else if aLength /= -1
+ then "5: " ++ show (take aLength (repeat elseVal))
+ else "6: INVALID"
+
+ isValidArray :: Int -> [(Int, Int)] -> Bool
+ isValidArray n [] = False
+ isValidArray n ((i, _) : xs) = if n == i
+ then isValidArray (n + 1) xs
+ else False
+ prettyModelVal (k, v) = error $ k ++ " = UNIMPLEMENTED " ++ show v
-- Remove all occurrences of ArrayRef and ArrayAsConst for easier processing later, also does type casting
modelCleanFunc :: ModelVal -> ModelVal
modelCleanFunc (BoolVal b) = BoolVal b
@@ -137,7 +161,6 @@ showRelevantModel model = do
IntVal _ -> True
_ -> False
-
-- Determine the equality of two method's pre/post conditions.
determineFormulaEq :: MethodDef -> MethodDef -> String -> IO ()
determineFormulaEq m1@(decls1, mbody1, env1) m2@(decls2, mbody2, env2) name = do
--
GitLab