Command-line entry point.

app/Main.hs

+module Main where
+
+import SimpleFormulaChecker (compareSpec)
+import Data.Semigroup ((<>))
+import Options.Applicative
+import Control.Monad
+
+-- | Command-line options.
+data Options = Options
+  { src :: String
+  , method1 :: String
+  , method2 :: String
+  }
+
+-- | Parsing of command-line options.
+parseOptions :: Parser Options
+parseOptions = Options
+  <$> option auto
+      (  long "src"
+      <> showDefault
+      <> value "examples/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java"
+      <> metavar "STRING"
+      <> help "Java source file"
+      )
+  <*> strOption
+      (  short 'a'
+      <> metavar "STRING"
+      <> help "First method"
+      )
+  <*> strOption
+      (  short 'b'
+      <> metavar "STRING"
+      <> help "Second method"
+      )
+
+withInfo :: Parser a -> String -> ParserInfo a
+withInfo opts desc = info (helper <*> opts) $ progDesc desc
+
+-- | Main.
+main :: IO ()
+main = run =<< execParser (parseOptions `withInfo` "Java WLP")
+
+-- | Run.
+
+run :: Options -> IO ()
+run (Options src method1 method2) = void $
+  compareSpec (src, method1) (src, method2)

javawlp.cabal

@@ -6,6 +6,15 @@ build-type:          Simple
 extra-source-files:  README.md
 cabal-version:       >=1.10
 
+executable javawlp
+  hs-source-dirs:      app
+  main-is:             Main.hs
+  ghc-options:         -threaded -rtsopts -with-rtsopts=-N
+  build-depends:       base
+                     , javawlp
+                     , optparse-applicative
+  default-language:    Haskell2010
+
 library
   hs-source-dirs:      src
   exposed-modules:     Javawlp.Engine.Types
@@ -17,6 +26,7 @@ library
                      , LogicIR.Backend.Z3
                      , LogicIR.Backend.Test
                      , LogicIR.Backend.ModelGenerator
+                     , LogicIR.Backend.SBV
                      , LogicIR.Backend.Pretty
                      , LogicIR.Backend.Null
                      , LogicIR.Fold
@@ -40,6 +50,7 @@ library
                      , pretty
                      , mtl
                      , containers
+                     , sbv
   default-language:    Haskell2010
 
 test-suite javawlp-tests

src/LogicIR/Backend/Z3.hs

+{-# LANGUAGE OverloadedStrings #-}
 module LogicIR.Backend.Z3 (lExprToZ3Ast) where
 
 import Z3.Monad
 
 import LogicIR.Expr
 import LogicIR.Fold
+import LogicIR.Parser
 
 lExprToZ3Ast :: LExpr -> Z3 AST
 lExprToZ3Ast = foldLExpr lExprToZ3AstAlgebra
@@ -12,62 +14,69 @@ lExprToZ3Ast = foldLExpr lExprToZ3AstAlgebra
 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)
-                    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
-                             TPrim PInt32 -> mkBvVar symbol 32
-                             TPrim PBool -> mkBoolVar symbol
-                             TArray (TPrim PInt32) -> do intSort <- mkBvSort 32
-                                                         arraySort <- mkArraySort intSort intSort
-                                                         mkVar symbol arraySort
-                             TArray (TPrim PBool) -> do intSort <- mkBvSort 32
-                                                        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
-                         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
-                             NShr     -> mkBvashr a b -- NOTE: signed shift right will keep the sign
-                             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
-    fIf c' a' b' = do c <- c'
-                      a <- a'
-                      b <- b'
-                      mkIte c a b
-    fQuant o v@(Var t n) d' a' = do a <- a'
-                                    d <- d'
-                                    case t of
-                                         TPrim PInt32 -> do vApp <- fVar v >>= toApp
-                                                            case o of
-                                                                 QAll -> do e <- mkImplies d a
-                                                                            mkForallConst [] [vApp] e
-                                                                 QAny -> do e <- mkAnd [d, a]
-                                                                            mkExistsConst [] [vApp] e
-                                         _ -> error $ "unsupported quantifier domain type: " ++ show (o, v)
-    fArray v a' = do v <- fVar v
-                     a <- a'
-                     mkSelect v a
+      CBool b -> mkBool b
+      CInt n -> mkBitvector 32 (fromIntegral n)
+      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
+        "[int]" -> do
+          intSort <- mkBvSort 32
+          arraySort <- mkArraySort intSort intSort
+          mkVar symbol arraySort
+        "[bool]" -> do
+          intSort <- mkBvSort 32
+          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
+        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
+        NShr     -> mkBvashr a b -- NOTE: signed shift right will keep the sign
+        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
+    fIf c' a' b' = do
+      c <- c'
+      a <- a'
+      b <- b'
+      mkIte c a b
+    fQuant o v@(Var t n) d' a' = do
+      a <- a'
+      d <- d'
+      case t of
+        "int" -> do
+          vApp <- fVar v >>= toApp
+          case o of
+            QAll -> do e <- mkImplies d a
+                       mkForallConst [] [vApp] e
+            QAny -> do e <- mkAnd [d, a]
+                       mkExistsConst [] [vApp] e
+        _ -> error $ "unsupported quantifier domain type: " ++ show (o, v)
+    fArray v a' = do
+      v <- fVar v
+      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

src/LogicIR/Fold.hs

@@ -15,7 +15,6 @@ 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

stack.yaml

@@ -49,6 +49,9 @@ 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: {}

test/TExamples.hs

 module TExamples where
-
 import System.IO.Unsafe (unsafePerformIO)
 import System.IO.Silently (silence)
 import Test.HUnit

test/TIRParser.hs

@@ -7,26 +7,23 @@ import Test.HUnit
 import LogicIR.Expr
 import LogicIR.Parser
 
-infix 1 @~
-(@~) prog ast = prog @?= ast
-
 parserTests =
-  [ "1 + 1" @~ n 1 .+ n 1
-  , "(1 == 1 ? 1 : 2)" @~
+  [ "1 + 1" @?= n 1 .+ n 1
+  , "(1 == 1 ? 1 : 2)" @?=
       LIf (n 1 .== n 1) (n 1) (n 2)
-  , "true \\/ (1 == 1 ? 1 : 2)" @~
+  , "true \\/ (1 == 1 ? 1 : 2)" @?=
       b True .|| LIf (n 1 .== n 1) (n 1) (n 2)
-  , "true \\/ (1 == 1 ? 1 : 2)" @~
+  , "true \\/ (1 == 1 ? 1 : 2)" @?=
       b True .|| LIf (n 1 .== n 1) (n 1) (n 2)
-  , "(forall x:int :: x:int >= 1 -> x:int + 1 > 1)" @~
+  , "(forall x:int :: x:int >= 1 -> x:int + 1 > 1)" @?=
       forall x (v x .>= n 1) (x' .+ n 1 .> n 1)
-  , "(exists x:int :: x:int >= 1 -> x:int + 1 > 1)" @~
+  , "(exists x:int :: x:int >= 1 -> x:int + 1 > 1)" @?=
       exists x (v x .>= n 1) (x' .+ n 1 .> n 1)
-  , "(exists x:[int] :: true -> x:[int][5] > 1)" @~
+  , "(exists x:[int] :: true -> x:[int][5] > 1)" @?=
       exists xArr (b True) ((xArr .! n 5) .> n 1)
-  , "len(x:[int]) > 1 + 1" @~
+  , "len(x:[int]) > 1 + 1" @?=
       LLen xArr .> n 1 .+ n 1
-  , "len(x:[int]) == 0 /\\ ! x:[int] == null" @~
+  , "len(x:[int]) == 0 /\\ ! x:[int] == null" @?=
       LLen xArr .== n 0 .&& lnot (LIsnull xArr)
   ]
   where x = var "x" "int"