-- from: crucible-c/src/Report.hs

{-# 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 )

-- Note these should be data files. However, cabal-new build doesn't make it easy for the installation
-- to find data files, so they are embedded as Text constants instead.

import Crux.UI.JS
import Crux.UI.Jquery (jquery)       -- ui/jquery.min.js
import Crux.UI.IndexHtml (indexHtml) -- ui/index.html


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)
       -- Due to CORS restrictions, the only current way of statically loading local data
       -- is by including a <script> with the contents we want.
       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
       -- However, for some purposes, having a JSON file is more practical.
       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


-- TODO: get the extensions from the Language configuration
-- XXX: currently we just use the file name as a label for the file,
-- but if files come from different directores this may lead to clashes,
-- so we should do something smarter (e.g., drop only the prefix that
-- is common to all files).
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 ()


-- | Return a list of all program locations referenced in a set of
-- proved goals.
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

-- | Return a list of all of the traces referenced in a set of proved goals.
--
-- This returns a sequence-of-sequences because a single 'ProvedGoals' can
-- involve many 'Branch'es, which mirror the branching structure of the program
-- execution that led to each individual 'ProvedGoal' or 'NotProvedGoal'.
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)

-- | Return a list of all files referenced in a set of proved goals.
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)