From 47b9f3fca0aafbf4a8f3d0a0dcb6460b8d078f86 Mon Sep 17 00:00:00 2001
From: ISWB Prasetya <iswbprasetya@iswbs-mbp.home>
Date: Wed, 16 Aug 2017 20:02:39 +0200
Subject: [PATCH] putting back a function to calculate the wlp of a method and
check its satisfiability.
---
src/Javawlp/API.hs | 17 ++++++++++++++++-
src/Javawlp/Engine/Verifier.hs | 16 ++++++++++++++++
2 files changed, 32 insertions(+), 1 deletion(-)
diff --git a/src/Javawlp/API.hs b/src/Javawlp/API.hs
index 30c9926..84e7c76 100644
--- a/src/Javawlp/API.hs
+++ b/src/Javawlp/API.hs
@@ -6,6 +6,7 @@ module Javawlp.API where
import Language.Java.Syntax
import Language.Java.Parser
import Language.Java.Pretty
+import Z3.Monad
import Javawlp.Engine.WLP
import Javawlp.Engine.Types
@@ -77,9 +78,23 @@ printWlp sourcePath methodName postCond = do
let q = post_ postCond
p <- wlpMethod defaultConf typeEnv decls (Ident methodName) q
putStrLn $ showMethodWlp methodName q p
+ let (result,model) = unsafeIsSatisfiable (extendEnv typeEnv decls (Ident methodName)) decls p
+ case result of
+ Unsat -> putStrLn "** The wlp is UNSATISFIABLE."
+ Undef -> putStrLn "** Unable to decide the wlp's satisfiablity."
+ _ -> do
+ putStrLn "** The wlp is SATISFIABLE."
+ case model of
+ Just m -> do { putStrLn "** Model:" ; s <- evalZ3 (modelToString m) ; putStrLn s }
+ _ -> return ()
+
showMethodWlp :: String -> Exp -> Exp -> String
showMethodWlp methodName postCond wlp =
- "wlp of " ++ methodName ++ " over " ++ prettyPrint postCond
+ "** wlp of " ++ methodName ++ " over " ++ prettyPrint postCond
++ " is "
++ prettyPrint wlp
+
+
+
+
diff --git a/src/Javawlp/Engine/Verifier.hs b/src/Javawlp/Engine/Verifier.hs
index d5e4c79..4661372 100644
--- a/src/Javawlp/Engine/Verifier.hs
+++ b/src/Javawlp/Engine/Verifier.hs
@@ -30,6 +30,22 @@ isFalse env decls e =
Unsat -> return True
_ -> return False
+-- | Check if a formula is satisfiable, and if so, return the model for it as well.
+-- The result is a pair (r,m) where r is either Sat, Unsat, or Undef. If r is Sat,
+-- then m is Just v where v a model witnessing the satisfiability of the input
+-- formula. Else m is Nothing.
+--
+unsafeIsSatisfiable :: TypeEnv -> [TypeDecl] -> Exp -> (Result, Maybe Model)
+unsafeIsSatisfiable env decls e = unsafePerformIO $ evalZ3 z3
+ where
+ z3 = do
+ ast <- foldExp expAssertAlgebra e env decls
+ assert ast
+ r <- solverCheckAndGetModel
+ solverReset
+ return r
+
+
-- | Unsafe version of isTrue
unsafeIsTrue :: TypeEnv -> [TypeDecl] -> Exp -> Bool
unsafeIsTrue env decls = unsafePerformIO . evalZ3 . isTrue env decls
--
GitLab