From 3d18fc67b7e388660847453b81096cff783737ef Mon Sep 17 00:00:00 2001
From: Orestis Melkonian <melkon.or@gmail.com>
Date: Mon, 15 Jan 2018 18:36:52 +0100
Subject: [PATCH] LIR: Real arithmetic
---
.../javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java | 12 ++++++++++++
javawlp.cabal | 2 --
src/LogicIR/Backend/Pretty.hs | 3 ++-
src/LogicIR/Backend/Z3.hs | 2 ++
src/LogicIR/Expr.hs | 2 ++
src/LogicIR/Fold.hs | 1 +
src/LogicIR/Frontend/Java.hs | 1 +
src/LogicIR/Parser.hs | 4 +++-
stack.yaml | 3 ---
9 files changed, 23 insertions(+), 7 deletions(-)
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 cec6feb..061e892 100644
--- a/examples/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java
+++ b/examples/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java
@@ -29,6 +29,18 @@ public class Main {
pre(~(a * 2) == (79 & 40)); // can't evaluate due to undefined variable
}
+ public static float float1(float a) {
+ pre(a >= 2);
+ a += a;
+ post(a >= 4);
+ }
+
+ public static float float2(float a) {
+ pre(a > 2 || a == 2);
+ a = a * 2;
+ post(a > 4 || a == 4);
+ }
+
public static int mymin(int[] a, int b) {
assert forall(a, i -> {
return a[i] > b;
diff --git a/javawlp.cabal b/javawlp.cabal
index c6f00f2..14b91a8 100644
--- a/javawlp.cabal
+++ b/javawlp.cabal
@@ -26,7 +26,6 @@ library
, LogicIR.Backend.Z3
, LogicIR.Backend.Test
, LogicIR.Backend.ModelGenerator
- , LogicIR.Backend.SBV
, LogicIR.Backend.Pretty
, LogicIR.Backend.Null
, LogicIR.Fold
@@ -50,7 +49,6 @@ library
, pretty
, mtl
, containers
- , sbv
default-language: Haskell2010
test-suite javawlp-tests
diff --git a/src/LogicIR/Backend/Pretty.hs b/src/LogicIR/Backend/Pretty.hs
index a311066..4af16c1 100644
--- a/src/LogicIR/Backend/Pretty.hs
+++ b/src/LogicIR/Backend/Pretty.hs
@@ -13,6 +13,7 @@ prettyLExpr = foldLExpr prettyLExprAlgebra
prettyType :: Type -> String
prettyType (TPrim PInt32) = "int"
prettyType (TPrim PBool) = "bool"
+prettyType (TPrim PFloat) = "float"
prettyType (TArray t) = prettyType t ++ "[]"
prettyLBinop :: LBinop -> String
@@ -43,7 +44,7 @@ prettyNUnop op =
LNot -> "!"
prettyVar :: Var -> String
-prettyVar (Var t n) = prettyType t ++ ":" ++ n
+prettyVar (Var t n) = n ++ ":" ++ prettyType t
prettyLExprAlgebra :: LExprAlgebra String
prettyLExprAlgebra = (fConst, prettyVar, fUnop, fBinop, fIf, fQuant, fArray, fIsnull, fLen) where
diff --git a/src/LogicIR/Backend/Z3.hs b/src/LogicIR/Backend/Z3.hs
index e45d099..6b1977f 100644
--- a/src/LogicIR/Backend/Z3.hs
+++ b/src/LogicIR/Backend/Z3.hs
@@ -16,12 +16,14 @@ lExprToZ3AstAlgebra = (fConst, fVar, fUnop, fBinop, fIf, fQuant, fArray, fIsnull
fConst c = case c of
CBool b -> mkBool b
CInt n -> mkBitvector 32 (fromIntegral n)
+ CFloat 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
"bool" -> mkBoolVar symbol
+ "float" -> mkRealVar symbol
"[int]" -> do
intSort <- mkBvSort 32
arraySort <- mkArraySort intSort intSort
diff --git a/src/LogicIR/Expr.hs b/src/LogicIR/Expr.hs
index 7049765..e9160a5 100644
--- a/src/LogicIR/Expr.hs
+++ b/src/LogicIR/Expr.hs
@@ -5,6 +5,7 @@ import Data.String
-- | The primitive types are bool and int32.
data Primitive = PBool
| PInt32
+ | PFloat
deriving (Show, Eq, Read)
-- | A Type can either be a primitive or an array type.
@@ -52,6 +53,7 @@ data QOp = QAll | QAny
-- | Constants.
data LConst = CBool Bool
| CInt Int
+ | CFloat Float
| CNil
deriving (Show, Eq, Read)
diff --git a/src/LogicIR/Fold.hs b/src/LogicIR/Fold.hs
index 2856788..dbed0f9 100644
--- a/src/LogicIR/Fold.hs
+++ b/src/LogicIR/Fold.hs
@@ -15,6 +15,7 @@ type LExprAlgebra r = (LConst -> r, -- LConst
)
-- Fold for logical expressions
+foldLExpr :: LExprAlgebra r -> LExpr -> r
foldLExpr (fConst, fVar, fUnop, fBinop, fIf, fQuant, fArray, fIsnull, fLen) = fold where
fold e = case e of
LConst c -> fConst c
diff --git a/src/LogicIR/Frontend/Java.hs b/src/LogicIR/Frontend/Java.hs
index 5f80a7c..4debba0 100644
--- a/src/LogicIR/Frontend/Java.hs
+++ b/src/LogicIR/Frontend/Java.hs
@@ -23,6 +23,7 @@ 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]")
_ -> error $ "Unimplemented nameToVar: " ++ show (name, arrayType)
where
diff --git a/src/LogicIR/Parser.hs b/src/LogicIR/Parser.hs
index feeeb72..ce5c222 100644
--- a/src/LogicIR/Parser.hs
+++ b/src/LogicIR/Parser.hs
@@ -92,7 +92,9 @@ bvarP = do
typeP :: Parser Type
typeP = try (TPrim <$> primTypeP) <|> (TArray <$> arrayTypeP)
where
- primTypeP = lexeme $ (PBool <$ str "bool") <|> (PInt32 <$ str "int")
+ primTypeP = lexeme (PBool <$ str "bool")
+ <|> (PInt32 <$ str "int")
+ <|> (PFloat <$ str "float")
arrayTypeP = "[" ~> typeP <~ "]"
-- | Useful marcros.
diff --git a/stack.yaml b/stack.yaml
index 5307da2..2dfeca2 100644
--- a/stack.yaml
+++ b/stack.yaml
@@ -49,9 +49,6 @@ packages:
# (e.g., acme-missiles-0.3)
extra-deps:
- z3-4.1.2
-- sbv-7.4
-- crackNum-1.9
-- FloatingHex-0.4
# Override default flag values for local packages and extra-deps
# flags: {}
--
GitLab