From 68ce94872ec6f296c44bdf4caa6aa4fb9c413ad7 Mon Sep 17 00:00:00 2001 From: Nicola Ruaro Date: Wed, 23 Aug 2023 23:27:56 -0700 Subject: [PATCH] make clean yices, update gigahorse client --- .../patches/gigahorse_greed_client.patch | 23 +++++++++++++++---- setup.sh | 1 + 2 files changed, 20 insertions(+), 4 deletions(-) diff --git a/resources/patches/gigahorse_greed_client.patch b/resources/patches/gigahorse_greed_client.patch index 867b72f..f3b5066 100644 --- a/resources/patches/gigahorse_greed_client.patch +++ b/resources/patches/gigahorse_greed_client.patch @@ -1,20 +1,36 @@ diff --git a/clientlib/greed_client.dl b/clientlib/greed_client.dl new file mode 100644 -index 0000000..d88493b +index 0000000..d71017d --- /dev/null +++ b/clientlib/greed_client.dl -@@ -0,0 +1,30 @@ +@@ -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 StorageVariableType ++.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") @@ -34,4 +50,3 @@ index 0000000..d88493b +// .output IRFunctionEntry +// .output FormalArgs +// .output StaticallyGuardedBlock -\ No newline at end of file diff --git a/setup.sh b/setup.sh index 84cda1f..fc7d349 100755 --- a/setup.sh +++ b/setup.sh @@ -115,6 +115,7 @@ 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; } 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; } make || { echo "${bold}${red}Failed to run make${normal}"; exit 1; }