do_memalloy_amplify

#!/usr/bin/env bash
#
# A harness script that runs memalloy (looking for it in the given directory),
# amplifies every result it generates, and outputs it into another given
# directory.

set -euo pipefail

SCRIPTDIR="${SCRIPTDIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"}"
# 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"

declare DEFAULT_MEMALLOY_EVENTS ACT_STANDARD_FLAGS ACT_STANDARD_OPTS
# shellcheck source=./act_bash/memalloy.sh
source "${SCRIPTDIR}/act_bash/memalloy.sh"

## 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 we are using Dune to execute c4f.
DUNE_EXEC="false"

# Whether we are forcing Memalloy and DNF to run even if we have a results directory.
FORCE_MEMALLOY="false"

# The directory in which Memalloy lives.
MEMALLOY_DIR=""

# The amplified output directory.
AMP_DIR=""

# The number of events to ask Memalloy to generate.
# Defaults to `DEFAULT_MEMALLOY_EVENTS` if empty.
MEMALLOY_EVENTS=""

## Functions ##


# Prints usage information and exits.
usage() {
  echo "Usage: $0"
  echo "  [-a ARCH] [-b BACKEND] [-e NUM_MEMALLOY_EVENTS]"
  echo "  [-f${ACT_STANDARD_FLAGS}] MEMALLOY_DIR OUTPUT_DIR"
  echo
  echo "-a: ID of architecture to use if the backend requires one"
  echo "-b: ID of backend to use for checking C files"
  echo "-e: number of events for Memalloy to produce (default ${DEFAULT_MEMALLOY_EVENTS})"
  echo "-f: force run of Memalloy even if MEMALLOY_DIR/results/_latest exists"
  act::standard_usage
  echo
  echo "OUTPUT_DIR will be created if needed, and MAY be a subdirectory of"
  echo "MEMALLOY_DIR/results/_latest".
  exit
}


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

  act::check_dune_exec

  if [[ $# -ne 2 ]]; then act::arg_error "need two directory arguments"; fi
  readonly MEMALLOY_DIR=$1
  readonly AMP_DIR=$2

  local results_dir="${MEMALLOY_DIR}/results/_latest"

  run_memalloy_if_needed "${results_dir}"

  amplify_if_needed "${results_dir}"
}


# Checks whether Memalloy forcing is on, or if the results directory is
# not present.  If either are true, runs `do_memalloy` in the specified
# Memalloy directory.
#
# Globals:
#   FORCE_MEMALLOY: read
#   (various others read indirectly)
#
# Arguments:
#   1: the memalloy results directory.
run_memalloy_if_needed() {
  local results_dir="${1}"

  if [[ ${FORCE_MEMALLOY} = "true" || ( ! -d "${results_dir}" ) ]]; then
    run_memalloy
  else
    act::log "Using existing memalloy results directory"
    dump_last_modified_time "${results_dir}"
    act::log ".\n"
  fi

  if [[ ! -d "${results_dir}" ]]; then
    act::fatal "Missing Memalloy results directory"
  fi
}


# Runs `do_memalloy` in the Memalloy directory.
#
# This does not take in the results directory as an argument, as
# Memalloy automatically infers it from its own directory.
#
# Globals:
#   MEMALLOY_DIR: read
#   MEMALLOY_EVENTS: read
#   SCRIPTDIR: read
#   (various others read indirectly)
run_memalloy() {
  act::log "Running memalloy.\n"
  act::run_with_qvx "${SCRIPTDIR}/do_memalloy" -e "${MEMALLOY_EVENTS}" "${MEMALLOY_DIR}"
}


# Checks whether Memalloy forcing is on, or if the DNF directory is
# not present.  If either are true, runs `make_amp` for each result in
# the results directory, outputting successful results to the
# DNF directory.
#
# If we are reusing the existing Memalloy directory, and verbosity is on,
#
# Globals:
#   AMP_DIR: read
#   FORCE_MEMALLOY: read
#   (various others read indirectly)
#
# Arguments:
#   1: the memalloy results directory.
amplify_if_needed() {
  local results_dir="${1}"

  if [[ ${FORCE_MEMALLOY} = "true" || ( ! -d "${AMP_DIR}" ) ]]; then
    amplify "${results_dir}" "${AMP_DIR}"
  else
    act::log "Using existing amplify directory"
    dump_last_modified_time "${AMP_DIR}"
    act::log ".\n"
  fi

  if [[ ! -d "${AMP_DIR}" ]]; then act::fatal "Missing amplify directory"; fi
}


# Amplifies each test in the results directory, outputting the # results to the
# given directory.
#
# Globals:
#   SCRIPTDIR: read
#   (various others read indirectly)
#
# Arguments:
#   1: the memalloy results directory.
#   2: the amp output directory.
amplify() {
  local results_dir="${1}"
  local amp_dir="${2}"

  act::log "Amplifying memalloy results.\n"
  mkdir -p "${amp_dir}"

  for file in "${results_dir}/litmus"/*.litmus; do
    local out_file
    out_file="${amp_dir}/$(basename "${file}")"
    act::log "~> %s (to %s)\n" "${file}" "${out_file}"
    act::run_with_qvx "${SCRIPTDIR}/amplify" \
      -a "${ARCH}" -b "${BACKEND}" \
      "${file}" > "${out_file}" || broken_amp "${out_file}"
  done
}


# Prints an error indicating that an attempt to convert a postcondition
# to a DNF failed, then moves the offending file out of the way.
#
# Because this might be caused by the backend used for DNF analysis not
# understanding the input correctly (which is eminently possible with
# backends like herd7), it needs to be handled semi-gracefully.
#
# Arguments:
#   1.  The file that failed postcondition conversion.
broken_amp() {
  local file="$1"
  local new_file="${file}.bad_amp"

  act::error "Couldn't DNF postcondition for ${file}."
  act::error "Moving out of the way (to ${new_file})."
  mv "${file}" "${new_file}"
}


# If `stat` is available, prints the last modified time of the given results
# directory symlink (less a newline).
#
# Arguments:
#   1: the results-directory symlink to inspect.
dump_last_modified_time() {
  local results_dir=$1

  # `stat` is non-standard: if it exists, it'll have different flags depending
  # on whether we're on a GNU or BSD system (or, indeed, a non-GNU non-BSD
  # system, but we don't support that yet).  The other thing is that `printf`
  # has different format flags!
  if [[ -z $(command -v stat)  ]]; then return 1; fi
  case "$(uname -s)" in
    Linux)
      # GNU stat and printf
      local mtime
      mtime="$(stat -Lc "%Y" "${results_dir}")"
      act::log " (last modified on %(%c)T)" "${mtime}"
      ;;
    Darwin|NetBSD|OpenBSD)
      # BSD stat and printf
      local mtime
      mtime="$(stat -Lf "%Sm" "${results_dir}")"
      act::log " (last modified on %s)" "${mtime}"
      ;;
    *) return 2 ;;
  esac
}


## Entry point ##
main "$@"