diff --git a/resources/greed_client.dl b/resources/greed_client.dl new file mode 100644 index 0000000..d71017d --- /dev/null +++ b/resources/greed_client.dl @@ -0,0 +1,46 @@ +#include "decompiler_imports.dl" + +#include "guards.dl" +#include "loops_semantics.dl" + +#include "memory_modeling/memory_modeling.dl" +#include "storage_modeling/storage_modeling.dl" + +// storage layout output +.output StorageOffset_Type +.output StorageVariableInfo + +// guards analysis output +.output StaticallyGuardedBlock +.output Dominates + +// calldata arrays (and loops) output +.output BlockInStructuredLoop +.output InductionVariable +.output InductionVariableStartsAtConst +.output InductionVariableIncreasesByConst +.output InductionVariableUpperBoundVar +.output InductionVariableDecreasesByConst +.output InductionVariableLowerBoundVar +.output CallDataCopyLoop +.output MemoryCopyLoop + + +// more required outputs (see greed's TAC_parser.py) +// .output IRInFunctionFiltered(IO="file", filename="InFunction.csv", delimiter="\t") +// .output PublicFunction(IO="file", filename="PublicFunction.csv", delimiter="\t") +// .output TAC_Block +// .output TAC_Op +// .output TAC_OriginalStatement_Block +// .output TAC_Variable_Value +// .output TAC_Def +// .output TAC_Use +// .output ConstantPossibleSigHash +// .output CallToSignature +// .output CallToSignatureFromSHA3 +// .output IRFallthroughEdge +// .output HighLevelFunctionName +// .output LocalBlockEdge +// .output IRFunctionEntry +// .output FormalArgs +// .output StaticallyGuardedBlock diff --git a/resources/patches/gigahorse_greed_client.patch b/resources/patches/gigahorse_greed_client.patch deleted file mode 100644 index f3b5066..0000000 --- a/resources/patches/gigahorse_greed_client.patch +++ /dev/null @@ -1,52 +0,0 @@ -diff --git a/clientlib/greed_client.dl b/clientlib/greed_client.dl -new file mode 100644 -index 0000000..d71017d ---- /dev/null -+++ b/clientlib/greed_client.dl -@@ -0,0 +1,46 @@ -+#include "decompiler_imports.dl" -+ -+#include "guards.dl" -+#include "loops_semantics.dl" -+ -+#include "memory_modeling/memory_modeling.dl" -+#include "storage_modeling/storage_modeling.dl" -+ -+// storage layout output -+.output StorageOffset_Type -+.output StorageVariableInfo -+ -+// guards analysis output -+.output StaticallyGuardedBlock -+.output Dominates -+ -+// calldata arrays (and loops) output -+.output BlockInStructuredLoop -+.output InductionVariable -+.output InductionVariableStartsAtConst -+.output InductionVariableIncreasesByConst -+.output InductionVariableUpperBoundVar -+.output InductionVariableDecreasesByConst -+.output InductionVariableLowerBoundVar -+.output CallDataCopyLoop -+.output MemoryCopyLoop -+ -+ -+// more required outputs (see greed's TAC_parser.py) -+// .output IRInFunctionFiltered(IO="file", filename="InFunction.csv", delimiter="\t") -+// .output PublicFunction(IO="file", filename="PublicFunction.csv", delimiter="\t") -+// .output TAC_Block -+// .output TAC_Op -+// .output TAC_OriginalStatement_Block -+// .output TAC_Variable_Value -+// .output TAC_Def -+// .output TAC_Use -+// .output ConstantPossibleSigHash -+// .output CallToSignature -+// .output CallToSignatureFromSHA3 -+// .output IRFallthroughEdge -+// .output HighLevelFunctionName -+// .output LocalBlockEdge -+// .output IRFunctionEntry -+// .output FormalArgs -+// .output StaticallyGuardedBlock diff --git a/setup.sh b/setup.sh index fa70d7b..31d4be8 100755 --- a/setup.sh +++ b/setup.sh @@ -42,60 +42,6 @@ ln -sf $GREED_DIR/resources/run.py $VIRTUAL_ENV/bin/greed # pip install greed pip install -e . -######################################################################################################################## -######################################################################################################################## -# GIGAHORSE -######################################################################################################################## - -if [ -z $NO_GIGAHORSE ]; then - echo "Number of parallel datalog jobs: $j (override with $0 -j N)" - read -rsn1 -p "Setting up gigahorse.. Press any key to continue (ctrl-c to abort)" - echo - - # clone the gigahorse-toolchain repo - if [ ! -d $GREED_DIR/gigahorse-toolchain ]; then - git clone --recursive https://github.com/nevillegrech/gigahorse-toolchain.git $GIGAHORSE_DIR - cd $GIGAHORSE_DIR - git checkout c5bce4d3495fc10f503b49368504efee3c676d03 - fi - - # apply patches - cd $GIGAHORSE_DIR - for PATCH_FILE in $GREED_DIR/resources/patches/*.patch; do - git apply --reverse --check $PATCH_FILE &>/dev/null || git apply $PATCH_FILE - done - cd $GREED_DIR - - # compile gigahorse clients - command -v >&- souffle || { echo "${bold}${red}souffle is not installed. Please install it before proceeding (https://souffle-lang.github.io/build, version 2.0.2 preferred)${normal}"; echo "${bold}${red}Or maybe you forgot --no-gigahorse?${normal}"; exit 1; } - dpkg -l | grep -q libboost-all-dev || { echo "${bold}${red}libboost-all-dev is not installed. Please install it before proceeding (e.g., sudo apt install libboost-all-dev)${normal}"; echo "${bold}${red}Or maybe you forgot --no-gigahorse?${normal}"; exit 1; } - - echo "Compiling gigahorse clients. This will take some time.." - - # compile souffle - cd $GIGAHORSE_DIR/souffle-addon - make || { echo "${bold}${red}Failed to build gigahorse's souffle-addon${normal}"; exit 1; } - cd $GREED_DIR - - function compile () { - echo "Compiling $1.." - souffle --jobs $j -M "GIGAHORSE_DIR=$GIGAHORSE_DIR BULK_ANALYSIS=" -o $GIGAHORSE_DIR/clients/$1_compiled.tmp $GIGAHORSE_DIR/$2 -L $GIGAHORSE_DIR/souffle-addon || { echo "${bold}${red}Failed to build $1_compiled${normal}"; exit 1; } && - mv $GIGAHORSE_DIR/clients/$1_compiled.tmp $GIGAHORSE_DIR/clients/$1_compiled && - mv $GIGAHORSE_DIR/clients/$1_compiled.tmp.cpp $GIGAHORSE_DIR/clients/$1_compiled.cpp && - echo "Successfully compiled $1.." - } - compile "main.dl" "logic/main.dl" - compile "greed_client.dl" "clientlib/greed_client.dl" - # compile "function_inliner.dl" "clientlib/function_inliner.dl" - # compile "loops_semantics.dl" "clientlib/loops_semantics.dl" - # compile "guards.dl" "clientlib/guards.dl" - - command -v >&- mkisofs || echo "${bold}${red}mkisofs is not installed. solc-select might not work correctly (e.g., sudo apt install mkisofs)${normal}" - solc-select versions | grep -q 0.8.7 || { echo "Installing solc 0.8.7"; solc-select install 0.8.7; } -else - true -fi - ######################################################################################################################## ######################################################################################################################## # YICES @@ -115,9 +61,9 @@ dpkg -l | grep -q gperf || { echo "${bold}${red}gperf is not installed. Please i dpkg -l | grep -q libgmp-dev || { echo "${bold}${red}libgmp-dev is not installed. Please install it before proceeding (e.g., sudo apt install libgmp-dev)${normal}"; exit 1; } # install -# make clean || { echo "${bold}${red}Failed to run make clean ${normal}"; exit 1; } +make clean || { echo "${bold}${red}Failed to run make clean ${normal}. Continuing..."; } autoconf || { echo "${bold}${red}Failed to run autoconf${normal}"; exit 1; } -./configure --enable-thread-safety || { echo "${bold}${red}Failed to run ./configure${normal}"; exit 1; } +./configure || { echo "${bold}${red}Failed to run ./configure${normal}"; exit 1; } make || { echo "${bold}${red}Failed to run make${normal}"; exit 1; } # finally, link yices2/build/lib/ to the virtualenv's site-packages dir @@ -135,8 +81,58 @@ if [ ! -d $GREED_DIR/yices2_python_bindings ]; then fi # for some reason github builds fail to find libyices.so. This should fix it +ls -lah $VIRTUAL_ENV_LIB | grep yices export PYTHONPATH=$PYTHONPATH:$VIRTUAL_ENV_LIB pip install -e yices2_python_bindings yices_python_info +######################################################################################################################## +######################################################################################################################## +# GIGAHORSE +######################################################################################################################## + +if [ -z $NO_GIGAHORSE ]; then + # install solc-select + command -v >&- mkisofs || echo "${bold}${red}mkisofs is not installed. solc-select might not work correctly (e.g., sudo apt install mkisofs)${normal}" + solc-select versions | grep -q 0.8.7 || { echo "Installing solc 0.8.7"; solc-select install 0.8.7; } + + # then install gigahorse from the official repo + echo "Number of parallel datalog jobs: $j (override with $0 -j N)" + read -rsn1 -p "Setting up gigahorse.. Press any key to continue (ctrl-c to abort)" + echo + + command -v >&- souffle || { echo "${bold}${red}souffle is not installed. Please install it before proceeding (see https://github.com/souffle-lang/souffle/releases/tag/2.4 and https://souffle-lang.github.io/build, version 2.4 preferred)${normal}"; echo "${bold}${red}Or maybe you forgot --no-gigahorse?${normal}"; exit 1; } + dpkg -l | grep -q libboost-all-dev || { echo "${bold}${red}libboost-all-dev is not installed. Please install it before proceeding (e.g., sudo apt install libboost-all-dev)${normal}"; echo "${bold}${red}Or maybe you forgot --no-gigahorse?${normal}"; exit 1; } + + # clone the gigahorse-toolchain repo + if [ ! -d $GREED_DIR/gigahorse-toolchain ]; then + git clone --recursive https://github.com/nevillegrech/gigahorse-toolchain.git $GIGAHORSE_DIR + cd $GIGAHORSE_DIR + git checkout c5bce4d3495fc10f503b49368504efee3c676d03 + fi + + # copy greed client + cp $GREED_DIR/resources/greed_client.dl $GIGAHORSE_DIR/clientlib/ + + # compile souffle + echo "Compiling souffle-addon.." + cd $GIGAHORSE_DIR/souffle-addon + make || { echo "${bold}${red}Failed to build gigahorse's souffle-addon${normal}"; exit 1; } + cd $GREED_DIR + + # compile gigahorse clients + echo "Compiling gigahorse clients. This will take some time.." + function compile () { + echo "Compiling $1.." + souffle --jobs $j -M "GIGAHORSE_DIR=$GIGAHORSE_DIR BULK_ANALYSIS=" -o $GIGAHORSE_DIR/clients/$1_compiled.tmp $GIGAHORSE_DIR/$2 -L $GIGAHORSE_DIR/souffle-addon || { echo "${bold}${red}Failed to build $1_compiled${normal}"; exit 1; } && + mv $GIGAHORSE_DIR/clients/$1_compiled.tmp $GIGAHORSE_DIR/clients/$1_compiled && + mv $GIGAHORSE_DIR/clients/$1_compiled.tmp.cpp $GIGAHORSE_DIR/clients/$1_compiled.cpp && + echo "Successfully compiled $1.." + } + compile "main.dl" "logic/main.dl" + compile "greed_client.dl" "clientlib/greed_client.dl" +else + true +fi + set +x