diff --git a/examples/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java b/examples/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java
index 061e8924065a7830032d00bd69035d4a4933b15c..3a8bb1597a4b44295dded23881bc1fab4b9c5f24 100644
--- a/examples/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java
+++ b/examples/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java
@@ -29,13 +29,13 @@ public class Main {
pre(~(a * 2) == (79 & 40)); // can't evaluate due to undefined variable
}
- public static float float1(float a) {
- pre(a >= 2);
+ public static float real1(float a) {
+ pre(a >= (2 - 1 + 1));
a += a;
- post(a >= 4);
+ post(a >= (4 - 3 + 3));
}
- public static float float2(float a) {
+ public static float real2(float a) {
pre(a > 2 || a == 2);
a = a * 2;
post(a > 4 || a == 4);
diff --git a/src/LogicIR/Backend/Pretty.hs b/src/LogicIR/Backend/Pretty.hs
index 4af16c1d5a43ec251dfab5521830e8db84aa88b4..6d6ef055957b6e1f90c53506d682cf96a6d1af12 100644
--- a/src/LogicIR/Backend/Pretty.hs
+++ b/src/LogicIR/Backend/Pretty.hs
@@ -13,8 +13,8 @@ prettyLExpr = foldLExpr prettyLExprAlgebra
prettyType :: Type -> String
prettyType (TPrim PInt32) = "int"
prettyType (TPrim PBool) = "bool"
-prettyType (TPrim PFloat) = "float"
-prettyType (TArray t) = prettyType t ++ "[]"
+prettyType (TPrim PReal) = "real"
+prettyType (TArray t) = "[" ++ prettyType t ++ "]"
prettyLBinop :: LBinop -> String
prettyLBinop op =
@@ -51,6 +51,7 @@ prettyLExprAlgebra = (fConst, prettyVar, fUnop, fBinop, fIf, fQuant, fArray, fIs
fConst c = case c of
CBool b -> if b then "true" else "false"
CInt n -> show n
+ CReal n -> show n
CNil -> "nil"
fUnop o a = prettyNUnop o ++ a
fBinop a o b = "(" ++ a ++ " " ++ prettyLBinop o ++ " " ++ b ++ ")"
diff --git a/src/LogicIR/Backend/Z3.hs b/src/LogicIR/Backend/Z3.hs
index 6b1977f433895ee67b0be4d2aef935e7a2156143..366cdcd1afdf38a6e6c32a106d0b035a9670da50 100644
--- a/src/LogicIR/Backend/Z3.hs
+++ b/src/LogicIR/Backend/Z3.hs
@@ -2,6 +2,7 @@
module LogicIR.Backend.Z3 (lExprToZ3Ast) where
import Z3.Monad
+import Control.Monad.Trans (liftIO)
import LogicIR.Expr
import LogicIR.Fold
@@ -10,55 +11,61 @@ import LogicIR.Parser
lExprToZ3Ast :: LExpr -> Z3 AST
lExprToZ3Ast = foldLExpr lExprToZ3AstAlgebra
+getSorts :: AST -> AST -> Z3 (String, String)
+getSorts a b = do
+ as <- getSort a
+ bs <- getSort b
+ return (show as, show bs)
+
-- TODO: support more types
lExprToZ3AstAlgebra :: LExprAlgebra (Z3 AST)
lExprToZ3AstAlgebra = (fConst, fVar, fUnop, fBinop, fIf, fQuant, fArray, fIsnull, fLen) where
fConst c = case c of
CBool b -> mkBool b
- CInt n -> mkBitvector 32 (fromIntegral n)
- CFloat f -> mkRealNum f
+ CInt n -> mkInteger $toInteger n
+ CReal f -> mkRealNum f
CNil -> error "null constants cannot be used directly with Z3 (use LogicIR.Backend.Null)"
fVar (Var t n) = do
symbol <- mkStringSymbol n
case t of
- "int" -> mkBvVar symbol 32
+ "int" -> mkIntVar symbol
"bool" -> mkBoolVar symbol
- "float" -> mkRealVar symbol
+ "real" -> mkRealVar symbol
"[int]" -> do
- intSort <- mkBvSort 32
+ intSort <- mkIntSort
arraySort <- mkArraySort intSort intSort
mkVar symbol arraySort
"[bool]" -> do
- intSort <- mkBvSort 32
+ intSort <- mkIntSort
arraySort <- mkBoolSort >>= mkArraySort intSort
mkVar symbol arraySort
_ -> error $ "unsupported type: " ++ show n
fUnop o a' = do
a <- a'
case o of
- NNeg -> mkBvneg a
- NNot -> mkBvnot a
+ NNeg -> mkUnaryMinus a
+ NNot -> mkBvnot a --
LNot -> mkNot a
fBinop a' o b' = do
a <- a'
b <- b'
case o of
- NAdd -> mkBvadd a b
- NSub -> mkBvsub a b
- NMul -> mkBvmul a b
- NDiv -> mkBvsdiv a b -- NOTE: signed division
- NRem -> mkBvsrem a b -- TODO: check if the correct remainder is taken
- NShl -> mkBvshl a b
+ NAdd -> mkAdd [a, b]
+ NSub -> mkSub [a, b]
+ NMul -> mkMul [a, b]
+ NDiv -> mkDiv a b -- NOTE: signed division
+ NRem -> mkRem a b -- TODO: check if the correct remainder is taken
+ NShl -> mkBvshl a b --
NShr -> mkBvashr a b -- NOTE: signed shift right will keep the sign
- NAnd -> mkBvand a b
- NOr -> mkBvor a b
- NXor -> mkBvxor a b
+ NAnd -> mkBvand a b --
+ NOr -> mkBvor a b --
+ NXor -> mkBvxor a b --
LAnd -> mkAnd [a, b]
LOr -> mkOr [a, b]
LImpl -> mkImplies a b
CEqual -> mkEq a b
- CLess -> mkBvslt a b
- CGreater -> mkBvsgt a b
+ CLess -> mkLt a b
+ CGreater -> mkGt a b
fIf c' a' b' = do
c <- c'
a <- a'
@@ -81,4 +88,4 @@ lExprToZ3AstAlgebra = (fConst, fVar, fUnop, fBinop, fIf, fQuant, fArray, fIsnull
a <- a'
mkSelect v a
fIsnull (Var (TArray _) n) = mkStringSymbol (n ++ "?null") >>= mkBoolVar
- fLen (Var (TArray _) n) = mkStringSymbol (n ++ "?length") >>= flip mkBvVar 32 -- TODO: support proper array lengths
+ fLen (Var (TArray _) n) = mkStringSymbol (n ++ "?length") >>= mkIntVar -- TODO: support proper array lengths
diff --git a/src/LogicIR/Expr.hs b/src/LogicIR/Expr.hs
index e9160a54d2717eab97d6204506350845e49aa394..ddcae70f7fd733ab919141b47448239e0d128455 100644
--- a/src/LogicIR/Expr.hs
+++ b/src/LogicIR/Expr.hs
@@ -5,7 +5,7 @@ import Data.String
-- | The primitive types are bool and int32.
data Primitive = PBool
| PInt32
- | PFloat
+ | PReal
deriving (Show, Eq, Read)
-- | A Type can either be a primitive or an array type.
@@ -31,6 +31,7 @@ data LBinop =
| NMul -- a * b
| NDiv -- a / b
| NRem -- a % b
+ -- bit-wise operators
| NShl -- a >> b
| NShr -- a << b
| NAnd -- a & b
@@ -53,7 +54,7 @@ data QOp = QAll | QAny
-- | Constants.
data LConst = CBool Bool
| CInt Int
- | CFloat Float
+ | CReal Double
| CNil
deriving (Show, Eq, Read)
@@ -78,6 +79,7 @@ forall = LQuant QAll
exists = LQuant QAny
var x t = Var t x
v = LVar
+r = LConst . CReal
n = LConst . CInt
b = LConst . CBool
nil = LConst CNil
diff --git a/src/LogicIR/Frontend/Java.hs b/src/LogicIR/Frontend/Java.hs
index 4debba0c60f49e05c958cac4cc6c5deabaaca69d..b15375c543e741caae3131f71f6dd1bb3d945850 100644
--- a/src/LogicIR/Frontend/Java.hs
+++ b/src/LogicIR/Frontend/Java.hs
@@ -21,10 +21,17 @@ javaExpToLExpr = foldExp javaExpToLExprAlgebra
nameToVar :: Name -> TypeEnv -> [TypeDecl] -> Var
nameToVar name env decls =
case arrayType of
- PrimType BooleanT -> fromString(symbol ++ ":bool")
- PrimType IntT -> fromString(symbol ++ ":int")
- PrimType FloatT -> fromString(symbol ++ ":float")
- RefType (ArrayType (PrimType IntT)) -> fromString(symbol ++ ":[int]")
+ PrimType BooleanT -> fromString(symbol ++ ":bool")
+ PrimType ShortT -> fromString(symbol ++ ":int")
+ PrimType IntT -> fromString(symbol ++ ":int")
+ PrimType LongT -> fromString(symbol ++ ":int")
+ PrimType FloatT -> fromString(symbol ++ ":real")
+ PrimType DoubleT -> fromString(symbol ++ ":real")
+ RefType (ArrayType (PrimType ShortT)) -> fromString(symbol ++ ":[int]")
+ RefType (ArrayType (PrimType IntT)) -> fromString(symbol ++ ":[int]")
+ RefType (ArrayType (PrimType LongT)) -> fromString(symbol ++ ":[int]")
+ RefType (ArrayType (PrimType FloatT)) -> fromString(symbol ++ ":[real]")
+ RefType (ArrayType (PrimType DoubleT)) -> fromString(symbol ++ ":[real]")
_ -> error $ "Unimplemented nameToVar: " ++ show (name, arrayType)
where
(arrayType, symbol) = (lookupType decls env name, prettyPrint name)
@@ -40,6 +47,8 @@ javaExpToLExprAlgebra =
case lit of
Boolean t -> b t
Int i -> n $ fromInteger i
+ Float i -> r i
+ Double i -> r i
Null -> "null"
_ -> error $ "Unsupported type: " ++ show lit
fClassLit = error "fClassLit not supported..."
diff --git a/src/LogicIR/Parser.hs b/src/LogicIR/Parser.hs
index ce5c222b0211f94982772ebb109885a5b385c30c..41d9fd3966659e472d6826c8e2be3f3c8b130c3f 100644
--- a/src/LogicIR/Parser.hs
+++ b/src/LogicIR/Parser.hs
@@ -77,10 +77,15 @@ iteP = do
e' <- exprP
return $ LIf g e e'
varP = LVar <$> bvarP
-constP = LConst <$> ((CBool <$> boolP) <|> (CInt <$> numP) <|> (CNil <$ nilP))
+constP = LConst <$> ((CBool <$> boolP)
+ <|> (CInt <$> numP)
+ <|> (CReal <$> realP)
+ <|> (CNil <$ nilP)
+ )
where
boolP = (True <$ str "true") <|> (False <$ str "false")
numP = lexeme $ fmap fromInteger (Tokens.integer haskell)
+ realP = lexeme $ Tokens.float haskell
nilP = str "null"
bvarP :: Parser Var
@@ -94,7 +99,7 @@ typeP = try (TPrim <$> primTypeP) <|> (TArray <$> arrayTypeP)
where
primTypeP = lexeme (PBool <$ str "bool")
<|> (PInt32 <$ str "int")
- <|> (PFloat <$ str "float")
+ <|> (PReal <$ str "real")
arrayTypeP = "[" ~> typeP <~ "]"
-- | Useful marcros.
diff --git a/src/ModelParser/Lexer.x b/src/ModelParser/Lexer.x
index 0a26bc804180013b3b3a5306b3ae0ef2b76cff3f..acd23baf36fd62a4caa6430ef69a396d752acebb 100644
--- a/src/ModelParser/Lexer.x
+++ b/src/ModelParser/Lexer.x
@@ -3,13 +3,13 @@ module ModelParser.Lexer where
import Numeric
}
-
+
%wrapper "basic"
-
+
$ident = [0-9a-zA-Z!\._\?]
$num = [0-9]
$value = [0-9a-f]
-
+
tokens :-
$white+ ;
"->" { \s -> Tarrow }
@@ -61,4 +61,4 @@ model2 = "a.length -> #x00000001\na.null -> true\ni!0 -> #x00000000\na -> (_ as-
model3 = "a.length -> #x00000003\ni!0 -> #x00000001\na -> (_ as-array k!1)\nk!1 -> {\n #x00000002 -> #x00000001\n #x00000001 -> #x00000000\n else -> #x00000001\n}"
model4 = "a.null -> false\nj -> #x00000010\na -> ((as const (Array (_ BitVec 32) (_ BitVec 32))) #xffffffff)\ni -> #x00000000\na.length -> #x00000001"
-}
\ No newline at end of file
+}
diff --git a/src/SimpleFormulaChecker.hs b/src/SimpleFormulaChecker.hs
index c7a02d24eba3de759493a46c1088b48b21a7f6d4..8d35c9cdde130c676217ec748bec301b3f9a1aec 100644
--- a/src/SimpleFormulaChecker.hs
+++ b/src/SimpleFormulaChecker.hs
@@ -213,7 +213,7 @@ determineFormulaEq m1@(decls1, mbody1, env1) m2@(decls2, mbody2, env2) name = do
case model of
Just m -> do s <- evalZ3With Nothing (Z3.Opts.opt "timeout" (1000 :: Int)) (modelToString m) -- TODO: the option is set, but does not actually work :(
putStrLn s
- showRelevantModel $ parseModel s
+ -- showRelevantModel $ parseModel s
return False
_ -> return False
where
diff --git a/test/TExamples.hs b/test/TExamples.hs
index 249118c4bbe86dbe071df2681dfc365574d059c0..629d16e1dd1016ce473498790f9b7f065b372cce 100644
--- a/test/TExamples.hs
+++ b/test/TExamples.hs
@@ -14,7 +14,8 @@ testEquiv b s s' =
(.!=) = testEquiv False
equivalenceTests =
- [ "swap_spec1" .== "swap_spec1"
+ [ "real1" .== "real2"
+ , "swap_spec1" .== "swap_spec1"
, "swap_spec1" .!= "swap_spec2"
, "getMax_spec1" .!= "getMax_spec2"
, "test1" .!= "test2"
diff --git a/test/TIRParser.hs b/test/TIRParser.hs
index 1fbf9e52f66d2d39d2729a5684b8ba3a3493789f..dbcbd8c48a01a643bcc80c4e79a04d8925a569c7 100644
--- a/test/TIRParser.hs
+++ b/test/TIRParser.hs
@@ -25,8 +25,10 @@ parserTests =
LLen xArr .> n 1 .+ n 1
, "len(x:[int]) == 0 /\\ ! x:[int] == null" @?=
LLen xArr .== n 0 .&& lnot (LIsnull xArr)
+ , "len(x:[real]) == 0 /\\ ! x:[real] == null" @?=
+ LLen xArr' .== n 0 .&& lnot (LIsnull xArr')
]
where x = var "x" "int"
x' = v x
xArr = var "x" "[int]"
- xArr' = v xArr
+ xArr' = var "x" "[real]"