amplify_postcondition

#!/usr/bin/env bash
# Reads a C litmus test in from the given file, runs it using the given backend,
# and generates an amplified postcondition from the resulting states.
#
# For usage information, scroll down to the `usage` function.

set -o errexit
set -o pipefail
set -o nounset

SCRIPTDIR="${SCRIPTDIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"}"
readonly SCRIPTDIR

# shellcheck source=./act_bash/args.sh
source "${SCRIPTDIR}/act_bash/args.sh"
# shellcheck source=./act_bash/exec.sh
source "${SCRIPTDIR}/act_bash/exec.sh"
# shellcheck source=./act_bash/log.sh
source "${SCRIPTDIR}/act_bash/log.sh"


## Constants and arguments ##


# The architecture ID to use, if we're targeting a backend that needs it.
# Can be empty.
ARCH=""

# The backend ID to use to get state sets.
# Can be empty, in which case the first backend defined gets run.
BACKEND=""

# TODO(@MattWindsor91): eventually reinstate compiler-indirect amplification.

# Whether or not we're running ACT programs through `dune exec`.
DUNE_EXEC="false"

# Whether or not verbose logging is enabled.
VERBOSE="false"


## Functions ##


# Prints usage information and exits.
usage() {
  echo "Usage: $0 [-a ARCH] [-b BACKEND] [-${ACT_STANDARD_FLAGS}] C_TEST"
  echo
  echo "-a: ID of architecture to use if the backend requires one"
  echo "-b: ID of backend to use for checking C files"
  act::standard_usage
  exit 1
}


main() {
  while getopts "a:b:qvx?h" a; do
    case ${a} in
    a) ARCH="${OPTARG}" ;;
    b) BACKEND="${OPTARG}" ;;
    *) act::parse_standard_args "${a}" "${OPTARG:-}" ;;
    esac
  done
  readonly ARCH BACKEND
  # These are used indirectly by various library functions.
  # shellcheck disable=SC2034
  readonly DUNE_EXEC VERBOSE
  shift $((OPTIND-1))

  act::check_dune_exec
  if [[ $# -ne 1 ]]; then act::arg_error "need precisely one file argument"; fi

  local original_file=$1

  c4t-backend -a "${ARCH}" -n "${BACKEND}" "${original_file}" |
  c4t-obs -p
}


## Entry point ##
main "${@}"