- wrote eval for LExpr;

- wrote a function in SimpleFormulaChecker.hs that can be used to evaluate (for now just preconditions) in java files;
- wrote some (for now) very basic tests for LExpr eval;
- worked on QuickCheck.hs, but I have some ideas (mainly regarding arrays) that I need to discuss before I proceed;
- added extra parentheses in Pretty.hs to make debugging the AST easier.

examples/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java

@@ -5,6 +5,18 @@ import static nl.uu.impress.EDSL.*;
 
 public class Main {
 
+    public static int simple_eval1() {
+        pre(~(-5 * 2) == (79 & 41)); // evaluates to 9 == 9
+    }
+
+    public static int simple_eval2() {
+        pre(~(-5 * 2) == (79 & 40)); // evaluates to 9 == 8
+    }
+
+    public static int simple_eval3(int a) {
+        pre(~(a * 2) == (79 & 40)); // can't evaluate due to undefined variable
+    }
+
     public static int mymin(int[] a, int b) {
         assert forall(a, i -> {
             return a[i] > b;

javawlp.cabal

@@ -15,9 +15,11 @@ library
                      , LogicIR.Parser
                      , LogicIR.Frontend.Java
                      , LogicIR.Backend.Z3
+                     , LogicIR.Backend.QuickCheck
                      , LogicIR.Backend.Pretty
                      , LogicIR.Backend.Null
                      , LogicIR.Fold
+                     , LogicIR.Eval
                      , ModelParser.Lexer
                      , ModelParser.Parser
                      , ModelParser.Model
@@ -31,6 +33,7 @@ library
   build-depends:       base >= 4.7 && < 5
                      , parsec
                      , z3
+                     , QuickCheck
                      , language-java
                      , array
                      , pretty
@@ -44,19 +47,20 @@ test-suite javawlp-tests
   main-is:             Spec.hs
   other-modules:       TExamples
                      , TIRParser
+                     , TIREval
   build-depends:       base
                      , javawlp
                      , test-framework
                      , test-framework-hunit
                      , HUnit
                      , z3
+                     , QuickCheck
                      , language-java
                      , array
                      , pretty
                      , mtl
                      , containers
                      , silently
-  -- ghc-options:         -threaded -rtsopts -with-rtsopts=-N
   default-language:    Haskell2010
 
 source-repository head

src/LogicIR/Backend/Pretty.hs

@@ -52,7 +52,7 @@ prettyLExprAlgebra = (fConst, prettyVar, fUnop, fBinop, fIf, fQuant, fArray, fIs
                     CInt n  -> show n
                     CNil    -> "nil"
     fUnop o a = prettyNUnop o ++ a
-    fBinop a o b = a ++ " " ++ prettyLBinop o ++ " " ++ b
+    fBinop a o b = "(" ++ a ++ " " ++ prettyLBinop o ++ " " ++ b ++ ")"
     fIf c a b = "(" ++ c ++ ") ? (" ++ a ++ ") : (" ++ b ++ ")"
     fQuant o v d a = '(' : show o ++ " " ++ prettyVar v ++ ": " ++ d ++ ": " ++ a ++ ")"
     fArray v a = prettyVar v ++ "[" ++ a ++ "]"

src/LogicIR/Backend/QuickCheck.hs

+module LogicIR.Backend.QuickCheck () where
+
+import LogicIR.Expr
+import LogicIR.Fold
+import LogicIR.Eval
+import Test.QuickCheck
+import Data.Maybe
+import Data.List (find)
+import Control.Exception
+
+{- 
+
+This module checks whether two LExprs are equal in the following manner:
+
+1. collect all currently known bounds of all variables in both LExprs
+2. 
+
+-}
+
+---- Tells, given a formula and a list of ranges for all variables in the formula,
+---- whether the formula evaluates to true or to false.
+--check :: LExpr -> [(Var, LExpr, LExpr)] -> LExpr
+--check e []     = e
+--check e varBounds = do
+--    let purelyBoundedVar = fstPureBounds varBounds
+--    let t@(v, mn, mx)    = if isJust purelyBoundedVar
+--                           then fromJust purelyBoundedVar
+--                           else head varBounds
+--    value <- choose (mn,mx)
+--    where randomVal       = 1
+--          cnst _          = []
+--          var v           = [v]
+--          uni _ a         = a
+--          bin a1 _ a2     = a1 ++ a2
+--          iff a1 a2 a3    = a1 ++ a2 ++ a3
+--          quant _ _ a1 a2 = a1 ++ a2
+--          arr v a         = v : a
+--          snull v         = [v]
+--          len v           = [v]
+
+-- Returns the first tuple in the given list that has pure bounds, i.e.
+-- both the minimum and maximum contain no variables.
+--fstPurelyBounded :: [(Var, LExpr, LExpr)] -> Maybe (Var, LExpr, LExpr)
+--fstPurelyBounded ranges = find pureBound ranges
+--    where pureBound (_, mn, mx) = (evalPossible mn) && (evalPossible mx)
+
+
+--getInstance :: (Var, LExpr, LExpr) -> LExpr
+--getInstance ((Var t s), mn, mx)
+
+-- Replaces all occurences in the secon argument of the first tuple argument
+-- with the second tuple argument, e.g. 
+-- substitute ("x", 5) "x + y" = "5 + y"
+--substitute :: (LExpr, LExpr) -> LExpr -> Bool
+--substitute t e = foldLExpr (substituteAlgebra t)
+
+--substituteAlgebra :: (LExpr, LExpr) -> LExprAlgebra Bool
+--substituteAlgebra (old, new) = (cnst, var, uni, bin, iff, quant, arr, snull, len)
+--    where cnst c           = subst (LConst c)
+--          uni op e         = LUnop op (subst e)
+--          bin le op re     = LBinop (subst le) op (subst re)
+--          iff ge e1 e2     = LIf (subst ge) (subst e1) (subst e2)
+--          var v            = subst (LVar v)
+--          quant op v a1 a2 = LQuant op (subst (LVar v)) (subst a1) (subst a2)
+--          arr v a          = subst (LArray (subst (LVar v)) (subst a))
+--          snull v          = subst (LVar v)
+--          len v            = subst (LVar v)
+
+--          subVar v         = if (LVar v) == old then new else (LVar v)
+--          subst e         = if e == old then new else e
+
+---- Returns the minimum and maximum range, expressed in LExprs, for
+---- every LVar in the given LExpr
+--findRanges :: LExpr -> [Var] -> [(LExpr, LExpr, LExpr)]
+--findRanges e = []
+
+---- Returns a list with all LVar's that appear in a given LExpr.
+--variables :: LExpr -> [Var]
+--variables = foldLExpr (cnst, var, uni, bin, iff, quant, arr, snull, len)
+--    where cnst _          = []
+--          var v           = [v]
+--          uni _ a         = a
+--          bin a1 _ a2     = a1 ++ a2
+--          iff a1 a2 a3    = a1 ++ a2 ++ a3
+--          quant _ _ a1 a2 = a1 ++ a2
+--          arr v a         = v : a
+--          snull v         = [v]
+--          len v           = [v]
\ No newline at end of file

src/LogicIR/Eval.hs

+module LogicIR.Eval (eval, evalPossible) where
+
+import LogicIR.Expr
+import LogicIR.Fold
+import LogicIR.Backend.Pretty
+
+import Data.Bits
+
+-- Returns True if an LExpr only contains constants and no variables whatsoever.
+evalPossible :: LExpr -> Bool
+evalPossible = foldLExpr evalPossibleAlgebra
+
+evalPossibleAlgebra :: LExprAlgebra Bool
+evalPossibleAlgebra = (cnst, var, uni, bin, iff, quant, arr, snull, len)
+    where cnst _          = True
+          uni _ c         = c
+          bin le _ re     = le && re
+          iff ge e1 e2    = ge && e1 && e2
+          var v           = False
+          quant _ _ a1 a2 = a1 && a2
+          arr v a         = False
+          snull v         = False
+          len v           = False
+
+-- Tells to which LConst a given LExpr evaluates.
+eval :: LExpr -> LConst
+eval = foldLExpr evalAlgebra
+
+evalAlgebra :: LExprAlgebra LConst
+evalAlgebra = (cnst, var, uni, bin, iff, quant, arr, snull, len)
+    where cnst b@(CBool _) = b
+          cnst i@(CInt  _) = i
+
+          uni NNeg (CInt i)  = CInt (-i)
+          uni NNot (CInt i)  = CInt (-i - 1)
+          uni LNot (CBool b) = CBool (not b)
+
+          bin le o re     = evalBin le o re
+
+          iff ge e1 e2    = if ge == (CBool True) then e1 else e2
+          -- TODO.
+          var v           = error "You can't call eval on an LExpr that contains vars"
+          quant _ _ a1 a2 = error "Quantifiers cannot yet be evaluated."
+          arr v a         = error "Arrays cannot yet be evaluated"
+          snull v         = error "Null checks cannot yet be evaluated"
+          len v           = error "Array length cannot yet be evaluated"
+
+-- Evaluates a binary operator expression.
+-- Comparison operators
+evalBin le       CEqual   re       = CBool (le == re)
+evalBin (CInt l) CLess    (CInt r) = CBool (l < r)
+evalBin (CInt l) CGreater (CInt r) = CBool (l > r)
+-- Logical operators
+evalBin (CBool l) LAnd  (CBool r) = CBool (l && r)
+evalBin (CBool l) LOr   (CBool r) = CBool (l || r)
+evalBin (CBool l) LImpl (CBool r) = CBool ((not l) || (l && r))
+-- Numerical operators
+evalBin (CInt l) o (CInt r) = CInt ((convert o) l r)
+     -- Both NShr and NShl are evaluated using the Data.Bits.shift function,
+     -- where a right shift is achieved by inverting the r integer.
+     where convert NAdd = (+)
+           convert NSub = (-)
+           convert NMul = (*)
+           convert NDiv = div
+           convert NRem = mod
+           convert NShl = shiftL
+           convert NShr = shiftR
+           convert NAnd = (.&.)
+           convert NOr  = (.|.)
+           convert NXor = xor

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
+                  LLen v         -> fLen v
\ No newline at end of file

src/SimpleFormulaChecker.hs

@@ -11,8 +11,10 @@ import Javawlp.Engine.Types
 import Javawlp.Engine.HelperFunctions
 
 import LogicIR.Expr
+import LogicIR.Eval
 import LogicIR.Frontend.Java
 import LogicIR.Backend.Z3
+--import LogicIR.Backend.QuickCheck
 import LogicIR.Backend.Pretty
 import LogicIR.Backend.Null
 
@@ -217,3 +219,13 @@ compareSpec method1@(_, name1) method2@(_, name2) = do
     putStrLn "\n----POST---"
     postAns <- determineFormulaEq m1 m2 "post"
     return $ preAns && postAns
+
+
+evaluate :: (FilePath, String) -> IO Bool
+evaluate method = do
+      m@(decls, mbody, env) <- parseMethod method
+      let e = extractExpr (getMethodCalls m "pre")
+      let lexpr = javaExpToLExpr e env decls
+      putStrLn (prettyLExpr lexpr)
+      return ((prettyLExpr (LConst (LogicIR.Eval.eval lexpr))) == "true")
+

test/Spec.hs

@@ -3,11 +3,13 @@ import Test.Framework.Providers.HUnit
 
 import TExamples
 import TIRParser
+import TIREval
 
 main = defaultMain
   [ constructTestSuite testName testSuite
   | (testName, testSuite) <- [ ("EXAMPLES", equivalenceTests)
                              , ("LIR_PARSER", parserTests)
+                             , ("EVAL", evalTests)
                              ]
   ]
 

test/TIREval.hs

+module TIREval where
+
+import System.IO.Unsafe (unsafePerformIO)
+import System.IO.Silently (silence)
+import Test.HUnit
+
+import SimpleFormulaChecker
+
+edslSrc = "examples/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java"
+
+testEval :: Bool -> String -> Assertion
+testEval b s =
+  unsafePerformIO (silence $ evaluate (edslSrc, s)) @?= b
+(.=) = testEval True
+(.!) = testEval False
+
+evalTests =
+  [ (.=) "simple_eval1"
+  , (.!) "simple_eval2"
+  ]