From 02f406cb440e633508a9342e9c8e8c9c24e10a6d Mon Sep 17 00:00:00 2001
From: Orestis Melkonian <melkon.or@gmail.com>
Date: Sat, 9 Dec 2017 20:56:04 +0100
Subject: [PATCH] Basic styling fixes.
---
src/LogicIR/Backend/Null.hs | 2 +-
src/LogicIR/Backend/Pretty.hs | 2 +-
src/LogicIR/Expr.hs | 2 +-
src/LogicIR/Fold.hs | 2 +-
src/LogicIR/Frontend/Java.hs | 10 +++++-----
src/ModelParser/Model.hs | 2 +-
src/SimpleFormulaChecker.hs | 24 +++++++++++-------------
7 files changed, 21 insertions(+), 23 deletions(-)
diff --git a/src/LogicIR/Backend/Null.hs b/src/LogicIR/Backend/Null.hs
index a765ee4..5785100 100644
--- a/src/LogicIR/Backend/Null.hs
+++ b/src/LogicIR/Backend/Null.hs
@@ -14,4 +14,4 @@ lExprPreprocessNull = foldLExpr (LConst, LVar, LUnop, fBinop, LIf, LQuant, LArra
_ -> LBinop a o b
where nullCheck (LVar v@(Var (TArray _) _)) (LConst CNil) = LIsnull v
nullCheck (LConst CNil) (LVar v@(Var (TArray _) _)) = LIsnull v
- nullCheck a b = LBinop a CEqual b
\ No newline at end of file
+ nullCheck a b = LBinop a CEqual b
diff --git a/src/LogicIR/Backend/Pretty.hs b/src/LogicIR/Backend/Pretty.hs
index 2e2aa82..97a3825 100644
--- a/src/LogicIR/Backend/Pretty.hs
+++ b/src/LogicIR/Backend/Pretty.hs
@@ -56,4 +56,4 @@ prettyLExprAlgebra = (fConst, prettyVar, fUnop, fBinop, fIf, fQuant, fArray, fIs
fQuant o v d a = '(' : show o ++ " " ++ prettyVar v ++ ": " ++ d ++ ": " ++ a ++ ")"
fArray v a = prettyVar v ++ "[" ++ a ++ "]"
fIsnull v = "isNull(" ++ prettyVar v ++ ")"
- fLen v = "len(" ++ prettyVar v ++ ")"
\ No newline at end of file
+ fLen v = "len(" ++ prettyVar v ++ ")"
diff --git a/src/LogicIR/Expr.hs b/src/LogicIR/Expr.hs
index d3345db..4cd35e4 100644
--- a/src/LogicIR/Expr.hs
+++ b/src/LogicIR/Expr.hs
@@ -69,4 +69,4 @@ data LExpr = LConst LConst -- constant
| LArray Var LExpr -- array access
| LIsnull Var -- var == null
| LLen Var -- len(array)
- deriving (Show, Eq, Read)
\ No newline at end of file
+ deriving (Show, Eq, Read)
diff --git a/src/LogicIR/Fold.hs b/src/LogicIR/Fold.hs
index a9f4b62..fa236e3 100644
--- a/src/LogicIR/Fold.hs
+++ b/src/LogicIR/Fold.hs
@@ -26,4 +26,4 @@ foldLExpr (fConst, fVar, fUnop, fBinop, fIf, fQuant, fArray, fIsnull, fLen) = fo
LQuant o b d a -> fQuant o b (fold d) (fold a)
LArray v a -> fArray v (fold a)
LIsnull v -> fIsnull v
- LLen v -> fLen v
\ No newline at end of file
+ LLen v -> fLen v
diff --git a/src/LogicIR/Frontend/Java.hs b/src/LogicIR/Frontend/Java.hs
index b760e1d..3e31960 100644
--- a/src/LogicIR/Frontend/Java.hs
+++ b/src/LogicIR/Frontend/Java.hs
@@ -29,7 +29,7 @@ javaExpToLExprAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation,
Boolean b -> LConst (CBool b)
Int n -> LConst (CInt (fromIntegral n))
Null -> LConst CNil
- _ -> error $ show $ lit
+ _ -> error $ show lit
fClassLit = error "fClassLit not supported..."
fThis = error "fThis not supported..."
fThisClass = error "fThisClass not supported..."
@@ -58,7 +58,7 @@ javaExpToLExprAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation,
-> quantr method name rbegin rend bound expr
_
-> error $ "Unimplemented fMethodInv: " ++ show inv
- where quant method name bound expr = let (i) = (Var (TPrim PInt32) bound) in
+ where quant method name bound expr = let i = Var (TPrim PInt32) bound in
let (zero, len) = (LConst (CInt 0), LLen (nameToVar name env decls)) in
case method of
"forall" -> lquantr QAll i zero len expr
@@ -76,7 +76,7 @@ javaExpToLExprAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation,
ArrayIndex (ExpName name) [expr]
-> LArray (nameToVar name env decls) (javaExpToLExpr expr env decls)
_
- -> error $ "Multidimensional arrays are not supported: " ++ show (arrayIndex)
+ -> error $ "Multidimensional arrays are not supported: " ++ show arrayIndex
fExpName name env decls = case name of -- TODO: type checking + check implicit `this.name`
Name [Ident a, Ident "length"] -> LLen $ nameToVar (Name [Ident a]) env decls
_ -> LVar $ nameToVar name env decls
@@ -84,7 +84,7 @@ javaExpToLExprAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation,
fPostDecrement = error "fPostDecrement has side effects..."
fPreIncrement = error "fPreIncrement has side effects..."
fPreDecrement = error "fPreDecrement has side effects..."
- fPrePlus e env decls = e env decls
+ fPrePlus e = e
fPreMinus e env decls = LUnop NNeg (e env decls)
fPreBitCompl e env decls = LUnop NNot (e env decls)
fPreNot e env decls = LUnop LNot (e env decls)
@@ -117,4 +117,4 @@ javaExpToLExprAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation,
fCond c a b env decls = LIf (c env decls) (a env decls) (b env decls)
fAssign = error "fAssign has side effects..."
fLambda = error "fLambda should be handled by fMethodInv..."
- fMethodRef = undefined
\ No newline at end of file
+ fMethodRef = undefined
diff --git a/src/ModelParser/Model.hs b/src/ModelParser/Model.hs
index eabfe43..1a2d512 100644
--- a/src/ModelParser/Model.hs
+++ b/src/ModelParser/Model.hs
@@ -11,4 +11,4 @@ data ModelVal = BoolVal Bool
| ArrayFunc [FuncInst]
deriving (Show, Read, Eq)
-type Z3Model = [(String, ModelVal)]
\ No newline at end of file
+type Z3Model = [(String, ModelVal)]
diff --git a/src/SimpleFormulaChecker.hs b/src/SimpleFormulaChecker.hs
index cfa78d5..9c9ee7f 100644
--- a/src/SimpleFormulaChecker.hs
+++ b/src/SimpleFormulaChecker.hs
@@ -59,7 +59,7 @@ parseMethod (src, name) = do
-- Get a list of all calls to a method of a specific name from a method definition.
getMethodCalls :: MethodDef -> String -> [MethodInvocation]
-getMethodCalls (_, StmtBlock (Block bs), _) name = catMaybes (map extractMethodInv bs)
+getMethodCalls (_, StmtBlock (Block bs), _) name = mapMaybe extractMethodInv bs
where
extractMethodInv :: BlockStmt -> Maybe MethodInvocation
extractMethodInv (BlockStmt (ExpStmt (MethodInv i@(MethodCall (Name [Ident n]) _)))) = if n == name then Just i else Nothing
@@ -69,7 +69,7 @@ getMethodCalls (_, StmtBlock (Block bs), _) name = catMaybes (map extractMethodI
extractExpr :: [MethodInvocation] -> Exp
extractExpr call = combineExprs $ map (\(MethodCall (Name [Ident _]) [a]) -> a) call
where combineExprs :: [Exp] -> Exp
- combineExprs (e:[]) = e
+ combineExprs [e] = e
combineExprs (e:es) = BinOp e CAnd (combineExprs es)
-- Check if two Z3 AST's are equivalent
@@ -95,7 +95,7 @@ showRelevantModel model = do
where modelMap :: M.Map String ModelVal
modelMap = M.fromList model
modelClean :: M.Map String ModelVal
- modelClean = M.filterWithKey (\k _ -> all (\e -> e /= '!') k) $ M.map modelCleanFunc modelMap
+ modelClean = M.filterWithKey (\k _ -> '!' `notElem` k) $ M.map modelCleanFunc modelMap
fromKeys :: [String] -> [(String, ModelVal)]
fromKeys = map (\k -> let v = M.findWithDefault defaultArray k modelClean in (k, v))
defaultArray :: ModelVal
@@ -114,20 +114,18 @@ showRelevantModel model = do
isInst (InstInt _ v) = True
isInst _ = False
isValidArray :: Bool
- isValidArray = length arrKv == 0 || (minIndex >= 0 && maxIndex < aLength)
+ isValidArray = null arrKv || (minIndex >= 0 && maxIndex < aLength)
where minIndex = minimum indices
maxIndex = maximum indices
indices = map fst arrKv
arrMap :: M.Map Int Int
arrMap = M.fromList arrKv
buildArray :: Int -> [Int]
- buildArray i = if aLength == 0 then [] else (M.findWithDefault elseVal i arrMap : if i + 1 == aLength || i + 1 > 100 then [] else buildArray (i + 1))
+ buildArray i = if aLength == 0 then [] else M.findWithDefault elseVal i arrMap : if i + 1 == aLength || i + 1 > 100 then [] else buildArray (i + 1)
final :: String
- final = if aNull
- then "null"
- else if isValidArray
- then show (buildArray 0) ++ if aLength > 100 then " (TRUNCATED, length: " ++ show aLength ++ ")" else "" --let xs = buildArray 0 in if length xs > 100 then show (take 100 xs) ++ " (TRUNCATED)" else show xs
- else "inconsistent array representation" -- blub2
+ final | aNull = "null"
+ | isValidArray = show (buildArray 0) ++ if aLength > 100 then " (TRUNCATED, length: " ++ show aLength ++ ")" else "" --let xs = buildArray 0 in if length xs > 100 then show (take 100 xs) ++ " (TRUNCATED)" else show xs
+ | otherwise = "inconsistent array representation" -- blub2
-- Remove all occurrences of ArrayRef and ArrayAsConst for easier processing later, also does type casting
modelCleanFunc :: ModelVal -> ModelVal
modelCleanFunc (BoolVal b) = BoolVal b
@@ -143,15 +141,15 @@ showRelevantModel model = do
cropInt32 n = fromIntegral (fromIntegral n :: Int32) :: Int
-- Names of the array variables
arrays :: [String]
- arrays = nub $ M.keys (M.filter isArray modelClean) ++ catMaybes (map arrayName (M.keys modelClean))
+ arrays = nub $ M.keys (M.filter isArray modelClean) ++ mapMaybe arrayName (M.keys modelClean)
-- Names of the constant variables
consts :: [String]
consts = filter (\v -> not (isSuffixOf "?length" v || isSuffixOf "?null" v)) $ M.keys (M.filter isConst modelClean)
-- Returns Just "a" for "a?length" and "a?null"
arrayName :: String -> Maybe String
arrayName s
- | isSuffixOf "?length" s = Just $ take (length s - 7) s
- | isSuffixOf "?null" s = Just $ take (length s - 5) s
+ | "?length" `isSuffixOf` s = Just $ take (length s - 7) s
+ | "?null" `isSuffixOf` s = Just $ take (length s - 5) s
| otherwise = Nothing
-- Whether a ModelVal is an array
isArray :: ModelVal -> Bool
--
GitLab