Tests: Real Arithmetic

examples/test_equiv/Doubles.java

+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);
+    }
+}

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

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

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

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

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..."

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_ "<" (.<)

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
+}

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)

test/TEquivalenceClasses.hs

 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 (.!=)
                 ]

test/TIRParser.hs

@@ -32,3 +32,4 @@ parserTests =
         x' = v x
         xArr = var "x" "[int]"
         xArr' = var "x" "[real]"
+        xArr'' = var "x" "[[real]]"