Skip to content

Commit

Permalink
Merge branch 'main' into _update-deps/runtimeverification/k
Browse files Browse the repository at this point in the history
  • Loading branch information
@rv-jenkins
rv-jenkins authored Mar 21, 2024
2 parents 38c6c5e + d090886 commit 279e6a9
Show file tree
Hide file tree
Showing 29 changed files with 10,982 additions and 515 deletions.
2 changes: 1 addition & 1 deletion cabal.project
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ packages:
source-repository-package
type: git
location: https://github.com/runtimeverification/haskell-backend.git
tag: 4d5d1fe232c41400e09a2db0d8cb4989a5dd5832
tag: 093af3153a5e07626d9b2e628d7ad4fc77c5a723
subdir: kore kore-rpc-types

source-repository-package
Expand Down
73 changes: 2 additions & 71 deletions cabal.project.freeze
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,24 +6,16 @@ constraints: any.Cabal ==3.10.1.0,
any.OneTuple ==0.4.1.1,
any.Only ==0.1,
any.QuickCheck ==2.14.3,
QuickCheck -old-random +templatehaskell,
any.StateVar ==1.2.2,
any.adjunctions ==4.4.2,
any.aeson ==2.1.2.1,
aeson -cffi +ordered-keymap,
any.aeson-pretty ==0.8.10,
aeson-pretty -lib-only,
any.ansi-terminal ==1.0.2,
ansi-terminal -example,
any.ansi-terminal-types ==0.11.5,
any.array ==0.5.6.0,
any.assoc ==1.1,
assoc +tagged,
any.async ==2.2.5,
async -bench,
any.attoparsec ==0.14.4,
attoparsec -developer,
any.attoparsec-aeson ==2.1.0.0,
any.auto-update ==0.1.6,
any.barbies ==2.0.5.0,
any.base ==4.18.2.0,
Expand All @@ -33,57 +25,39 @@ constraints: any.Cabal ==3.10.1.0,
any.base16 ==1.0,
any.basement ==0.0.16,
any.bifunctors ==5.6.1,
bifunctors +tagged,
any.binary ==0.8.9.1,
any.bitvec ==1.1.5.0,
bitvec +simd,
any.blaze-builder ==0.4.2.3,
any.blaze-html ==0.9.1.2,
any.blaze-markup ==0.8.3.0,
any.blaze-textual ==0.2.3.1,
blaze-textual -developer -integer-simple +native,
any.boring ==0.2.1,
boring +tagged,
any.bytebuild ==0.3.16.2,
bytebuild -checked,
any.byteslice ==0.2.13.2,
byteslice +avoid-rawmemchr,
any.bytesmith ==0.3.11.0,
any.bytestring ==0.11.5.3,
any.bz2 ==1.0.1.0,
bz2 -cross +with-bzlib,
any.c2hs ==0.28.8,
c2hs +base3 -regression,
any.cabal-doctest ==1.0.9,
any.call-stack ==0.4.0,
any.case-insensitive ==1.2.1.0,
any.casing ==0.1.4.1,
any.cereal ==0.5.8.3,
cereal -bytestring-builder,
any.cereal-conduit ==0.8.0,
any.chronos ==1.1.6.0,
any.clock ==0.8.4,
clock -llvm,
any.cmdargs ==0.10.22,
cmdargs +quotation -testprog,
any.co-log ==0.6.0.2,
co-log -tutorial,
any.co-log-core ==0.3.2.1,
any.colour ==2.3.6,
any.comonad ==5.0.8,
comonad +containers +distributive +indexed-traversable,
any.concurrent-output ==1.10.20,
any.conduit ==1.3.5,
any.conduit-extra ==1.3.6,
any.constraints ==0.14,
any.constraints-extras ==0.4.0.0,
constraints-extras +build-readme,
any.containers ==0.6.7,
any.contiguous ==0.6.4.2,
any.contravariant ==1.5.5,
contravariant +semigroups +statevar +tagged,
any.cryptonite ==0.30,
cryptonite -check_alignment +integer-gmp -old_toolchain_inliner +support_aesni +support_deepseq -support_pclmuldq +support_rdrand -support_sse +use_target_attributes,
any.data-default ==0.7.1.1,
any.data-default-class ==0.1.2.0,
any.data-default-instances-containers ==0.0.1,
Expand All @@ -96,22 +70,17 @@ constraints: any.Cabal ==3.10.1.0,
any.dependent-sum ==0.7.2.0,
any.deriving-aeson ==0.2.9,
any.direct-sqlite ==2.3.29,
direct-sqlite +dbstat +fulltextsearch +haveusleep +json1 -mathfunctions -systemlib +urifilenames,
any.directory ==1.3.8.1,
any.distributive ==0.6.2.1,
distributive +semigroups +tagged,
any.dlist ==1.0,
dlist -werror,
any.easy-file ==0.2.5,
any.entropy ==0.4.1.10,
entropy -donotgetentropy,
any.erf ==2.0.0.0,
any.errors ==2.3.0,
any.exceptions ==0.10.7,
any.extra ==1.7.14,
any.fast-logger ==3.2.2,
any.fgl ==5.8.2.0,
fgl +containers042,
any.filepath ==1.4.200.1,
any.free ==5.2,
any.generic-lens ==2.2.2.0,
Expand All @@ -125,11 +94,8 @@ constraints: any.Cabal ==3.10.1.0,
any.ghc-trace-events ==0.1.2.8,
any.gitrev ==1.3.1,
any.graphviz ==2999.20.2.0,
graphviz -test-parsing,
any.hashable ==1.4.2.0,
hashable +integer-gmp -random-initial-seed,
any.hashtables ==1.3.1,
hashtables -bounds-checking -debug -detailed-profiling -portable -sse42 +unsafe-tricks,
any.haskeline ==0.8.2.1,
any.haskell-lexer ==1.1.1,
any.haskell-src-exts ==1.23.1,
Expand All @@ -149,7 +115,6 @@ constraints: any.Cabal ==3.10.1.0,
any.indexed-traversable-instances ==0.1.1.2,
any.integer-gmp ==1.1,
any.integer-logarithms ==1.0.3.1,
integer-logarithms -check-bounds +integer-gmp,
any.intern ==0.9.5,
any.invariant ==0.6.2,
any.json-rpc ==1.0.4,
Expand All @@ -159,51 +124,39 @@ constraints: any.Cabal ==3.10.1.0,
kore +threaded,
any.kore-rpc-types ==0.60.0.0,
any.language-c ==0.9.3,
language-c -allwarnings +iecfpextension +usebytestrings,
any.lens ==5.2.3,
lens -benchmark-uniplate -dump-splices +inlining -j +test-hunit +test-properties +test-templates +trustworthy,
any.libyaml ==0.1.2,
libyaml -no-unicode -system-libyaml,
any.lifted-async ==0.10.2.5,
any.lifted-base ==0.2.3.12,
any.logict ==0.8.1.0,
any.loop ==0.3.0,
any.math-functions ==0.3.4.3,
math-functions +system-erf +system-expm1,
any.matrix ==0.3.6.3,
any.megaparsec ==9.5.0,
megaparsec -dev,
any.memory ==0.18.0,
memory +support_bytestring +support_deepseq,
any.mmorph ==1.2.0,
any.monad-control ==1.0.3.1,
any.monad-logger ==0.3.40,
monad-logger +template_haskell,
any.monad-loops ==0.4.3,
monad-loops +base4,
any.monad-validate ==1.3.0.0,
any.mono-traversable ==1.0.15.3,
any.mtl ==2.3.1,
any.multiset ==0.3.4.3,
any.mwc-random ==0.15.0.2,
any.natural-arithmetic ==0.1.4.0,
any.network ==3.1.4.0,
network -devel,
any.network-run ==0.2.6,
any.old-locale ==1.0.0.7,
any.old-time ==1.1.0.4,
any.optparse-applicative ==0.18.1.0,
optparse-applicative +process,
any.parallel ==3.2.2.0,
any.parsec ==3.1.16.1,
any.parser-combinators ==1.3.0,
parser-combinators -dev,
any.polyparse ==1.13,
any.pqueue ==1.5.0.0,
any.pretty ==1.1.3.6,
any.pretty-show ==1.10,
any.prettyprinter ==1.7.1,
prettyprinter -buildreadme +text,
any.prettyprinter-ansi-terminal ==1.1.3,
any.primitive ==0.8.0.0,
any.primitive-addr ==0.1.0.2,
Expand All @@ -214,9 +167,7 @@ constraints: any.Cabal ==3.10.1.0,
any.quickcheck-io ==0.2.0,
any.random ==1.2.1.2,
any.recursion-schemes ==5.2.2.5,
recursion-schemes +template-haskell,
any.reflection ==2.1.7,
reflection -slow +template-haskell,
any.regex-base ==0.94.0.2,
any.regex-pcre-builtin ==0.95.2.3.8.44,
any.resourcet ==1.3.0,
Expand All @@ -225,37 +176,28 @@ constraints: any.Cabal ==3.10.1.0,
any.safe ==0.3.21,
any.safe-exceptions ==0.1.7.4,
any.scientific ==0.3.7.0,
scientific -bytestring-builder -integer-simple,
any.secp256k1-haskell ==1.1.0,
any.semialign ==1.3,
semialign +semigroupoids,
any.semigroupoids ==6.0.0.1,
semigroupoids +comonad +containers +contravariant +distributive +tagged +unordered-containers,
any.semigroups ==0.20,
semigroups +binary +bytestring -bytestring-builder +containers +deepseq +hashable +tagged +template-haskell +text +transformers +unordered-containers,
any.smallcheck ==1.2.1.1,
any.smtlib-backends ==0.3,
any.smtlib-backends-process ==0.3,
any.some ==1.0.6,
some +newtype-unsafe,
any.sop-core ==0.5.0.2,
any.split ==0.2.5,
any.splitmix ==0.1.0.5,
splitmix -optimised-mixer,
any.sqlite-simple ==0.4.19.0,
any.stm ==2.5.1.0,
any.stm-chans ==3.0.0.9,
any.stm-conduit ==4.0.1,
any.streaming-commons ==0.2.2.6,
streaming-commons -use-bytestring-builder,
any.streams ==3.3.2,
any.strict ==0.5,
any.string-conversions ==0.4.0.1,
any.syb ==0.7.2.4,
any.tagged ==0.8.8,
tagged +deepseq +transformers,
any.tar ==0.5.1.1,
tar -old-bytestring -old-time,
any.tasty ==1.4.3,
tasty +unix,
any.tasty-discover ==5.0.0,
Expand All @@ -273,7 +215,6 @@ constraints: any.Cabal ==3.10.1.0,
any.terminfo ==0.4.1.6,
any.text ==2.0.2,
any.text-short ==0.1.5,
text-short -asserts,
any.tf-random ==0.5,
any.th-abstraction ==0.5.0.0,
any.th-compat ==0.1.4,
Expand All @@ -284,43 +225,33 @@ constraints: any.Cabal ==3.10.1.0,
any.these ==1.2,
any.time ==1.12.2,
any.time-compat ==1.9.6.1,
time-compat -old-locale,
any.time-manager ==0.0.1,
any.torsor ==0.1.0.1,
any.transformers ==0.6.1.0,
any.transformers-base ==0.4.6,
transformers-base +orphaninstances,
any.transformers-compat ==0.7.2,
transformers-compat -five +five-three -four +generic-deriving +mtl -three -two,
any.tuples ==0.1.0.0,
any.type-equality ==1,
any.typed-process ==0.2.11.1,
any.unix ==2.8.4.0,
any.unix-compat ==0.7.1,
unix-compat -old-time,
any.unix-time ==0.4.12,
any.unliftio ==0.2.25.0,
any.unliftio-core ==0.2.1.0,
any.unordered-containers ==0.2.20,
unordered-containers -debug,
any.utf8-string ==1.0.2,
any.uuid-types ==1.0.5.1,
any.vector ==0.13.1.0,
vector +boundschecks -internalchecks -unsafechecks -wall,
any.vector-algorithms ==0.9.0.1,
vector-algorithms +bench +boundschecks -internalchecks -llvm +properties -unsafechecks,
any.vector-stream ==0.1.0.1,
any.void ==0.7.3,
void -safe,
any.wide-word ==0.1.6.0,
any.witherable ==0.4.2,
any.wl-pprint-annotated ==0.1.0.1,
any.wl-pprint-text ==1.2.0.2,
any.xml-conduit ==1.9.1.3,
any.xml-types ==0.3.8,
any.yaml ==0.11.11.2,
yaml +no-examples +no-exe,
any.zigzag ==0.0.1.0,
any.zlib ==0.6.3.0,
zlib -bundled-c-zlib -non-blocking-ffi -pkg-config
index-state: hackage.haskell.org 2024-02-26T02:47:27Z
any.zlib ==0.6.3.0
index-state: hackage.haskell.org 2024-02-29T08:06:57Z
2 changes: 1 addition & 1 deletion deps/haskell-backend_release
View file
Original file line number Diff line number Diff line change
@@ -1 +1 @@
4d5d1fe232c41400e09a2db0d8cb4989a5dd5832
093af3153a5e07626d9b2e628d7ad4fc77c5a723
21 changes: 16 additions & 5 deletions dev-tools/booster-dev/Server.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ License : BSD-3-Clause
-}
module Main (main) where

import Booster.Util (runHandleLoggingT)
import Booster.Util (runHandleLoggingT, withLogFile)
import Control.Concurrent (newMVar)
import Control.DeepSeq (force)
import Control.Exception (evaluate)
Expand All @@ -15,7 +15,7 @@ import Control.Monad.Logger.CallStack (LogLevel (LevelError))
import Data.Conduit.Network (serverSettings)
import Data.Map (Map)
import Data.Map.Strict qualified as Map
import Data.Maybe (isNothing)
import Data.Maybe (fromMaybe, isNothing)
import Data.Text (Text, unpack)
import Options.Applicative
import System.IO qualified as IO
Expand Down Expand Up @@ -45,6 +45,7 @@ main = do
, smtOptions
, equationOptions
, eventlogEnabledUserEvents
, simplificationLogFile
} = options

forM_ eventlogEnabledUserEvents $ \t -> do
Expand All @@ -55,7 +56,8 @@ main = do
<> definitionFile
<> ", main module "
<> show mainModuleName
withLlvmLib llvmLibraryFile $ \mLlvmLibrary -> do

withLogFile simplificationLogFile $ \mLogFileHandle -> withLlvmLib llvmLibraryFile $ \mLlvmLibrary -> do
definitionMap <-
loadDefinition definitionFile
>>= mapM (mapM ((fst <$>) . runNoLoggingT . computeCeilsDefinition mLlvmLibrary))
Expand All @@ -68,7 +70,14 @@ main = do
writeGlobalEquationOptions equationOptions

putStrLn "Starting RPC server"
runServer port definitionMap mainModuleName mLlvmLibrary smtOptions (adjustLogLevels logLevels)
runServer
port
definitionMap
mainModuleName
mLlvmLibrary
mLogFileHandle
smtOptions
(adjustLogLevels logLevels)
where
withLlvmLib libFile m = case libFile of
Nothing -> m Nothing
Expand All @@ -92,12 +101,14 @@ runServer ::
Map Text KoreDefinition ->
Text ->
Maybe LLVM.API ->
Maybe IO.Handle ->
Maybe SMT.SMTOptions ->
(LogLevel, [LogLevel]) ->
IO ()
runServer port definitions defaultMain mLlvmLibrary mSMTOptions (logLevel, customLevels) =
runServer port definitions defaultMain mLlvmLibrary mLogFileHandle mSMTOptions (logLevel, customLevels) =
do
let logLevelToHandle = \case
Log.LevelOther "SimplifyJson" -> fromMaybe IO.stderr mLogFileHandle
_ -> IO.stderr

stateVar <-
Expand Down
26 changes: 21 additions & 5 deletions dev-tools/pretty/Pretty.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,10 @@ module Main (
import Booster.Prettyprinter (renderDefault)
import Booster.Syntax.Json (KoreJson (..))
import Booster.Syntax.Json.Internalise (
InternalisedPredicates (..),
PatternError (..),
internalisePattern,
internalisePredicates,
pattern CheckSubsorts,
pattern DisallowAlias,
)
Expand All @@ -35,8 +38,21 @@ main = do
case eitherDecode fileContent of
Left err -> putStrLn $ "Error: " ++ err
Right KoreJson{term} -> do
let (trm, _subst, _unsupported) =
either (error . show) id $
runExcept $
internalisePattern DisallowAlias CheckSubsorts Nothing internalDef term
putStrLn $ renderDefault $ pretty trm
case runExcept $ internalisePattern DisallowAlias CheckSubsorts Nothing internalDef term of
Right (trm, _subst, _unsupported) -> do
putStrLn "Pretty-printing pattern: "
putStrLn $ renderDefault $ pretty trm
Left (NoTermFound _) ->
case runExcept $ internalisePredicates DisallowAlias CheckSubsorts Nothing internalDef [term] of
Left es -> error (show es)
Right ts -> do
putStrLn "Pretty-printing predicates: "
putStrLn "Bool predicates: "
mapM_ (putStrLn . renderDefault . pretty) ts.boolPredicates
putStrLn "Ceil predicates: "
mapM_ (putStrLn . renderDefault . pretty) ts.ceilPredicates
putStrLn "Substitution: "
mapM_ (putStrLn . renderDefault . pretty) ts.substitution
putStrLn "Unsupported predicates: "
mapM_ print ts.unsupported
Left err -> error (show err)
Loading

0 comments on commit 279e6a9

Please sign in to comment.