Skip to content

Commit

Permalink
clean setup.sh
Browse files Browse the repository at this point in the history
  • Loading branch information
@ruaronicola
ruaronicola committed Sep 27, 2023
1 parent 84b82bf commit e0af7ba
Show file tree
Hide file tree
Showing 3 changed files with 98 additions and 108 deletions.
46 changes: 46 additions & 0 deletions resources/greed_client.dl
View file
Original file line number Diff line number Diff line change
@@ -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
52 changes: 0 additions & 52 deletions resources/patches/gigahorse_greed_client.patch
View file

This file was deleted.

108 changes: 52 additions & 56 deletions setup.sh
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand All @@ -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

0 comments on commit e0af7ba

Please sign in to comment.