From 7f9cfb0c703a45965fea092b8ff198fdd7f81fe4 Mon Sep 17 00:00:00 2001
From: Robert Dockins <rdockins@galois.com>
Date: Tue, 13 Sep 2016 15:05:52 -0700
Subject: [PATCH] Initial commit of project structure

---
 .gitignore                  | 11 +++++
 README.md                   | 42 +++++++++++++++++++
 scripts/build-sandbox.sh    | 83 +++++++++++++++++++++++++++++++++++++
 scripts/dreal-tee           |  2 +
 scripts/generate_hpc_report | 24 +++++++++++
 scripts/run_graphmod.sh     | 22 ++++++++++
 scripts/yices-tee           |  2 +
 scripts/z3-tee              |  2 +
 stack.yaml                  | 25 +++++++++++
 9 files changed, 213 insertions(+)
 create mode 100644 .gitignore
 create mode 100644 README.md
 create mode 100755 scripts/build-sandbox.sh
 create mode 100755 scripts/dreal-tee
 create mode 100755 scripts/generate_hpc_report
 create mode 100755 scripts/run_graphmod.sh
 create mode 100755 scripts/yices-tee
 create mode 100755 scripts/z3-tee
 create mode 100644 stack.yaml

diff --git a/.gitignore b/.gitignore
new file mode 100644
index 000000000..e86bf931c
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,11 @@
+/build/
+/dependencies/
+.cabal-sandbox
+.stack-work
+**/cabal.config
+cabal.sandbox.config
+dist
+TAGS
+unitTest.tix
+hpc_report
+stack.yaml
\ No newline at end of file
diff --git a/README.md b/README.md
new file mode 100644
index 000000000..f802ea45d
--- /dev/null
+++ b/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://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.
diff --git a/scripts/build-sandbox.sh b/scripts/build-sandbox.sh
new file mode 100755
index 000000000..332867e85
--- /dev/null
+++ b/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="git@github.com: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://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 "git@github.com:GaloisInc/$pkg.git" $pkg
+done
+
+checkout "git@github.com: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
diff --git a/scripts/dreal-tee b/scripts/dreal-tee
new file mode 100755
index 000000000..9fc7bfb69
--- /dev/null
+++ b/scripts/dreal-tee
@@ -0,0 +1,2 @@
+#!/bin/bash
+tee $HOME/dreal.in | dReal $@ 2> $HOME/dreal.err | tee $HOME/dreal.out
diff --git a/scripts/generate_hpc_report b/scripts/generate_hpc_report
new file mode 100755
index 000000000..5b8e35f3d
--- /dev/null
+++ b/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"
diff --git a/scripts/run_graphmod.sh b/scripts/run_graphmod.sh
new file mode 100755
index 000000000..15324d055
--- /dev/null
+++ b/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"
diff --git a/scripts/yices-tee b/scripts/yices-tee
new file mode 100755
index 000000000..187aa5975
--- /dev/null
+++ b/scripts/yices-tee
@@ -0,0 +1,2 @@
+#!/bin/bash
+tee yices.in | yices $@ | tee yices.out
diff --git a/scripts/z3-tee b/scripts/z3-tee
new file mode 100755
index 000000000..64e1d341e
--- /dev/null
+++ b/scripts/z3-tee
@@ -0,0 +1,2 @@
+#!/bin/bash
+tee z3.in | z3 $@ | tee z3.out
diff --git a/stack.yaml b/stack.yaml
new file mode 100644
index 000000000..c52a4fefc
--- /dev/null
+++ b/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