Initial commit of project structure

.gitignore

@@ -0,0 +1,11 @@
+/build/
+/dependencies/
+.cabal-sandbox
+.stack-work
+**/cabal.config
+cabal.sandbox.config
+dist
+TAGS
+unitTest.tix
+hpc_report
+stack.yaml

README.md

@@ -0,0 +1,42 @@
+This `git` repo contains the source code for crucible and the crucible server
+
+ * **`crucible-server`**, a standalone process that allows constructing
+ and symbolically executing Crucible programs via a [Protocol Buffers][pb].
+
+[pb]: https://developers.google.com/protocol-buffers/ "Protocol Buffers"
+
+Crucible has been designed as a set of Haskell packages organized so that Crucible
+itself has a minimal number of external dependencies, and functionality
+independent of crucible can be separated into sub-libraries.
+
+Currently, the repo consists of the following Haskell packages:
+
+ * **`crucible`** provides the core Crucible definitions, the
+ symbolic simulator, the `SimpleBackend` formula representation, interfaces
+ between `SimpleBackend` and SMT solvers, and LLVM and MATLAB to
+ Crucible translators.
+ * **`crucible-abc`** provides functionality for generating
+ ABC networks from `SimpleBackend` expressions.
+ * **`crucible-blt`** provides functionality for generating
+ BLT problems from `SimpleBackend` expressions.
+ * **`crucible-saw`** provides functionality for generating
+ SAW Core terms from Crucible Control-Flow-Graphs.
+ * **`crucible-server`** provides the `crucible-server` binary, and
+ also contains a Java API for working with `crucible-server`.
+ * **`galois-matlab`** provides a few data structures for working with
+ MATLAB values.
+
+For developing `crucible`, this repo follows a workflow similar to the
+[Gitflow][gitflow] workflow model.
+
+[gitflow]: http:https://nvie.com/posts/a-successful-git-branching-model/ "Gitflow Model"
+
+The current development version is in the `develop` branch, and major feature
+development should occur in branches of `develop` that are prefixed with
+initials identifying the main author of the feature (e.g., `jhx-symbolic-fn`).
+Minor fixes can occur directly on `develop`, but an effort should be made to
+ensure that develop always builds.
+
+To use `stack` to build crucible, you can use the shell script
+`scripts/build-sandbox.sh` to retrieve the appropriate repos for
+building.

scripts/build-sandbox.sh

@@ -0,0 +1,83 @@
+#!/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 `crucible-public` source repo. This will checkout all needed
+# Galois dependencies in `$PWD/dependencies` and execute a build.
+#
+# 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="abcBridge aig blt saw-core hpb llvm-pretty llvm-pretty-bc-parser parameterized-utils"
+
+# base GitHub URL for Galois repos
+GITHUB_URL="[email protected]:GaloisInc"
+
+# Check if 'stack' is in the path
+if type stack >/dev/null 2>&1; then
+ echo "Found stack"
+else
+ echo >&2 "I require 'stack' but it's not installed. Aborting."
+ echo >&2 "Stack available at: http:https://docs.haskellstack.org/en/stable/install_and_upgrade"
+ exit 1
+fi
+
+if [ ! -d "dependencies" ]; then
+ mkdir -p "dependencies"
+fi
+
+# Download GitHub repos
+for pkg in $PKG_LIST; do
+ checkout "[email protected]:GaloisInc/$pkg.git" $pkg
+done
+
+checkout "[email protected]:joehendrix/IHaskell.git" IHaskell
+
+# Check for zmq
+pkg_result=$(pkg-config --exists "libzmq >= 4.0" || echo "NOT FOUND")
+if [[ ! -z $pkg_result ]]; then
+ echo "Failed to find libzmq using pkg-config."
+ echo "Please install it and set PKG_CONFIG_PATH to allow pkg-config to find it."
+fi

scripts/dreal-tee

@@ -0,0 +1,2 @@
+#!/bin/bash
+tee $HOME/dreal.in | dReal $@ 2> $HOME/dreal.err | tee $HOME/dreal.out

scripts/generate_hpc_report

@@ -0,0 +1,24 @@
+#!/bin/bash
+set -e
+
+echo "This script should be run from the mss root directory."
+
+
+show_help () {
+ echo ""
+ echo "mss does not appear to be built with coverage information."
+ echo ""
+ echo "Please rebuild mss with the following line:"
+ echo " cabal install --enable-tests --enable-library-coverage -f=enable-hpc"
+ echo ""
+ echo " --enable-library-coverage enables coverage information for the library."
+ echo " -f=enable-hpc does the same for the unitTest executable."
+}
+
+# Deleting existing coverage
+rm -f unitTest.tix
+# Run unit tests
+# ./dist/dist-sandbox-f97cc5fd/build/unitTest/unitTest
+# Generate markup report in hpc directory
+hpc markup --hpcdir=dist/hpc/mix/unitTest --hpcdir=dist/hpc/mix/galois-mss-0.5.18 --destdir=hpc_report unitTest.tix || show_help
+echo "Report available at hpc_report/hpc_index.html"

scripts/run_graphmod.sh

@@ -0,0 +1,22 @@
+#!/bin/bash
+set -e
+DIRS="galois-matlab/src crucible/src galois-mss/src galois-mss/mss"
+DIRS="crucible/src"
+
+# make sure graphmod and dot are in the PATH
+if ! type -p graphmod || ! type -p dot; then
+ echo "Error: cannot find 'graphmod' and/or 'dot' in PATH" 1>&2
+ exit 1
+fi
+
+run_graphmod()
+{
+ local dir="$1"
+ local name="$2"
+ local FILES="$(find $dir -name '*.hs')"
+ echo "Writing graphmod file to $2.svg"
+ graphmod -i $dir -p --no-cluster $FILES -q | dot -Tsvg > $2.svg
+}
+
+run_graphmod "galois-matlab/src" "galois-matlab"
+run_graphmod "crucible/src" "crucible"

scripts/yices-tee

@@ -0,0 +1,2 @@
+#!/bin/bash
+tee yices.in | yices $@ | tee yices.out

scripts/z3-tee

@@ -0,0 +1,2 @@
+#!/bin/bash
+tee z3.in | z3 $@ | tee z3.out

stack.yaml

@@ -0,0 +1,25 @@
+flags: {}
+extra-lib-dirs:
+ - /usr/local/lib
+
+packages:
+- crucible
+- crucible-abc
+- crucible-blt
+- crucible-saw
+- crucible-server
+- galois-matlab
+- dependencies/abcBridge
+- dependencies/aig
+- dependencies/blt
+- dependencies/IHaskell/ipython-kernel
+- dependencies/parameterized-utils
+- dependencies/hpb
+- dependencies/saw-core
+- dependencies/llvm-pretty
+- dependencies/llvm-pretty-bc-parser
+extra-deps:
+- clock-0.5.2
+- dotgen-0.4.2
+- fgl-visualize-0.1.0.1
+resolver: lts-5.3