{-# Language LambdaCase #-}
{-# Language OverloadedStrings #-}
module Crux.Report where
import Data.Void (Void)
import System.FilePath
import System.Directory (createDirectoryIfMissing, canonicalizePath)
import System.IO
import qualified Data.Foldable as Fold
import Data.Functor.Const
import Data.List (partition)
import Data.Maybe (fromMaybe)
import qualified Data.Sequence as Seq
import Data.Sequence (Seq)
import qualified Data.Set as Set
import qualified Data.Text as Text
import Control.Exception (catch, SomeException(..))
import Control.Monad (forM_)
import Prettyprinter (Doc)
import qualified Data.Text.IO as T
import Lang.Crucible.Simulator.SimError
import Lang.Crucible.Backend
import What4.ProgramLoc
import What4.Expr (GroundValueWrapper)
import Crux.Types
import Crux.Config.Common
import Crux.Loops
import Crux.Model ( modelJS )
import Crux.UI.JS
import Crux.UI.Jquery (jquery)
import Crux.UI.IndexHtml (indexHtml)
generateReport :: CruxOptions -> CruxSimulationResult -> IO ()
generateReport :: CruxOptions -> CruxSimulationResult -> IO ()
generateReport CruxOptions
opts CruxSimulationResult
res
| CruxOptions -> String
outDir CruxOptions
opts String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
"" Bool -> Bool -> Bool
|| CruxOptions -> Bool
skipReport CruxOptions
opts = () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
| Bool
otherwise =
do let xs :: Seq (ProcessedGoals, ProvedGoals)
xs = CruxSimulationResult -> Seq (ProcessedGoals, ProvedGoals)
cruxSimResultGoals CruxSimulationResult
res
goals :: [ProvedGoals]
goals = ((ProcessedGoals, ProvedGoals) -> ProvedGoals)
-> [(ProcessedGoals, ProvedGoals)] -> [ProvedGoals]
forall a b. (a -> b) -> [a] -> [b]
map (ProcessedGoals, ProvedGoals) -> ProvedGoals
forall a b. (a, b) -> b
snd ([(ProcessedGoals, ProvedGoals)] -> [ProvedGoals])
-> [(ProcessedGoals, ProvedGoals)] -> [ProvedGoals]
forall a b. (a -> b) -> a -> b
$ Seq (ProcessedGoals, ProvedGoals)
-> [(ProcessedGoals, ProvedGoals)]
forall a. Seq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Fold.toList Seq (ProcessedGoals, ProvedGoals)
xs
referencedFiles :: [String]
referencedFiles = Set String -> [String]
forall a. Set a -> [a]
Set.toList ([String] -> Set String
forall a. Ord a => [a] -> Set a
Set.fromList (CruxOptions -> [String]
inputFiles CruxOptions
opts) Set String -> Set String -> Set String
forall a. Semigroup a => a -> a -> a
<> (ProvedGoals -> Set String) -> [ProvedGoals] -> Set String
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap ProvedGoals -> Set String
provedGoalFiles [ProvedGoals]
goals)
Bool -> String -> IO ()
createDirectoryIfMissing Bool
True (CruxOptions -> String
outDir CruxOptions
opts)
CruxOptions -> [String] -> IO ()
maybeGenerateSource CruxOptions
opts [String]
referencedFiles
[JS]
scs <- CruxOptions -> [ProvedGoals] -> IO [JS]
renderSideConds CruxOptions
opts [ProvedGoals]
goals
let contents :: String
contents = JS -> String
renderJS ([JS] -> JS
jsList [JS]
scs)
String -> String -> IO ()
writeFile (CruxOptions -> String
outDir CruxOptions
opts String -> String -> String
</> String
"report.js") (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"var goals = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
contents
String -> String -> IO ()
writeFile (CruxOptions -> String
outDir CruxOptions
opts String -> String -> String
</> String
"report.json") String
contents
String -> Text -> IO ()
T.writeFile (CruxOptions -> String
outDir CruxOptions
opts String -> String -> String
</> String
"index.html") Text
indexHtml
String -> Text -> IO ()
T.writeFile (CruxOptions -> String
outDir CruxOptions
opts String -> String -> String
</> String
"jquery.min.js") Text
jquery
maybeGenerateSource :: CruxOptions -> [FilePath] -> IO ()
maybeGenerateSource :: CruxOptions -> [String] -> IO ()
maybeGenerateSource CruxOptions
opts [String]
files =
do let exts :: [String]
exts = [String
".c", String
".i", String
".cc", String
".cpp", String
".cxx", String
".C", String
".ii", String
".h", String
".hpp", String
".hxx", String
".hh"]
renderFiles :: [String]
renderFiles = (String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
filter ((String -> [String] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
exts) (String -> Bool) -> (String -> String) -> String -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
takeExtension) [String]
files
Handle
h <- String -> IOMode -> IO Handle
openFile (CruxOptions -> String
outDir CruxOptions
opts String -> String -> String
</> String
"source.js") IOMode
WriteMode
Handle -> String -> IO ()
hPutStrLn Handle
h String
"var sources = ["
[String] -> (String -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [String]
renderFiles ((String -> IO ()) -> IO ()) -> (String -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \String
file -> do
String
absFile <- String -> IO String
canonicalizePath String
file
String
txt <- String -> IO String
readFile String
absFile
Handle -> String -> IO ()
hPutStr Handle
h (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"{\"label\":" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show (String -> String
takeFileName String
absFile) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
","
Handle -> String -> IO ()
hPutStr Handle
h (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"\"name\":" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
absFile String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
","
Handle -> String -> IO ()
hPutStr Handle
h (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"\"lines\":" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall a. Show a => a -> String
show (String -> [String]
lines String
txt)
Handle -> String -> IO ()
hPutStrLn Handle
h String
"},"
Handle -> String -> IO ()
hPutStrLn Handle
h String
"]"
Handle -> IO ()
hClose Handle
h
IO () -> (SomeException -> IO ()) -> IO ()
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`catch` \(SomeException {}) -> () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
provedGoalLocs :: ProvedGoals -> [ProgramLoc]
provedGoalLocs :: ProvedGoals -> [ProgramLoc]
provedGoalLocs = (Seq ProgramLoc -> [ProgramLoc])
-> Seq (Seq ProgramLoc) -> [ProgramLoc]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Seq ProgramLoc -> [ProgramLoc]
forall a. Seq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Fold.toList (Seq (Seq ProgramLoc) -> [ProgramLoc])
-> (ProvedGoals -> Seq (Seq ProgramLoc))
-> ProvedGoals
-> [ProgramLoc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProvedGoals -> Seq (Seq ProgramLoc)
provedGoalTraces
provedGoalTraces :: ProvedGoals -> Seq (Seq ProgramLoc)
provedGoalTraces :: ProvedGoals -> Seq (Seq ProgramLoc)
provedGoalTraces =
\case
Branch ProvedGoals
pgs1 ProvedGoals
pgs2 -> ProvedGoals -> Seq (Seq ProgramLoc)
provedGoalTraces ProvedGoals
pgs1 Seq (Seq ProgramLoc)
-> Seq (Seq ProgramLoc) -> Seq (Seq ProgramLoc)
forall a. Semigroup a => a -> a -> a
<> ProvedGoals -> Seq (Seq ProgramLoc)
provedGoalTraces ProvedGoals
pgs2
ProvedGoal [CrucibleAssumption (Const ())]
_ SimError
err [ProgramLoc]
locs Bool
_ ->
Seq ProgramLoc -> Seq (Seq ProgramLoc)
forall a. a -> Seq a
Seq.singleton ([ProgramLoc] -> Seq ProgramLoc
forall a. [a] -> Seq a
Seq.fromList [ProgramLoc]
locs Seq ProgramLoc -> ProgramLoc -> Seq ProgramLoc
forall a. Seq a -> a -> Seq a
Seq.|> SimError -> ProgramLoc
simErrorLoc SimError
err)
NotProvedGoal [CrucibleAssumption (Const ())]
_ SimError
err Doc Void
_ [ProgramLoc]
locs Maybe (ModelView, [CrucibleEvent GroundValueWrapper])
_ [String]
_ ->
Seq ProgramLoc -> Seq (Seq ProgramLoc)
forall a. a -> Seq a
Seq.singleton ([ProgramLoc] -> Seq ProgramLoc
forall a. [a] -> Seq a
Seq.fromList [ProgramLoc]
locs Seq ProgramLoc -> ProgramLoc -> Seq ProgramLoc
forall a. Seq a -> a -> Seq a
Seq.|> SimError -> ProgramLoc
simErrorLoc SimError
err)
provedGoalFiles :: ProvedGoals -> Set.Set FilePath
provedGoalFiles :: ProvedGoals -> Set String
provedGoalFiles = (Set String -> Position -> Set String)
-> Set String -> [Position] -> Set String
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
Fold.foldl' Set String -> Position -> Set String
ins Set String
forall a. Monoid a => a
mempty ([Position] -> Set String)
-> (ProvedGoals -> [Position]) -> ProvedGoals -> Set String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ProgramLoc -> Position) -> [ProgramLoc] -> [Position]
forall a b. (a -> b) -> [a] -> [b]
map ProgramLoc -> Position
plSourceLoc ([ProgramLoc] -> [Position])
-> (ProvedGoals -> [ProgramLoc]) -> ProvedGoals -> [Position]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProvedGoals -> [ProgramLoc]
provedGoalLocs
where
ins :: Set String -> Position -> Set String
ins Set String
s (SourcePos Text
f Int
_ Int
_) = String -> Set String -> Set String
forall a. Ord a => a -> Set a -> Set a
Set.insert (Text -> String
Text.unpack Text
f) Set String
s
ins Set String
s (BinaryPos Text
f Word64
_) = String -> Set String -> Set String
forall a. Ord a => a -> Set a -> Set a
Set.insert (Text -> String
Text.unpack Text
f) Set String
s
ins Set String
s Position
_ = Set String
s
renderSideConds :: CruxOptions -> [ProvedGoals] -> IO [ JS ]
renderSideConds :: CruxOptions -> [ProvedGoals] -> IO [JS]
renderSideConds CruxOptions
opts = (ProvedGoals -> IO [JS]) -> [ProvedGoals] -> IO [JS]
forall {t :: * -> *} {f :: * -> *} {a} {a}.
(Traversable t, Monad f) =>
(a -> f [a]) -> t a -> f [a]
concatMapM ProvedGoals -> IO [JS]
go
where
concatMapM :: (a -> f [a]) -> t a -> f [a]
concatMapM a -> f [a]
f t a
xs = t [a] -> [a]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (t [a] -> [a]) -> f (t [a]) -> f [a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> f [a]) -> t a -> f (t [a])
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> t a -> m (t b)
mapM a -> f [a]
f t a
xs
flatBranch :: [ProvedGoals] -> [ProvedGoals]
flatBranch (Branch ProvedGoals
x ProvedGoals
y : [ProvedGoals]
more) = [ProvedGoals] -> [ProvedGoals]
flatBranch (ProvedGoals
x ProvedGoals -> [ProvedGoals] -> [ProvedGoals]
forall a. a -> [a] -> [a]
: ProvedGoals
y ProvedGoals -> [ProvedGoals] -> [ProvedGoals]
forall a. a -> [a] -> [a]
: [ProvedGoals]
more)
flatBranch (ProvedGoals
x : [ProvedGoals]
more) = ProvedGoals
x ProvedGoals -> [ProvedGoals] -> [ProvedGoals]
forall a. a -> [a] -> [a]
: [ProvedGoals] -> [ProvedGoals]
flatBranch [ProvedGoals]
more
flatBranch [] = []
isGoal :: ProvedGoals -> Bool
isGoal ProvedGoals
x = case ProvedGoals
x of
ProvedGoal {} -> Bool
True
NotProvedGoal {} -> Bool
True
Branch{} -> Bool
False
go :: ProvedGoals -> IO [JS]
go ProvedGoals
gs =
case ProvedGoals
gs of
Branch ProvedGoals
g1 ProvedGoals
g2 ->
let ([ProvedGoals]
now,[ProvedGoals]
rest) = (ProvedGoals -> Bool)
-> [ProvedGoals] -> ([ProvedGoals], [ProvedGoals])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition ProvedGoals -> Bool
isGoal ([ProvedGoals] -> [ProvedGoals]
flatBranch [ProvedGoals
g1,ProvedGoals
g2]) in
[JS] -> [JS] -> [JS]
forall a. [a] -> [a] -> [a]
(++) ([JS] -> [JS] -> [JS]) -> IO [JS] -> IO ([JS] -> [JS])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ProvedGoals -> IO [JS]) -> [ProvedGoals] -> IO [JS]
forall {t :: * -> *} {f :: * -> *} {a} {a}.
(Traversable t, Monad f) =>
(a -> f [a]) -> t a -> f [a]
concatMapM ProvedGoals -> IO [JS]
go [ProvedGoals]
now IO ([JS] -> [JS]) -> IO [JS] -> IO [JS]
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (ProvedGoals -> IO [JS]) -> [ProvedGoals] -> IO [JS]
forall {t :: * -> *} {f :: * -> *} {a} {a}.
(Traversable t, Monad f) =>
(a -> f [a]) -> t a -> f [a]
concatMapM ProvedGoals -> IO [JS]
go [ProvedGoals]
rest
ProvedGoal [CrucibleAssumption (Const ())]
asmps SimError
conc [ProgramLoc]
locs Bool
triv
| CruxOptions -> Bool
skipSuccessReports CruxOptions
opts -> [JS] -> IO [JS]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
| Bool
otherwise -> [ProgramLoc]
-> [CrucibleAssumption (Const ())] -> SimError -> Bool -> IO [JS]
jsProvedGoal [ProgramLoc]
locs [CrucibleAssumption (Const ())]
asmps SimError
conc Bool
triv
NotProvedGoal [CrucibleAssumption (Const ())]
asmps SimError
conc Doc Void
explain [ProgramLoc]
locs Maybe (ModelView, [CrucibleEvent GroundValueWrapper])
cex [String]
_
| CruxOptions -> Bool
skipIncompleteReports CruxOptions
opts
, SimError ProgramLoc
_ (ResourceExhausted String
_) <- SimError
conc
-> [JS] -> IO [JS]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
| Bool
otherwise -> [ProgramLoc]
-> [CrucibleAssumption (Const ())]
-> SimError
-> Doc Void
-> Maybe (ModelView, [CrucibleEvent GroundValueWrapper])
-> IO [JS]
jsNotProvedGoal [ProgramLoc]
locs [CrucibleAssumption (Const ())]
asmps SimError
conc Doc Void
explain Maybe (ModelView, [CrucibleEvent GroundValueWrapper])
cex
removeRepeats :: Eq a => [a] -> [a]
removeRepeats :: forall a. Eq a => [a] -> [a]
removeRepeats = (a -> a -> Bool) -> [a] -> [a]
forall a. (a -> a -> Bool) -> [a] -> [a]
removeRepeatsBy a -> a -> Bool
forall a. Eq a => a -> a -> Bool
(==)
removeRepeatsBy :: (a -> a -> Bool) -> [a] -> [a]
removeRepeatsBy :: forall a. (a -> a -> Bool) -> [a] -> [a]
removeRepeatsBy a -> a -> Bool
f = [a] -> [a]
go
where
go :: [a] -> [a]
go [] = []
go [a
x] = [a
x]
go (a
x:a
y:[a]
zs)
| a -> a -> Bool
f a
x a
y = [a] -> [a]
go (a
ya -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
zs)
| Bool
otherwise = a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a] -> [a]
go (a
ya -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
zs)
jsPath :: [ProgramLoc] -> IO [ JS ]
jsPath :: [ProgramLoc] -> IO [JS]
jsPath [ProgramLoc]
locs = [[JS]] -> [JS]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[JS]] -> [JS]) -> IO [[JS]] -> IO [JS]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (([Int], ProgramLoc) -> IO [JS])
-> [([Int], ProgramLoc)] -> IO [[JS]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ([Int], ProgramLoc) -> IO [JS]
forall {a}. Show a => ([a], ProgramLoc) -> IO [JS]
mkStep [([Int], ProgramLoc)]
locs'
where
locs' :: [([Int], ProgramLoc)]
locs' = [ProgramLoc] -> [([Int], ProgramLoc)]
forall a. Ord a => [a] -> [([Int], a)]
annotateLoops ([ProgramLoc] -> [ProgramLoc]
forall a. Eq a => [a] -> [a]
removeRepeats [ProgramLoc]
locs)
mkStep :: ([a], ProgramLoc) -> IO [JS]
mkStep ([a]
a,ProgramLoc
l) =
ProgramLoc -> IO (Maybe JS)
jsLoc ProgramLoc
l IO (Maybe JS) -> (Maybe JS -> IO [JS]) -> IO [JS]
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Maybe JS
Nothing -> [JS] -> IO [JS]
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return []
Just JS
l' ->
[JS] -> IO [JS]
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [[(String, JS)] -> JS
jsObj
[ String
"loop" String -> JS -> (String, JS)
forall a b. a -> b -> (a, b)
~> [JS] -> JS
jsList ((a -> JS) -> [a] -> [JS]
forall a b. (a -> b) -> [a] -> [b]
map a -> JS
forall a. Show a => a -> JS
jsNum [a]
a)
, String
"loc" String -> JS -> (String, JS)
forall a b. a -> b -> (a, b)
~> JS
l'
]]
jsProvedGoal ::
[ ProgramLoc ] ->
[ CrucibleAssumption (Const ()) ] ->
SimError ->
Bool ->
IO [JS]
jsProvedGoal :: [ProgramLoc]
-> [CrucibleAssumption (Const ())] -> SimError -> Bool -> IO [JS]
jsProvedGoal [ProgramLoc]
locs [CrucibleAssumption (Const ())]
asmps SimError
conc Bool
triv =
do JS
loc <- JS -> Maybe JS -> JS
forall a. a -> Maybe a -> a
fromMaybe JS
jsNull (Maybe JS -> JS) -> IO (Maybe JS) -> IO JS
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ProgramLoc -> IO (Maybe JS)
jsLoc (SimError -> ProgramLoc
simErrorLoc SimError
conc)
[JS]
asmps' <- (CrucibleAssumption (Const ()) -> IO JS)
-> [CrucibleAssumption (Const ())] -> IO [JS]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM CrucibleAssumption (Const ()) -> IO JS
forall {e :: BaseType -> *}. CrucibleAssumption e -> IO JS
mkAsmp [CrucibleAssumption (Const ())]
asmps
[JS]
path <- [ProgramLoc] -> IO [JS]
jsPath [ProgramLoc]
locs
[JS] -> IO [JS]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [[(String, JS)] -> JS
jsObj
[ String
"status" String -> JS -> (String, JS)
forall a b. a -> b -> (a, b)
~> String -> JS
jsStr String
"ok"
, String
"goal" String -> JS -> (String, JS)
forall a b. a -> b -> (a, b)
~> JS
goalReason
, String
"details-short" String -> JS -> (String, JS)
forall a b. a -> b -> (a, b)
~> JS
goalDetails
, String
"location" String -> JS -> (String, JS)
forall a b. a -> b -> (a, b)
~> JS
loc
, String
"assumptions" String -> JS -> (String, JS)
forall a b. a -> b -> (a, b)
~> [JS] -> JS
jsList [JS]
asmps'
, String
"trivial" String -> JS -> (String, JS)
forall a b. a -> b -> (a, b)
~> Bool -> JS
jsBool Bool
triv
, String
"path" String -> JS -> (String, JS)
forall a b. a -> b -> (a, b)
~> [JS] -> JS
jsList [JS]
path
]]
where
mkAsmp :: CrucibleAssumption e -> IO JS
mkAsmp CrucibleAssumption e
asmp =
do JS
l <- JS -> Maybe JS -> JS
forall a. a -> Maybe a -> a
fromMaybe JS
jsNull (Maybe JS -> JS) -> IO (Maybe JS) -> IO JS
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ProgramLoc -> IO (Maybe JS)
jsLoc (CrucibleAssumption e -> ProgramLoc
forall (e :: BaseType -> *). CrucibleAssumption e -> ProgramLoc
assumptionLoc CrucibleAssumption e
asmp)
JS -> IO JS
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (JS -> IO JS) -> JS -> IO JS
forall a b. (a -> b) -> a -> b
$ [(String, JS)] -> JS
jsObj
[ String
"loc" String -> JS -> (String, JS)
forall a b. a -> b -> (a, b)
~> JS
l
, String
"text" String -> JS -> (String, JS)
forall a b. a -> b -> (a, b)
~> String -> JS
jsStr (Doc Any -> String
forall a. Show a => a -> String
show ((forall (tp :: BaseType). e tp -> Doc Any)
-> CrucibleAssumption e -> Doc Any
forall (e :: BaseType -> *) ann.
(forall (tp :: BaseType). e tp -> Doc ann)
-> CrucibleAssumption e -> Doc ann
ppAssumption (\e tp
_ -> Doc Any
forall a. Monoid a => a
mempty) CrucibleAssumption e
asmp))
]
goalReason :: JS
goalReason = String -> JS
jsStr (SimErrorReason -> String
simErrorReasonMsg (SimError -> SimErrorReason
simErrorReason SimError
conc))
goalDetails :: JS
goalDetails
| String -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
msg = JS
jsNull
| Bool
otherwise = String -> JS
jsStr String
msg
where msg :: String
msg = SimErrorReason -> String
simErrorDetailsMsg (SimError -> SimErrorReason
simErrorReason SimError
conc)
jsNotProvedGoal ::
[ ProgramLoc ] ->
[ CrucibleAssumption (Const ()) ] ->
SimError ->
Doc Void ->
Maybe (ModelView, [CrucibleEvent GroundValueWrapper]) ->
IO [JS]
jsNotProvedGoal :: [ProgramLoc]
-> [CrucibleAssumption (Const ())]
-> SimError
-> Doc Void
-> Maybe (ModelView, [CrucibleEvent GroundValueWrapper])
-> IO [JS]
jsNotProvedGoal [ProgramLoc]
locs [CrucibleAssumption (Const ())]
asmps SimError
conc Doc Void
explain Maybe (ModelView, [CrucibleEvent GroundValueWrapper])
cex =
do JS
loc <- JS -> Maybe JS -> JS
forall a. a -> Maybe a -> a
fromMaybe JS
jsNull (Maybe JS -> JS) -> IO (Maybe JS) -> IO JS
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ProgramLoc -> IO (Maybe JS)
jsLoc (SimError -> ProgramLoc
simErrorLoc SimError
conc)
[JS]
asmps' <- (CrucibleAssumption (Const ()) -> IO JS)
-> [CrucibleAssumption (Const ())] -> IO [JS]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM CrucibleAssumption (Const ()) -> IO JS
forall {e :: BaseType -> *}. CrucibleAssumption e -> IO JS
mkAsmp [CrucibleAssumption (Const ())]
asmps
JS
ex <- case Maybe (ModelView, [CrucibleEvent GroundValueWrapper])
cex of
Just (ModelView
m,[CrucibleEvent GroundValueWrapper]
_) -> ModelView -> IO JS
modelJS ModelView
m
Maybe (ModelView, [CrucibleEvent GroundValueWrapper])
_ -> JS -> IO JS
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure JS
jsNull
[JS]
path <- [ProgramLoc] -> IO [JS]
jsPath [ProgramLoc]
locs
[JS] -> IO [JS]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [[(String, JS)] -> JS
jsObj
[ String
"status" String -> JS -> (String, JS)
forall a b. a -> b -> (a, b)
~> JS
status
, String
"counter-example" String -> JS -> (String, JS)
forall a b. a -> b -> (a, b)
~> JS
ex
, String
"goal" String -> JS -> (String, JS)
forall a b. a -> b -> (a, b)
~> JS
goalReason
, String
"details-short" String -> JS -> (String, JS)
forall a b. a -> b -> (a, b)
~> JS
goalDetails
, String
"location" String -> JS -> (String, JS)
forall a b. a -> b -> (a, b)
~> JS
loc
, String
"assumptions" String -> JS -> (String, JS)
forall a b. a -> b -> (a, b)
~> [JS] -> JS
jsList [JS]
asmps'
, String
"trivial" String -> JS -> (String, JS)
forall a b. a -> b -> (a, b)
~> Bool -> JS
jsBool Bool
False
, String
"path" String -> JS -> (String, JS)
forall a b. a -> b -> (a, b)
~> [JS] -> JS
jsList [JS]
path
, String
"details-long" String -> JS -> (String, JS)
forall a b. a -> b -> (a, b)
~> String -> JS
jsStr (Doc Void -> String
forall a. Show a => a -> String
show Doc Void
explain)
]]
where
status :: JS
status = case Maybe (ModelView, [CrucibleEvent GroundValueWrapper])
cex of
Just (ModelView, [CrucibleEvent GroundValueWrapper])
_
| ResourceExhausted String
_ <- SimError -> SimErrorReason
simErrorReason SimError
conc -> String -> JS
jsStr String
"unknown"
| Bool
otherwise -> String -> JS
jsStr String
"fail"
Maybe (ModelView, [CrucibleEvent GroundValueWrapper])
Nothing -> String -> JS
jsStr String
"unknown"
mkAsmp :: CrucibleAssumption e -> IO JS
mkAsmp CrucibleAssumption e
asmp =
do JS
l <- JS -> Maybe JS -> JS
forall a. a -> Maybe a -> a
fromMaybe JS
jsNull (Maybe JS -> JS) -> IO (Maybe JS) -> IO JS
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ProgramLoc -> IO (Maybe JS)
jsLoc (CrucibleAssumption e -> ProgramLoc
forall (e :: BaseType -> *). CrucibleAssumption e -> ProgramLoc
assumptionLoc CrucibleAssumption e
asmp)
JS -> IO JS
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (JS -> IO JS) -> JS -> IO JS
forall a b. (a -> b) -> a -> b
$ [(String, JS)] -> JS
jsObj
[ String
"loc" String -> JS -> (String, JS)
forall a b. a -> b -> (a, b)
~> JS
l
, String
"text" String -> JS -> (String, JS)
forall a b. a -> b -> (a, b)
~> String -> JS
jsStr (Doc Any -> String
forall a. Show a => a -> String
show ((forall (tp :: BaseType). e tp -> Doc Any)
-> CrucibleAssumption e -> Doc Any
forall (e :: BaseType -> *) ann.
(forall (tp :: BaseType). e tp -> Doc ann)
-> CrucibleAssumption e -> Doc ann
ppAssumption (\e tp
_ -> Doc Any
forall a. Monoid a => a
mempty) CrucibleAssumption e
asmp))
]
goalReason :: JS
goalReason = String -> JS
jsStr (SimErrorReason -> String
simErrorReasonMsg (SimError -> SimErrorReason
simErrorReason SimError
conc))
goalDetails :: JS
goalDetails
| String -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
msg = JS
jsNull
| Bool
otherwise = String -> JS
jsStr String
msg
where msg :: String
msg = SimErrorReason -> String
simErrorDetailsMsg (SimError -> SimErrorReason
simErrorReason SimError
conc)