diff --git a/k-distribution/src/main/assembly/bin.xml b/k-distribution/src/main/assembly/bin.xml index 98d9693c566..3ea8529e2bd 100644 --- a/k-distribution/src/main/assembly/bin.xml +++ b/k-distribution/src/main/assembly/bin.xml @@ -96,6 +96,18 @@ ${project.basedir}/../llvm-backend/target/build/install/bindings /bindings + + ${project.basedir}/../llvm-backend/src/main/scripts/bin + /bin + 775 + 775 + + + ${project.basedir}/../llvm-backend/src/main/scripts/lib + /lib/kframework + 775 + 775 + ${project.basedir}/../haskell-backend/src/main/native/haskell-backend/src/main/kore /include/kframework/kore diff --git a/llvm-backend/src/main/scripts/bin/llvm-kompile-matching b/llvm-backend/src/main/scripts/bin/llvm-kompile-matching new file mode 100755 index 00000000000..116c22aa2ee --- /dev/null +++ b/llvm-backend/src/main/scripts/bin/llvm-kompile-matching @@ -0,0 +1,56 @@ +#!/usr/bin/env sh + +PNAME=$(basename "$0") + +print_usage () { +cat < [logging] + +$PNAME options: + The definition.kore file to generate the matching decision + tree from. + + A string of single characters representing a sequence of + heuristics to use during pattern matching compilation. + Valid choices are f, d, b, a, l, r, n, p, q, _, N, L, R. + The most common case is 'qbaL' + + The directory where the dt files will be written + + Threshold heuristic to use when choosing which axioms to + optimize. A value of 0 turns the optimization off; a value + of 1 turns the optimization on for every axiom. Values in + between (expressed as a fraction of two integers, e.g. 1/2), + control the aggressiveness of the optimization. Higher + values increase compilation times extremely, but also + increase the effectiveness of the optimization. Consider + decreasing this threshold if compilation is too slow. + The most common case is '1/2' + + [logging] Set this (ie. to '1') to enable logging (very large output) +HERE +} + +fail () { + print_usage + echo + echo "$1" + exit 1 +} + +if [ $# -eq 0 ]; +then + print_usage + exit +elif [ $# -lt 4 ]; +then + fail "ERROR: Not enough arguments!" +elif [ ! -f $1 ]; +then + fail "ERROR: not a file!" +elif [ ! -d $3 ]; +then + fail "ERROR: not a directory!" +fi + +"$(dirname "$0")/../lib/kframework/llvm-backend" "$@" diff --git a/llvm-backend/src/main/scripts/lib/llvm-backend b/llvm-backend/src/main/scripts/lib/llvm-backend new file mode 100755 index 00000000000..249e7a837d8 --- /dev/null +++ b/llvm-backend/src/main/scripts/lib/llvm-backend @@ -0,0 +1,6 @@ +#!/usr/bin/env bash +source "$(dirname "$0")/setenv" +ulimit -s "$(ulimit -H -s)" + +eval "$JAVA" org.kframework.backend.llvm.matching.Matching '"$@"' +