diff --git a/deploy.sh b/deploy.sh
new file mode 100755
index 0000000000000000000000000000000000000000..b8aaf9f295d8d93ef2b13d5c1d9fe2aad1cff959
--- /dev/null
+++ b/deploy.sh
@@ -0,0 +1,17 @@
+#!/bin/bash
+# $1: port number to run the server
+# $2: filename to log output
+
+# Get latest HEAD
+git pull origin master
+# Build project
+stack build
+# Kill previous process
+pkill javawlp
+# Backup previous log
+if [ -f $2 ]
+then
+ mv $2 "$2".backup
+fi
+ # Run server
+nohup stack exec javawlp -- --runServer -p $1 > $2 &
diff --git a/src/API.hs b/src/API.hs
index 56724a7464de321b7abbbbb9577da277e2a5094e..125d1f16fbf57a9c33f2ef42fbad6fbaba3ac3eb 100644
--- a/src/API.hs
+++ b/src/API.hs
@@ -2,19 +2,24 @@
module API where
import Control.Concurrent
+import Data.List (intercalate)
+import Data.List.Split (splitOn)
import Data.Maybe
-import Data.List.Split (splitOn)
+import Prelude hiding (log)
+import System.IO
import Javawlp.Engine.HelperFunctions
import Javawlp.Engine.Types
+import Language.Java.Pretty
import Language.Java.Syntax
import qualified LogicIR.Backend.QuickCheck.API as Test
-import qualified LogicIR.Backend.Z3.API as Z3
-import LogicIR.Expr
-import LogicIR.Frontend.Java (javaExpToLExpr)
-import LogicIR.Null (lExprPreprocessNull)
-import Model
+import qualified LogicIR.Backend.Z3.API as Z3
+import LogicIR.Expr
+import LogicIR.Frontend.Java (javaExpToLExpr)
+import LogicIR.Null (lExprPreprocessNull)
+import LogicIR.Pretty
+import Model
import Control.DeepSeq
import Control.Exception.Base
@@ -40,17 +45,42 @@ compareSpec :: Mode -- ^ The execution mode
-> (FilePath, String) -- ^ Specification 2
-> IO Response -- ^ Result of spec comparison.
compareSpec m pMode methodA methodB = do
- mv1 <- newEmptyMVar
- mv2 <- if m == Debug then newEmptyMVar else return mv1
- _ <- compareSpecHelper mv1 (checkSpec pMode Z3.equivalentTo)
- _ <- compareSpecHelper mv2 (checkSpec pMode Test.equivalentTo)
- res1 <- readMVar mv1
- res2 <- readMVar mv2 -- if Release then mv1 == mv2 and this won't block
- return $ getRes m res1 res2
- where -- | Runs f on a separate thread and stores the result in mv.
- compareSpecHelper mv f = forkIO $ do
- res <- f methodA methodB
- res `seq` putMVar mv res
+ -- Parsing.
+ [mA, mB] <- mapM (parseMethod pMode) [methodA, methodB]
+ log "\n********************************************************************"
+ log $ "MethodA:\n" ++ ppMethodDef mA ++ "\n"
+ log $ "MethodB:\n" ++ ppMethodDef mB ++ "\n"
+ res <- methodDefToLExpr mA mB "pre"
+ case res of
+ Left e -> do
+ log $ "*** ERROR: " ++ show e
+ return $ mkErrorResponse e
+ Right (preL, preL') -> do
+ log $ "Pre\n" ++ "~~~\n"
+ log $ "LExprA:\n" ++ prettyLExpr preL ++ "\n"
+ log $ "LExprB:\n" ++ prettyLExpr preL' ++ "\n"
+ res' <- methodDefToLExpr mA mB "post"
+ case res' of
+ Left e' -> do
+ log $ "*** ERROR: " ++ show e'
+ return $ mkErrorResponse e'
+ Right (postL, postL') -> do
+ log $ "Post\n" ++ "~~~~\n"
+ log $ "LExprA:\n" ++ prettyLExpr postL ++ "\n"
+ log $ "LExprB:\n" ++ prettyLExpr postL' ++ "\n"
+
+ mv1 <- newEmptyMVar
+ mv2 <- if m == Debug then newEmptyMVar else return mv1
+ mapM_ (compareSpecHelper mv1) [ ("Z3", Z3.equivalentTo)
+ , ("Test", Test.equivalentTo)
+ ]
+ res1 <- readMVar mv1
+ res2 <- readMVar mv2 -- if Release, this won't block
+ return $ getRes m res1 res2
+ where -- | Runs f on a separate thread and stores the result in mv.
+ compareSpecHelper mv (name, impl) = forkIO $ do
+ res <- checkSpec name impl (preL, preL') (postL, postL')
+ res `seq` putMVar mv res
-- | Makes sure that both Responses are the same, otherwise, if we
-- run in debug mode, an error will be thrown. If not in debug mode,
@@ -68,22 +98,13 @@ getRes Release resp _ = resp
getRes Debug resp resp' =
error $ "proveSpec says " ++ show resp ++ ", testSpec says " ++ show resp'
-checkSpec :: ParseMode -> EquivImpl -> (Source, String) -> (FilePath, String) -> IO Response
-checkSpec pMode equivTo methodA methodB = do
- [m1, m2] <- mapM (parseMethod pMode) [methodA, methodB]
- res <- methodDefToLExpr m1 m2 "pre"
- case res of
- Left e ->
- return $ ErrorResponse $ head $ splitOn "CallStack" e
- Right (preL, preL') -> do
- preRes <- preL `equivTo` preL'
- res' <- methodDefToLExpr m1 m2 "post"
- case res' of
- Left e' ->
- return $ ErrorResponse e'
- Right (postL, postL') -> do
- postRes <- postL `equivTo` postL'
- return $ preRes <> postRes
+checkSpec :: String -> EquivImpl -> (LExpr, LExpr) -> (LExpr, LExpr) -> IO Response
+checkSpec name equivTo (preL, preL') (postL, postL') = do
+ preRes <- preL `equivTo` preL'
+ log $ "PreResponse (" ++ name ++ "):\n" ++ show preRes ++ "\n"
+ postRes <- postL `equivTo` postL'
+ log $ "PostResponse (" ++ name ++ "):\n" ++ show postRes ++ "\n"
+ return $ preRes <> postRes
--------------------------------------------------------------------------------
@@ -130,3 +151,18 @@ extractExpr call = combineExprs $ map (\(MethodCall (Name [Ident _]) [a]) -> a)
combineExprs [] = true
combineExprs [e] = e
combineExprs (e:es) = e &* combineExprs es
+
+--------------------------------- Debugging ------------------------------------
+log :: String -> IO ()
+log = hPutStrLn stderr
+
+mkErrorResponse :: String -> Response
+mkErrorResponse = ErrorResponse . head . splitOn "\nCallStack"
+
+ppMethodDef :: MethodDef -> String
+ppMethodDef (typeDecls, stmt, typeEnv) =
+ ppTypeEnv typeEnv ++ "\n" ++ prettyPrint stmt
+
+ppTypeEnv :: TypeEnv -> String
+ppTypeEnv = intercalate ", " . map ppNT
+ where ppNT (n, t) = prettyPrint t ++ " " ++ prettyPrint n
diff --git a/src/LogicIR/Backend/QuickCheck/API.hs b/src/LogicIR/Backend/QuickCheck/API.hs
index aaebb684fb720a6801de7984aa36ac0b4c19d7ef..b6c919666ba390f5c7512876df098734c5314695 100644
--- a/src/LogicIR/Backend/QuickCheck/API.hs
+++ b/src/LogicIR/Backend/QuickCheck/API.hs
@@ -16,10 +16,10 @@ equivalentTo lexpr lexpr' = do
(eq, testModel) <- testEquality 1000 lexpr lexpr'
if eq
then return Equivalent
- else return $ NotEquivalent $ toZ3Model testModel
+ else return $ NotEquivalent $ toModel testModel
-toZ3Model :: (QC.Model, QC.ArrayModel) -> Model
-toZ3Model (m, arrayM) = do
+toModel :: (QC.Model, QC.ArrayModel) -> Model
+toModel (m, arrayM) = do
let arrayKeys = map LVar $ M.keys arrayM
let arrayVals = map (map LConst) $ M.elems arrayM
let arrayKVs = zip arrayKeys (map toModelVals arrayVals)
diff --git a/src/LogicIR/Frontend/Java.hs b/src/LogicIR/Frontend/Java.hs
index c50458e84106e8e4eb09cd8f71bce4ed674b5ebd..eab9bf1c82aee141a7f57c60d58e055410c949e8 100644
--- a/src/LogicIR/Frontend/Java.hs
+++ b/src/LogicIR/Frontend/Java.hs
@@ -17,7 +17,7 @@ javaExpToLExpr = foldExp javaExpToLExprAlgebra
-- Converts a name to a LogicIR.Var, it queries the type environment to find the correct type.
nameToVar :: Name -> TypeEnv -> [TypeDecl] -> Var
nameToVar name env decls =
- case arrayType of
+ case type_ of
PrimType BooleanT -> fromString(symbol ++ ":bool")
PrimType ShortT -> fromString(symbol ++ ":int")
PrimType IntT -> fromString(symbol ++ ":int")
@@ -29,9 +29,9 @@ nameToVar name env decls =
RefType (ArrayType (PrimType LongT)) -> fromString(symbol ++ ":[int]")
RefType (ArrayType (PrimType FloatT)) -> fromString(symbol ++ ":[real]")
RefType (ArrayType (PrimType DoubleT)) -> fromString(symbol ++ ":[real]")
- _ -> error $ "Unimplemented nameToVar: " ++ show (name, arrayType)
+ _ -> error $ "Unsupported type: " ++ prettyPrint type_ ++ " " ++ prettyPrint name
where
- (arrayType, symbol) = (lookupType decls env name, prettyPrint name)
+ (type_, symbol) = (lookupType decls env name, prettyPrint name)
javaExpToLExprAlgebra :: ExpAlgebra (TypeEnv -> [TypeDecl] -> LExpr)
javaExpToLExprAlgebra =
@@ -76,21 +76,21 @@ javaExpToLExprAlgebra =
MethodCall (Name [Ident method]) [ExpName name, rbegin, rend, Lambda (LambdaSingleParam (Ident bound)) (LambdaBlock (Block [BlockStmt (Return (Just expr))]))]
-> quantr method name rbegin rend bound expr
_
- -> error $ "Unimplemented fMethodInv: " ++ show inv
+ -> error $ "Unimplemented fMethodInv: " ++ prettyPrint inv
where quant method name bound expr =
let i = Var (TPrim PInt) bound
(zero, len) = (LConst (CInt 0), LLen (nameToVar name env decls))
in case method of
"forall" -> lquantr QAll i zero len expr
"exists" -> lquantr QAny i zero len expr
- _ -> error $ "Unimplemented fMethodInv: " ++ show inv
+ _ -> error $ "Unimplemented fMethodInv: " ++ prettyPrint inv
quantr method name rbegin rend bound expr =
let (begin, end) = (refold rbegin, refold rend)
(i, _) = (Var (TPrim PInt) bound, nameToVar name env decls)
in case method of
"forallr" -> lquantr QAll i begin end expr
"existsr" -> lquantr QAny i begin end expr
- _ -> error $ "Unimplemented fMethodInv: " ++ show inv
+ _ -> error $ "Unimplemented fMethodInv: " ++ prettyPrint inv
lquantr op i begin end expr =
LQuant op i (LBinop (v i .>= begin) LAnd (LBinop (LVar i) CLess end)) (refold expr)
refold expr =
@@ -100,7 +100,7 @@ javaExpToLExprAlgebra =
ArrayIndex (ExpName name) [expr]
-> LArray (nameToVar name env decls) (javaExpToLExpr expr env decls)
_
- -> error $ "Multidimensional arrays are not supported: " ++ show arrayIndex
+ -> error $ "Multidimensional arrays are not supported: " ++ prettyPrint arrayIndex
fExpName name env decls =
case name of
Name [Ident a, Ident "length"] -> LLen $ nameToVar (Name [Ident a]) env decls
@@ -136,7 +136,7 @@ javaExpToLExprAlgebra =
GThanE -> (.>=)
Equal -> (.==)
NotEq -> (.!=)
- _ -> error $ "Unsupported operation: " ++ show op
+ _ -> error $ "Unsupported operation: " ++ prettyPrint 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/stack.yaml b/stack.yaml
index 2dfeca2b41ed909f724df038ac86040e3583d32d..9a83bebe9d525aa0a08a98668a185105fcf16720 100644
--- a/stack.yaml
+++ b/stack.yaml
@@ -1,75 +1,9 @@
-# This file was automatically generated by 'stack init'
-#
-# Some commonly used options have been documented as comments in this file.
-# For advanced use and comprehensive documentation of the format, please see:
-# https://docs.haskellstack.org/en/stable/yaml_configuration/
-
-# A warning or info to be displayed to the user on config load.
-user-message: ! 'Warning (added by new or init): Specified resolver could not satisfy
- all dependencies. Some external packages have been added as dependencies.
-
- You can omit this message by removing it from stack.yaml
-
-'
-
-# Resolver to choose a 'specific' stackage snapshot or a compiler version.
-# A snapshot resolver dictates the compiler version and the set of packages
-# to be used for project dependencies. For example:
-#
-# resolver: lts-3.5
-# resolver: nightly-2015-09-21
-# resolver: ghc-7.10.2
-# resolver: ghcjs-0.1.0_ghc-7.10.2
-# resolver:
-# name: custom-snapshot
-# location: "./custom-snapshot.yaml"
resolver: lts-9.17
+# resolver: lts-9.21
+# resolver: lts-10.7
-# User packages to be built.
-# Various formats can be used as shown in the example below.
-#
-# packages:
-# - some-directory
-# - https://example.com/foo/bar/baz-0.0.2.tar.gz
-# - location:
-# git: https://github.com/commercialhaskell/stack.git
-# commit: e7b331f14bcffb8367cd58fbfc8b40ec7642100a
-# - location: https://github.com/commercialhaskell/stack/commit/e7b331f14bcffb8367cd58fbfc8b40ec7642100a
-# extra-dep: true
-# subdirs:
-# - auto-update
-# - wai
-#
-# A package marked 'extra-dep: true' will only be built if demanded by a
-# non-dependency (i.e. a user package), and its test suites and benchmarks
-# will not be run. This is useful for tweaking upstream packages.
packages:
- .
-# Dependency packages to be pulled from upstream that are not in the resolver
-# (e.g., acme-missiles-0.3)
+
extra-deps:
- z3-4.1.2
-
-# Override default flag values for local packages and extra-deps
-# flags: {}
-
-# Extra package databases containing global packages
-# extra-package-dbs: []
-
-# Control whether we use the GHC we find on the path
-# system-ghc: true
-#
-# Require a specific version of stack, using version ranges
-# require-stack-version: -any # Default
-# require-stack-version: ">=1.6"
-#
-# Override the architecture used by stack, especially useful on Windows
-# arch: i386
-# arch: x86_64
-#
-# Extra directories used by stack for building
-# extra-include-dirs: [/path/to/dir]
-# extra-lib-dirs: [/path/to/dir]
-#
-# Allow a newer minor version of GHC than the snapshot specifies
-# compiler-check: newer-minor