Rip out most of the guts of the build-sandbox.sh script, and replace

it with use of submodules instead.

Update README and project build metadata to include new packages.

.gitignore

@@ -1,6 +1,4 @@
 /build/
-/dependencies/
-/dependencies
 .cabal-sandbox
 .stack-work
 **/cabal.config

.gitmodules

@@ -0,0 +1,56 @@
+[submodule "dependencies/abcBridge"]
+ path = dependencies/abcBridge
+ url = [email protected]:GaloisInc/abcBridge.git
+ branch = master
+[submodule "dependencies/aig"]
+ path = dependencies/aig
+ url = [email protected]:GaloisInc/aig.git
+ branch = master
+[submodule "dependencies/blt"]
+ path = dependencies/blt
+ url = [email protected]:GaloisInc/blt.git
+ branch = master
+[submodule "dependencies/cryptol"]
+ path = dependencies/cryptol
+ url = [email protected]:GaloisInc/cryptol.git
+ branch = master
+[submodule "dependencies/cryptol-verifier"]
+ path = dependencies/cryptol-verifier
+ url = [email protected]:GaloisInc/cryptol-verifier.git
+ branch = master
+[submodule "dependencies/jvm-parser"]
+ path = dependencies/jvm-parser
+ url = [email protected]:GaloisInc/jvm-parser.git
+ branch = master
+[submodule "dependencies/llvm-pretty"]
+ path = dependencies/llvm-pretty
+ url = [email protected]:elliottt/llvm-pretty.git
+ branch = master
+[submodule "dependencies/llvm-pretty-bc-parser"]
+ path = dependencies/llvm-pretty-bc-parser
+ url = [email protected]:GaloisInc/llvm-pretty-bc-parser.git
+ branch = master
+[submodule "dependencies/hpb"]
+ path = dependencies/hpb
+ url = [email protected]:GaloisInc/hpb.git
+ branch = master
+[submodule "dependencies/parameterized-utils"]
+ path = dependencies/parameterized-utils
+ url = [email protected]:GaloisInc/parameterized-utils.git
+ branch = master
+[submodule "dependencies/saw-core"]
+ path = dependencies/saw-core
+ url = [email protected]:GaloisInc/saw-core.git
+ branch = master
+[submodule "dependencies/saw-core-aig"]
+ path = dependencies/saw-core-aig
+ url = [email protected]:GaloisInc/saw-core-aig.git
+ branch = master
+[submodule "dependencies/saw-core-sbv"]
+ path = dependencies/saw-core-sbv
+ url = [email protected]:GaloisInc/saw-core-sbv.git
+ branch = master
+[submodule "dependencies/saw-core-what4"]
+ path = dependencies/saw-core-what4
+ url = [email protected]:GaloisInc/saw-core-what4.git
+ branch = master

README.md

@@ -35,6 +35,20 @@ Currently, the repository consists of the following Haskell packages:
  executing JVM bytecode programs in the Crucible symbolic simulator.
  * **`crucible-saw`** provides functionality for generating
  SAW Core terms from Crucible Control-Flow-Graphs.
+ * **`crucible-syntax`** provides a native SExpression based concrete
+ syntax for crucible programs. It is useful for being able to
+ directly interact with the core Crucible simulator without bringing
+ in issues related to the translation of other front-ends (e.g. the
+ LLVM translation). It is primarily intended for the purpose of
+ writing test cases.
+ * **`crux`** provides common support libraries for running the
+ crucible simulator in a basic "all-at-once" use mode for simulation
+ and verification. This includes most of the setup steps required
+ to actually set the simulator off and running, as well as
+ functionality for collecting and discharging safety conditions and
+ generated assertions via solvers. Both the `crucible-c` and `crucible-jvm`
+ executables are thin wrappers around the functionality provided
+ by `crux`.
 
 In addition, there are the following library/executable packages:
 
@@ -47,6 +61,10 @@ In addition, there are the following library/executable packages:
 
 [sv-comp]: https://sv-comp.sosy-lab.org
 
+ * **`crucible-jvm`**, also contains an executable for directly
+ running compiled JVM bytecode programs, in a similar vein
+ to the `crucible-c` package.
+
  * **`crucible-server`**, a standalone process that allows constructing
  and symbolically executing Crucible programs via [Protocol Buffers][pb].
  The crucible-server directory also contains a Java API for
@@ -66,20 +84,12 @@ directory for details).
 
 Quick start
 -------------
-
-Crucible is mainly intended to be used as a library for other
-downstream projects. As such, the build system infrastructure in this
-repository is relatively minimal. Downstream projects are expected to
-do the primary work of tracking dependencies, and maintaining a
-coherent working set of git submodules, etc.
-
-However, for convenience, we provide here some basic support for
-building crucible in place.
-
 To fetch all the latest git versions of immediate dependencies of
 libraries in this repository, use the `scripts/build-sandbox.sh` shell
-script. You will find it most convenient to setup public-key login
-for GitHub before you perform this step.
+script; alternately, you can manually invoke the git commands to
+initialize and recursively update submodules. You will find it most
+convenient to setup public-key login for GitHub before you perform
+this step.
 
 Now, you may use either `stack` or `cabal new-build` to compile the
 libraries, as you prefer.
@@ -97,6 +107,8 @@ cabal new-configure
 cabal new-build all
 ```
 
+Alternately, you can target a more specific sub-packge instead of `all`.
+
 If you wish to build `crucible-server` (which will be built if you
 build all packages, as above), then the build depends on having `hpb`
 in your path. After fetching the dependencies, this can be arranged by

cabal.project

@@ -10,11 +10,11 @@ packages:
  what4-blt/
 
  crucible/
+ crucible-c/
  crucible-jvm/
  crucible-llvm/
  crucible-saw/
  crucible-server/
- crucible-c/
  crucible-syntax/
  crux/
 

scripts/build-sandbox.sh

@@ -1,73 +1,4 @@
 #!/bin/bash
-#
-# This script checks out the repos needed to build crucible libraries and the crucible-server.
-#
-# This script only requires git to run, but crucible has the following prerequites:
-#
-# * stack
-# - https://github.com/commercialhaskell/stack/wiki/Downloads
-#
-# * Libraries & Utils: pkg-config, libzmq, NTL, GLPK, Boost
-# - to install NTL, GLPK, and Boost easily, see:
-# https://github.com/GaloisInc/blt/blob/master/bootstrap.sh
-# - to install pkg-config and libzmq on Debian/Ubuntu, do:
-# $ sudo apt-get install pkg-config libzmq3 libzmq3-dev
-#
-# * GHC >= 7.10 (Optional)
-# - https://www.haskell.org/ghc/download
-#
-# Installation:
-#
-# Execute this script from the top level of the `crucible-public` source repo.
-# This will checkout all needed Galois dependencies in `$PWD/dependencies`.
-#
-# Options:
-#
-# Set $NO_GIT_PULL if you do not want to 'git pull' in pre-existing dependency repos.
-#
 
-set -e
-
-checkout () {
- local url=$1 # File to unpack
- local pkg=$2
- if [ ! -d "dependencies/$pkg" ]; then
- pushd dependencies > /dev/null
- git clone "$url"
- if [ $? -ne 0 ]; then
- echo "\n\nFailed to clone private GitHub repos. Please check your \
- ssh keys to make sure you are authorized for the Galois GitHub \
- account"
- exit 1
- fi
- popd > /dev/null
- elif [ -z "${NO_GIT_PULL}" ]; then
- echo "Pulling from $pkg"
- pushd "dependencies/$pkg" > /dev/null
- git pull
- popd > /dev/null
- fi
-}
-
-# GitHub repos (some private, some public) required by the build
-PKG_LIST="GaloisInc/abcBridge GaloisInc/aig GaloisInc/blt \
- GaloisInc/saw-core GaloisInc/saw-core-aig GaloisInc/saw-core-sbv \
- GaloisInc/saw-core-what4 \
- GaloisInc/hpb elliottt/llvm-pretty \
- GaloisInc/jvm-parser \
- GaloisInc/cryptol GaloisInc/cryptol-verifier \
- elliottt/llvm-pretty \
- GaloisInc/llvm-pretty-bc-parser GaloisInc/parameterized-utils"
-
-# Set base GitHub URL for Galois repos if it's not already set
-: ${GITHUB_URL:="[email protected]:"}
-echo "Using github url: $GITHUB_URL"
-
-if [ ! -d "dependencies" ]; then
- mkdir -p "dependencies"
-fi
-
-# Download GitHub repos
-for pkg in $PKG_LIST; do
- checkout "$GITHUB_URL$pkg.git" ${pkg#*/}
-done
+git submodule init
+git submodule update --recursive

stack.yaml

@@ -5,11 +5,13 @@ packages:
  - what4-blt/
 
  - crucible/
+ - crucible-c/
  - crucible-jvm/
  - crucible-llvm/
  - crucible-saw/
  - crucible-server/
- - crucible-c/
+ - crucible-syntax/
+ - crux/
 
  - dependencies/abcBridge/
  - dependencies/aig/