bisect

#!/usr/bin/env bash
# Copyright (c) 2020 Matt Windsor and contributors
#
# This file is part of c4-scripts.
# Licenced under the MIT licence; see `LICENSE`.

# Frontend for act's trace bisection.  Remembers all the arguments so you
# don't have to.

set -euo pipefail

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"
# shellcheck source=act_bash/naming.sh
source "${SCRIPTDIR}/act_bash/naming.sh"


## Arguments ##


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

# The name of the output directory.
# If empty, we use a temporary directory.
OUTPUT_DIR=""

# The ID of the machine to run.
MACHINE="localhost"

# The ID of the compiler to run.
COMPILER="gcc"

# The opt of the compiler to run.
OPT=""

# The mopt of the compiler to run.
MOPT=""

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


## Functions ##


# Prints the script's usage and exits.
usage() {
  echo "usage: $0 [-d DIR] [-m MACHINE] [-c COMPILER] [-O OPT] [-M OPT] [-${ACT_STANDARD_FLAGS}] TRACE BASE" >&2
  echo
  echo "-d: directory to use for outputting intermediate files"
  echo "-m: ID of machine to use"
  echo "-c: ID of compiler to use"
  echo "-O: optimisation level to use"
  echo "-M: machine optimisation profile to use"
  act::standard_usage

  exit 1
}

# The main function.
main() {
  while getopts "d:m:c:O:M:qvx?h" a; do
    case "${a}" in
    d) OUTPUT_DIR="${OPTARG}" ;;
    m) MACHINE="${OPTARG}" ;;
    c) COMPILER="${OPTARG}" ;;
    O) OPT="${OPTARG}" ;;
    M) MOPT="${OPTARG}" ;;
    *) act::parse_standard_args "${a}" "${OPTARG:-}" ;;
    esac
  done
  # VERBOSE etc. are used indirectly by various library functions.
  # shellcheck disable=SC2034
  readonly VERBOSE FUZZ MACHINE
  shift $((OPTIND-1))

  if [[ $# -ne 2 ]]; then act::arg_error "need two file arguments"; fi
  local trace="$1"
  local base="$2"

  local out_trace="$(basename trace).mini"
  local out_litmus="${out_trace}.litmus"

  act::fuzz bisect \
    -command "${SCRIPTDIR}/bisect_oracle" \
    -o "${out_trace}" \
    "${trace}" -- "${base}" \
    "${SCRIPTDIR}/bisect_driver" \
    "$(act::flags_qvx)" \
    -m "${MACHINE}" -c "${COMPILER}" -O "${OPT}" -M "${MOPT}"

  act::fuzz replay -o "${out_litmus}" -trace "${out_trace}" "${base}"

  diff -u "${base}" "${out_litmus}"
}

main "$@"