run_yul_equivalence.sh

#!/usr/bin/sh

TMPDIR=$(mktemp -d)
cd "$TMPDIR"

compile()
{
	solc --yul --yul-dialect evm $1 2> /dev/null | awk 'f{print;f=0} /Binary representation:/{f=1}'
}

echo ""
echo "Checking optimization equivalence for $1"

nonopt_bin=$(compile $1)
if [ -z "$nonopt_bin" ]
then
	echo "Could not compile nonoptimized code."
	exit 1
fi

sed '0,/^\/\/ step:/d' $1 | sed -e 's!\/\/!!' > optsource
opt_bin=$(compile optsource)
if [ -z "$opt_bin" ]
then
	echo "Could not compile optimized code."
	exit 1
fi

if [[ "$nonopt_bin" == "$opt_bin" ]]
then
	echo "Nonoptimized and optimized bytecodes are the same."
	exit 1
fi

echo "Checking bytecode equivalence: $nonopt_bin vs $opt_bin"
timeout 10s /home/leonardo/devel/dapptools/src/hevm/hevm equivalence --code-a $nonopt_bin --code-b $opt_bin --smttimeout 1000
if [[ $? == 124 ]]
then
	echo "HEVM timeout."
fi

rm -rf "$TMPDIR"
exit 0