From 349df8d16d13f2d06e00b7e59cf7453da98e0dfd Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Fri, 15 Mar 2024 13:56:38 +0100 Subject: [PATCH] add flags for optimizations --- action.yml | 8 ++++++++ docker-action/entrypoint.sh | 7 +++++++ entrypoint.sh | 1 + 3 files changed, 16 insertions(+) diff --git a/action.yml b/action.yml index f6ac949..fdf4eeb 100644 --- a/action.yml +++ b/action.yml @@ -90,6 +90,14 @@ inputs: description: 'Disable non-linear integer arithmetic. Non compatible yet with Carbon' required: false default: '0' + moreJoins: + description: 'Use a more complete state merging algorithm.' + required: false + default: '0' + unsafeWildcardOptimization: + description: "Perform the optimization described in silicon's PR #756. You must ensure that the necessary conditions for the optimization are met." + required: false + default: '0' useZ3API: description: 'Use the Z3 API in silicon.' required: false diff --git a/docker-action/entrypoint.sh b/docker-action/entrypoint.sh index 50babc8..cee8368 100644 --- a/docker-action/entrypoint.sh +++ b/docker-action/entrypoint.sh @@ -121,11 +121,18 @@ if [[ $INPUT_DISABLENL -eq 1 ]]; then GOBRA_ARGS="$GOBRA_ARGS --disableNL" fi +if [[ $INPUT_UNSAFEWILDCARDOPTIMIZATION -eq 1 ]]; then + GOBRA_ARGS="$GOBRA_ARGS --unsafeWildcardOptimization" +fi if [[ $INPUT_CONDITIONALIZEPERMISSIONS -eq 1 ]]; then GOBRA_ARGS="$GOBRA_ARGS --conditionalizePermissions" fi +if [[ $INPUT_MOREJOINS -eq 1 ]]; then + GOBRA_ARGS="$GOBRA_ARGS --moreJoins" +fi + if [[ $INPUT_OVERFLOW -eq 1 ]]; then GOBRA_ARGS="$GOBRA_ARGS --overflow" fi diff --git a/entrypoint.sh b/entrypoint.sh index 23129f8..f782a4e 100644 --- a/entrypoint.sh +++ b/entrypoint.sh @@ -11,6 +11,7 @@ docker run -e INPUT_CACHING -e INPUT_PROJECTLOCATION -e INPUT_INCLUDEPATHS -e IN -e INPUT_OVERFLOW -e INPUT_VIPERBACKEND -e INPUT_JAVAXSS -e INPUT_JAVAXMX -e INPUT_TIMEOUT -e INPUT_HEADERONLY -e INPUT_STATSFILE \ -e INPUT_MODULE -e INPUT_RECURSIVE -e INPUT_ASSUMEINJECTIVITYONINHALE -e INPUT_CHECKCONSISTENCY -e INPUT_MCEMODE \ -e INPUT_REQUIRETRIGGERS \ + -e INPUT_UNSAFEWILDCARDOPTIMIZATION -e INPUT_MOREJOINS \ -e INPUT_USEZ3API -e INPUT_DISABLENL \ -e INPUT_PARALLELIZEBRANCHES -e INPUT_CONDITIONALIZEPERMISSIONS -e GITHUB_WORKSPACE -e GITHUB_REPOSITORY \ -e STATS_TARGET -e DEBUG_MODE -v "$RUNNER_WORKSPACE:$GITHUB_WORKSPACE" -v "$INPUT_STATSFILE:$STATS_TARGET" \