API: Simple server + docs

API.md

+## Welcome
+
+This is our webservice's API.
+
+Enjoy!
+
+## GET /compare
+
+Clients must supply the following data
+
+#### GET Parameters:
+
+- a
+  - **Values**: *examples/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java:real1, ...*
+  - **Description**: Method location formatted as: < java_source_file>:< method_name>
+
+- b
+  - **Values**: *examples/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java:real2, ...*
+  - **Description**: Method location formatted as: < java_source_file>:< method_name>
+
+#### Response:
+
+- Status code 200
+- Headers: []
+
+```javascript
+{ "model": {
+    "a": [0, -0.5],
+    "i": 10
+  },
+  "responseType": "NotEquivalent"
+}
+```

README.md

@@ -2,25 +2,46 @@
 We want to help students learn about formal program verification. One aspect of this is writing pre and post conditions for their programs. To help the students learn this we developed a tool that can compare two program specifications and can come up with a counter example if the two specifications don't match.
 
 One use case could be to integrate our tool in a submission system like [DOMjudge](https://www.domjudge.org). We then allow students to submit their programs and they get instant feedback on their work.
-
-A proof of concept can be found in `src/SimpleFormulaChecker.hs`, the "main" function is `compareSpec`.
-
-To compile the project you need to install following packages:
 
-- [z3](https://hackage.haskell.org/package/z3) (see the [repository wiki](https://git.science.uu.nl/d.h.ogilvie2/javawlp/wikis/Installing-z3-haskell) for installation instructions)
+## Dependencies:
+- [z3](https://hackage.haskell.org/package/z3)
+- [haskell](https://www.haskell.org/)
+- [stack](https://docs.haskellstack.org/en/stable/README/)
 
+## Usage
 To setup the Haskell project:
 ```
-stack setup
-stack build
-```
-To run the tests:
-```
-stack test
-```
-To start an interactive GHC session:
-```
-stack ghci
+> stack setup
+> stack build
+```
+
+Command-line usage:
+```
+stack exec javawlp --
+  [--srcA STRING] [--srcB STRING] [-a STRING] [-b STRING]
+  [-w|--runServer] [-p|--port INT]
+```
+
+To run a comparison between two methods:
+```
+> stack exec javawlp -- \
+  --srcA 'examples/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java' -a 'real1' \
+  --srcB 'examples/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java' -b 'real2'
+```
+
+To run the server API at port 8080:
+```
+> stack exec javawlp -- -p 8080 --runServer
+```
+
+To query the server (see [API.md](https://git.science.uu.nl/impresshs/javawlp/blob/master/API.md) for available options):
+```
+> curl localhost:8080/compare?a="examples/Main.java:real1"&b="examples/Main.java:real2"
+```
+
+To run the tests:
+```
+> stack test
 ```
 
 ## Java EDSL

app/Main.hs

 module Main where
 
-import SimpleFormulaChecker (compareSpec)
+import Control.Monad
 import Data.Semigroup ((<>))
 import Options.Applicative
-import Control.Monad
+import SimpleFormulaChecker (compareSpec)
+
+import Server (runApi)
 
 -- | Command-line options.
 data Options = Options
-  { src :: String
-  , method1 :: String
-  , method2 :: String
+  { srcA      :: String
+  , srcB      :: String
+  , method1   :: String
+  , method2   :: String
+  , runServer :: Bool
+  , port      :: Int
   }
 
 -- | Parsing of command-line options.
 parseOptions :: Parser Options
 parseOptions = Options
-  <$> option auto
-      (  long "src"
+  <$> strOption
+      (  long "srcA"
+      <> showDefault
+      <> value "examples/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java"
+      <> metavar "STRING"
+      <> help "Java source file for A"
+      )
+  <*> strOption
+      (  long "srcB"
       <> showDefault
       <> value "examples/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java"
       <> metavar "STRING"
-      <> help "Java source file"
+      <> help "Java source file for B"
       )
   <*> strOption
       (  short 'a'
+      <> value "_default_"
       <> metavar "STRING"
       <> help "First method"
       )
   <*> strOption
       (  short 'b'
+      <> value "_default_"
       <> metavar "STRING"
       <> help "Second method"
       )
+  <*> switch
+      (  short 'w'
+      <> long "runServer"
+      <> help "Run server"
+      )
+  <*> option auto
+      (  short 'p'
+      <> long "port"
+      <> metavar "INT"
+      <> showDefault
+      <> value 8888
+      <> help "Listening port"
+      )
 
 withInfo :: Parser a -> String -> ParserInfo a
 withInfo opts desc = info (helper <*> opts) $ progDesc desc
 
 -- | Main.
 main :: IO ()
-main = run =<< execParser (parseOptions `withInfo` "Java WLP")
+main = runMain =<< execParser (parseOptions `withInfo` "Java WLP")
 
 -- | Run.
-
-run :: Options -> IO ()
-run (Options src method1 method2) = void $
-  compareSpec (src, method1) (src, method2)
+runMain :: Options -> IO ()
+runMain (Options srcA srcB methodA methodB runServer port) =
+  if runServer then
+    runApi
+  else do
+    when (methodA == "_default_") $ fail "No files given."
+    response <- compareSpec (srcA, methodA) (srcB, methodB)
+    print response

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

@@ -92,7 +92,7 @@ public class Main {
     }
 
     public static void swap_spec3(int[] a, int i, int j) {
-        pre(a == null);
+        // pre(a == null);
         pre(a.length > 0);
         pre(i >= 0);
         pre(j >= 0);
@@ -104,6 +104,7 @@ public class Main {
     }
 
     public static void swap_spec4(int[] a, int i, int j) {
+        pre(a != null);
         pre(a.length > 0);
         pre(i >= 0);
         pre(j >= 0);

javawlp.cabal

@@ -20,6 +20,8 @@ library
   exposed-modules:     Javawlp.Engine.Types
                      , Javawlp.Engine.HelperFunctions
                      , Javawlp.Engine.Folds
+                     -- Server
+                     , Server
                      -- LIR
                      , LogicIR.Expr
                      , LogicIR.Fold
@@ -54,6 +56,19 @@ library
                      , pretty
                      , mtl
                      , containers
+                     , servant
+                     , servant-server
+                     , servant-docs
+                     , transformers
+                     , aeson
+                     , wai
+                     , warp
+                     , split
+                     , mtl
+                     , vector
+                     , bytestring
+                     , text
+                     , http-types
   default-language:    Haskell2010
 
 test-suite javawlp-tests

src/LogicIR/Backend/Z3/Model.hs

-{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE FlexibleInstances    #-}
+{-# LANGUAGE OverloadedStrings    #-}
+{-# LANGUAGE TypeSynonymInstances #-}
 module LogicIR.Backend.Z3.Model where
 
 import qualified Data.Map as M
 import Data.String
+import Data.List (isSuffixOf)
 import Text.Parsec hiding (runP)
 import Text.Parsec.Expr
 import Text.Parsec.Language
@@ -16,7 +19,7 @@ data ModelVal = BoolVal Bool
               | IntVal Integer
               | RealVal Double
               | ManyVal [ModelVal]
-              deriving (Eq)
+              deriving Eq
 
 type Z3Model = M.Map String ModelVal
 emptyZ3Model = M.empty :: Z3Model
@@ -30,13 +33,20 @@ instance Show ModelVal where
 
 -- | Crop arrays until their specified length.
 sanitize :: Z3Model -> Z3Model
-sanitize model = M.mapWithKey f model
+sanitize model =
+  M.filterWithKey isNotLen $ M.filterWithKey isNotNull $ M.mapWithKey f model
   where f k (ManyVal array) = ManyVal $ take (counts k) array
-        f _ x = x
+        f _ x               = x
         counts k = fromInteger $
           case model M.! (k ++ "?length") of
             (IntVal i) -> i
-            _ -> error "non-int length"
+            _          -> error "non-int length"
+        isNotNull k _ =
+          ((k ++ "?null") `M.notMember` model) ||
+          case model M.! (k ++ "?null") of
+            (BoolVal b) -> not b
+            _           -> error "non-bool null"
+        isNotLen k _ = not $ "?length" `isSuffixOf` k
 
 -- | Parsers.
 modelP :: Parser ModelVal

src/Server.hs

+{-# LANGUAGE DataKinds     #-}
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE OverloadedStrings #-}
+module Server (runApi) where
+
+import Data.Maybe
+import qualified Data.Map as M
+import Data.List.Split (splitOn)
+import Control.Monad.Trans (liftIO)
+import Data.Vector (fromList)
+import Data.ByteString.Lazy (ByteString)
+import Data.Proxy
+import Data.Text.Lazy.Encoding (encodeUtf8)
+import Data.Text.Lazy (pack)
+import Data.Aeson
+
+import Control.Monad.Trans.Except
+import System.IO
+import GHC.Generics
+
+import Network.HTTP.Types
+import Network.Wai.Handler.Warp
+import Network.Wai
+import Servant
+import Servant.Server
+import Servant.Docs
+
+import SimpleFormulaChecker (compareSpec)
+import qualified SimpleFormulaChecker as S
+import LogicIR.Backend.Z3.Model
+
+-- | Data types.
+type ApiArg = String
+data ApiResponseType = Equivalent | NotEquivalent | Undefined
+  deriving Generic
+data ApiResponse = ApiResponse
+  { responseType :: ApiResponseType
+  , model :: Maybe Z3Model
+  }
+  deriving Generic
+instance ToJSON ApiResponseType
+instance ToJSON ApiResponse
+instance ToJSON ModelVal where
+  toJSON (BoolVal b) = toJSON b
+  toJSON (IntVal n) = toJSON n
+  toJSON (RealVal n) = toJSON n
+  toJSON (ManyVal vs) = Array $ fromList $ map toJSON vs
+
+type CompareApi = "compare"
+  :> QueryParam "a" ApiArg
+  :> QueryParam "b" ApiArg
+  :> Get '[JSON] ApiResponse
+
+compareApi :: Proxy CompareApi
+compareApi = Proxy
+
+-- | API documentation.
+instance ToParam (QueryParam "a" String) where
+  toParam _ =
+    DocQueryParam "a" ["examples/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java:real1", "..."]
+                  "Method location formatted as: <java_source_file>:<method_name>"
+                  Normal
+
+instance ToParam (QueryParam "b" String) where
+  toParam _ =
+    DocQueryParam "b" ["examples/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java:real2", "..."]
+                  "Method location formatted as: <java_source_file>:<method_name>" Normal
+
+instance ToSample ApiResponse where
+  toSamples _ = singleSample ApiResponse
+    { responseType = NotEquivalent
+    , model = Just $ M.fromList
+      [ ("a", ManyVal [RealVal 0.0, RealVal (-0.5)])
+      , ("i", IntVal 10)
+      ]
+    }
+
+docsBS :: ByteString
+docsBS = encodeUtf8
+       . pack
+       . markdown
+       $ docsWithIntros [intro] compareApi
+  where intro = DocIntro "Welcome" ["This is our webservice's API.", "Enjoy!"]
+
+apiDocs :: API
+apiDocs = docs compareApi
+
+type DocsApi = CompareApi :<|> Raw
+
+docsApi :: Proxy DocsApi
+docsApi = Proxy
+
+server :: Server DocsApi
+server = server' :<|> Tagged serveDocs where
+    serveDocs _ respond =
+        respond $ responseLBS ok200 [plain] docsBS
+    plain = ("Content-Type", "text/plain")
+
+app :: Application
+app = serve docsApi server
+
+-- | Server implementation.
+runApi :: IO ()
+runApi = do
+  let port = 8888
+      settings =
+        setPort port $
+        setBeforeMainLoop (hPutStrLn stderr ("listening on port " ++ show port))
+        defaultSettings
+  runSettings settings app
+
+server' :: Server CompareApi
+server' = getCompareResponse
+
+getCompareResponse :: Maybe String -> Maybe String -> Handler ApiResponse
+getCompareResponse a b = do
+    let [srcA, methodA] = splitOn ":" (fromJust a)
+    let [srcB, methodB] = splitOn ":" (fromJust b)
+    response <- liftIO $ compareSpec (srcA, methodA) (srcB, methodB)
+    return $ case response of
+                  S.Equivalent ->
+                    ApiResponse { responseType = Equivalent, model = Nothing }
+                  S.NotEquivalent model ->
+                    ApiResponse { responseType = NotEquivalent, model = Just model }
+                  _ -> ApiResponse { responseType = Undefined, model = Nothing }

src/SimpleFormulaChecker.hs

@@ -5,6 +5,7 @@ import Control.Monad (when)
 import Control.Monad.Trans (liftIO)
 import qualified Data.Map as M
 import Data.Maybe
+import Data.String
 
 import Javawlp.Engine.HelperFunctions
 import Javawlp.Engine.Types
@@ -25,7 +26,7 @@ import LogicIR.Pretty (prettyLExpr)
 
 -- | Response type.
 data Response = Equivalent | NotEquivalent Z3Model | Undefined | Timeout
-                deriving (Eq, Show)
+                deriving (Eq)
 
 (<>) :: Response -> Response -> Response
 Equivalent <> r = r
@@ -33,6 +34,14 @@ NotEquivalent s <> _ = NotEquivalent s
 Timeout <> _ = Timeout
 Undefined <> _ = Undefined
 
+instance Show Response where
+  show Equivalent = "Formulas are equivalent"
+  show Undefined = "Oops... could not determine if formulas are equivalent"
+  show Timeout = "Timeout occured"
+  show (NotEquivalent model) = "Not equivalent: " ++ show model
+
+debug = False
+
 -- Function that compares both the pre and the post condition for two methods.
 -- It is assumed that both methods have the same environment (parameter names, class member names, etc).
 compareSpec :: (FilePath, String) -> (FilePath, String) -> IO Response
@@ -42,9 +51,9 @@ compareSpec method1@(_, name1) method2@(_, name2) = do
     m2@(decls2, mbody2, env2) <- parseMethod method2
     when (decls1 /= decls2) $ fail "inconsistent class declarations"
     -- when (env1 /= env2) $ fail "inconsistent environments"
-    putStrLn $ "----PRE---- (" ++ name1 ++ " vs " ++ name2 ++ ")"
+    -- putStrLn $ "----PRE---- (" ++ name1 ++ " vs " ++ name2 ++ ")"
     preAns <- determineFormulaEq m1 m2 "pre"
-    putStrLn "\n----POST---"
+    -- putStrLn "\n----POST---"
     postAns <- determineFormulaEq m1 m2 "post"
     return $ preAns <> postAns
 
@@ -53,10 +62,10 @@ determineFormulaEq :: MethodDef -> MethodDef -> String -> IO Response
 determineFormulaEq m1@(decls1, mbody1, env1) m2@(decls2, mbody2, env2) name = do
     -- get pre/post condition
     let (e1, e2) = (extractCond m1 name, extractCond m2 name)
-    putStrLn $ "e1:\n" ++ prettyPrint e1 ++ "\n\ne2:\n" ++ prettyPrint e2 ++ "\n"
+    when debug $ putStrLn $ "e1:\n" ++ prettyPrint e1 ++ "\n\ne2:\n" ++ prettyPrint e2 ++ "\n"
     let (l1, l2) = (javaExpToLExpr e1 env1 decls1, javaExpToLExpr e2 env2 decls2)
     let (l, l') = (lExprPreprocessNull l1, lExprPreprocessNull l2) -- preprocess "a == null" to "isNull(a)"
-    putStrLn $ "LogicIR.Pretty 1:\n" ++ prettyLExpr l ++ "\n\nLogicIR.Pretty 2:\n" ++ prettyLExpr l' ++ "\n"
+    -- putStrLn $ "LogicIR.Pretty 1:\n" ++ prettyLExpr l ++ "\n\nLogicIR.Pretty 2:\n" ++ prettyLExpr l' ++ "\n"
     z3Response <- l `Z3.equivalentTo` l'
     case z3Response of
       Z3.Equivalent      -> return Equivalent