From 0be6c7c9f4442d7096182a3a6586fd91c5f3dd73 Mon Sep 17 00:00:00 2001
From: Orestis Melkonian <melkon.or@gmail.com>
Date: Sun, 28 Jan 2018 23:26:27 +0100
Subject: [PATCH] Tests: Real Arithmetic
---
examples/test_equiv/Doubles.java | 56 +++++++++++++++++++
.../uu/javawlp_edsl => test_equiv}/Test.java | 0
src/LogicIR/Backend/Pretty.hs | 6 --
src/LogicIR/Backend/Z3.hs | 10 +---
src/LogicIR/Expr.hs | 12 ----
src/LogicIR/Fold.hs | 2 +-
src/LogicIR/Frontend/Java.hs | 8 +--
src/LogicIR/Parser.hs | 5 +-
src/ModelParser/Parser.y | 2 +-
src/SimpleFormulaChecker.hs | 6 +-
test/TEquivalenceClasses.hs | 20 +++++--
test/TIRParser.hs | 1 +
12 files changed, 82 insertions(+), 46 deletions(-)
create mode 100644 examples/test_equiv/Doubles.java
rename examples/{javawlp_edsl/src/nl/uu/javawlp_edsl => test_equiv}/Test.java (100%)
diff --git a/examples/test_equiv/Doubles.java b/examples/test_equiv/Doubles.java
new file mode 100644
index 0000000..56f64ec
--- /dev/null
+++ b/examples/test_equiv/Doubles.java
@@ -0,0 +1,56 @@
+package nl.uu;
+import static nl.uu.impress.EDSL.*;
+
+public class Doubles {
+
+ // 1) Simple real arithmetic
+ public static float real1_1(float a) {
+ pre(a >= (2 - 1 + 1));
+ a += a;
+ post(a >= (4 - 3 + 3));
+ }
+
+ public static float real2_1(float a) {
+ pre(a > 2 || a == 2);
+ a = a * 2;
+ post(a > 4 || a == 4);
+ }
+
+ public static float real3_1(float a) {
+ pre(a > 1);
+ pre(a > 2 || a == 2);
+ a = a * 2;
+ a = a / 2;
+ a = a * 2;
+ post(a > 4 || a == 4);
+ post(a > 3);
+ }
+
+ // 2) Different Java precision (irrelevant for LIR)
+ public static float real1_2(float a, double b) {
+ pre(a % b == 0 && a == 7.0);
+ c = a / b;
+ post(c == 1.0 || c == 7.0);
+ }
+
+ public static float real2_2(float a, double b) {
+ pre(a % b == 0 || false);
+ pre(a == 3 * 10 - 23 && true);
+ c = a / b;
+ post(c == 7/(1 + 5.1 - 5.1) || c == 1.0/(1.0 * 15 / 15));
+ }
+
+ // 3) Mix ints
+ public static float real1_3(float a, int b) {
+ pre(a > b && a < b + .3);
+ b += 1;
+ post(a < b - .7);
+ }
+
+ public static float real2_3(float a, int b) {
+ pre(a > b);
+ pre(a - (10 * .3 / 10) < b);
+ b += 1;
+ post(a + (.7 * (10 - 9.0)) < b);
+ }
+}
diff --git a/examples/javawlp_edsl/src/nl/uu/javawlp_edsl/Test.java b/examples/test_equiv/Test.java
similarity index 100%
rename from examples/javawlp_edsl/src/nl/uu/javawlp_edsl/Test.java
rename to examples/test_equiv/Test.java
diff --git a/src/LogicIR/Backend/Pretty.hs b/src/LogicIR/Backend/Pretty.hs
index 6d6ef05..b1da39c 100644
--- a/src/LogicIR/Backend/Pretty.hs
+++ b/src/LogicIR/Backend/Pretty.hs
@@ -24,11 +24,6 @@ prettyLBinop op =
NMul -> "*"
NDiv -> "/"
NRem -> "%"
- NShl -> ">>"
- NShr -> "<<"
- NAnd -> "&"
- NOr -> "|"
- NXor -> "^"
LAnd -> "&&"
LOr -> "||"
LImpl -> "->"
@@ -40,7 +35,6 @@ prettyNUnop :: LUnop -> String
prettyNUnop op =
case op of
NNeg -> "-"
- NNot -> "~"
LNot -> "!"
prettyVar :: Var -> String
diff --git a/src/LogicIR/Backend/Z3.hs b/src/LogicIR/Backend/Z3.hs
index 366cdcd..ad2a7a5 100644
--- a/src/LogicIR/Backend/Z3.hs
+++ b/src/LogicIR/Backend/Z3.hs
@@ -44,7 +44,6 @@ lExprToZ3AstAlgebra = (fConst, fVar, fUnop, fBinop, fIf, fQuant, fArray, fIsnull
a <- a'
case o of
NNeg -> mkUnaryMinus a
- NNot -> mkBvnot a --
LNot -> mkNot a
fBinop a' o b' = do
a <- a'
@@ -53,13 +52,8 @@ lExprToZ3AstAlgebra = (fConst, fVar, fUnop, fBinop, fIf, fQuant, fArray, fIsnull
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 --
+ NDiv -> mkDiv a b
+ NRem -> mkRem a b
LAnd -> mkAnd [a, b]
LOr -> mkOr [a, b]
LImpl -> mkImplies a b
diff --git a/src/LogicIR/Expr.hs b/src/LogicIR/Expr.hs
index ddcae70..5b89e77 100644
--- a/src/LogicIR/Expr.hs
+++ b/src/LogicIR/Expr.hs
@@ -19,7 +19,6 @@ data Var = Var Type String
-- | Unary operators.
data LUnop = NNeg -- -n (numeric negation)
- | NNot -- ~n (numeric binary not)
| LNot -- !n (logical not)
deriving (Show, Eq, Read)
@@ -31,12 +30,6 @@ data LBinop =
| NMul -- a * b
| NDiv -- a / b
| NRem -- a % b
- -- bit-wise operators
- | NShl -- a >> b
- | NShr -- a << b
- | NAnd -- a & b
- | NOr -- a | b
- | NXor -- a ^ b
-- logical operators
| LAnd -- a && b
| LOr -- a || b
@@ -84,7 +77,6 @@ n = LConst . CInt
b = LConst . CBool
nil = LConst CNil
lnot = LUnop LNot
-nnot = LUnop NNot
infix 1 .: ; infix 1 .!
(.:) x t = LVar $ Var t x
@@ -95,10 +87,6 @@ infix 2 .==> ; infix 3 .&& ; infix 3 .||
infix 4 .== ; infix 4 .!= ; infix 4 .> ; infix 4 .< ; infix 4 .<= ; infix 4 .>=
infix 5 .* ; infix 5 ./ ; infix 5 .%
infix 6 .+ ; infix 6 .-
-infix 7 .>> ; infix 7 .<<
-infix 8 .| ; infix 8 .^ ; infix 8 .&
-(.|) = binOp NOr ; (.^) = binOp NXor ; (.&) = binOp NAnd
-(.>>) = binOp NShl ; (.<<) = binOp NShr
(.+) = binOp NAdd ; (.-) = binOp NSub
(.*) = binOp NMul ; (./) = binOp NDiv ; (.%) = binOp NRem
(.==) = binOp CEqual ; (.!=) x y = lnot $ x .== y
diff --git a/src/LogicIR/Fold.hs b/src/LogicIR/Fold.hs
index dbed0f9..fb9f4c3 100644
--- a/src/LogicIR/Fold.hs
+++ b/src/LogicIR/Fold.hs
@@ -15,7 +15,7 @@ type LExprAlgebra r = (LConst -> r, -- LConst
)
-- Fold for logical expressions
-foldLExpr :: LExprAlgebra r -> LExpr -> r
+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 b15375c..bfe7320 100644
--- a/src/LogicIR/Frontend/Java.hs
+++ b/src/LogicIR/Frontend/Java.hs
@@ -114,7 +114,7 @@ javaExpToLExprAlgebra =
fPreDecrement = error "fPreDecrement has side effects..."
fPrePlus e = e
fPreMinus e env decls = LUnop NNeg (e env decls)
- fPreBitCompl e env decls = LUnop NNot (e env decls)
+ fPreBitCompl e env decls = error "Bitwise operations not supported..."
fPreNot e env decls = LUnop LNot (e env decls)
fCast = error "fCast is not supported..." -- TODO: perhaps support cast for some types?
fBinOp e1 op e2 env decls = -- TODO: type checking?
@@ -128,12 +128,7 @@ javaExpToLExprAlgebra =
Rem -> (.%)
Add -> (.+)
Sub -> (.-)
- LShift -> (.>>)
- RShift -> (.<<)
RRShift -> undefined
- And -> (.&)
- Or -> (.|)
- Xor -> (.^)
-- Logical
CAnd -> (.&&)
COr -> (.||)
@@ -144,6 +139,7 @@ javaExpToLExprAlgebra =
GThanE -> (.>=)
Equal -> (.==)
NotEq -> (.!=)
+ _ -> error $ "Unsupported operation: " ++ show op
fInstanceOf = error "fInstanceOf is not supported..."
fCond c a b env decls = LIf (c env decls) (a env decls) (b env decls)
fAssign = error "fAssign has side effects..."
diff --git a/src/LogicIR/Parser.hs b/src/LogicIR/Parser.hs
index 41d9fd3..68fb24f 100644
--- a/src/LogicIR/Parser.hs
+++ b/src/LogicIR/Parser.hs
@@ -25,10 +25,7 @@ exprP :: Parser LExpr
exprP =
buildExpressionParser table term <?> "expression"
where table = [ -- Numeric
- [ prefix "~" nnot]
- , [ infix_ ">>" (.>>), infix_ "<<" (.<<) ]
- , [ infix_ "&" (.&), infix_ "|" (.|), infix_ "^" (.^) ]
- , [ infix_ "*" (.*), infix_ "/" (./), infix_ "%" (.%) ]
+ [ infix_ "*" (.*), infix_ "/" (./), infix_ "%" (.%) ]
, [ infix_ "+" (.+) , infix_ "-" (.-) ]
-- Comparison
, [ infix_ "==" (.==) , infix_ "!=" (.!=) , infix_ "<" (.<)
diff --git a/src/ModelParser/Parser.y b/src/ModelParser/Parser.y
index c9b1576..b9bc4a3 100644
--- a/src/ModelParser/Parser.y
+++ b/src/ModelParser/Parser.y
@@ -54,4 +54,4 @@ parseError t = error $ "Model parse error " ++ show t
parseModel :: String -> Z3Model
parseModel = happyParseTokens . alexScanTokens
-}
\ No newline at end of file
+}
diff --git a/src/SimpleFormulaChecker.hs b/src/SimpleFormulaChecker.hs
index 8d35c9c..1031d33 100644
--- a/src/SimpleFormulaChecker.hs
+++ b/src/SimpleFormulaChecker.hs
@@ -87,9 +87,9 @@ getMethodCalls (_, StmtBlock (Block bs), _) name = mapMaybe extractMethodInv bs
extractExpr :: [MethodInvocation] -> Exp
extractExpr call = combineExprs $ map (\(MethodCall (Name [Ident _]) [a]) -> a) call
where combineExprs :: [Exp] -> Exp
- combineExprs [] = Lit $ Boolean True -- If the expression is empty, just return True.
- combineExprs [e] = e
- combineExprs (e:es) = BinOp e CAnd (combineExprs es)
+ combineExprs [] = true
+ combineExprs [e] = e
+ combineExprs (e:es) = e &* combineExprs es
-- Check if two Z3 AST's are equivalent
isEquivalent :: Z3 AST -> Z3 AST -> IO (Result, Maybe Model)
diff --git a/test/TEquivalenceClasses.hs b/test/TEquivalenceClasses.hs
index 428ca78..522c3bb 100644
--- a/test/TEquivalenceClasses.hs
+++ b/test/TEquivalenceClasses.hs
@@ -1,12 +1,15 @@
module TEquivalenceClasses where
-import System.IO.Unsafe (unsafePerformIO)
-import System.IO.Silently (silence)
+
+import Data.List (elemIndex)
import Data.List.Split (splitOn)
+import System.IO.Silently (silence)
+import System.IO.Unsafe (unsafePerformIO)
+import Control.Monad
import Test.HUnit
import SimpleFormulaChecker (compareSpec, parseMethodIds)
-edslSrc = "examples/javawlp_edsl/src/nl/uu/javawlp_edsl/Test.java"
+edslSrc = "examples/test_equiv/Doubles.java"
testEquiv :: Bool -> String -> String -> Assertion
testEquiv b s s' =
@@ -17,8 +20,15 @@ testEquiv b s s' =
equivClassesTests =
let methodIds = unsafePerformIO (silence $ parseMethodIds edslSrc)
getClass = last . splitOn "_"
+ tailFrom :: Eq a => [a] -> a -> [a]
+ tailFrom xs x = case elemIndex x xs of Just i -> snd $ splitAt i xs
+ Nothing -> []
in [ a `op` b | a <- methodIds
- , b <- methodIds
+ , b <- methodIds `tailFrom` a
, a /= b
- , let op = if getClass a == getClass b then (.==) else (.!=)
+ , let op = unsafePerformIO $ do
+ let eq = getClass a == getClass b
+ putStrLn $ foldl1 (++)
+ [" (", a, if eq then " == " else " != ", b, ")"]
+ return $ if eq then (.==) else (.!=)
]
diff --git a/test/TIRParser.hs b/test/TIRParser.hs
index dbcbd8c..e61a4a1 100644
--- a/test/TIRParser.hs
+++ b/test/TIRParser.hs
@@ -32,3 +32,4 @@ parserTests =
x' = v x
xArr = var "x" "[int]"
xArr' = var "x" "[real]"
+ xArr'' = var "x" "[[real]]"
--
GitLab