Formally verified x86-64 decompilation
dot
is accessible by updating the PATH
environment variable.PATH
variable: PATH=$PATH:$HOME/.local/bin
./make.sh
and then sudo ./make.sh install
.git clone git@github.com:ssrg-vt/FoxDec.git
../foxdec/
.stack build --haddock --haddock-arguments --odir=docs/haddock
.
This builds the application and generates documentation using Haddock.stack install
. This copies executables to accessible locations.-c ./config/config.dhall -d examples/wc_small/ -n wc -v -i BINARY --Gmetrics
. This runs FoxDec on the wc
example.We use some tools that are assumed to be standard available and accessible (i.e., added to the PATH
environment variable). For Linux, these are readelf
and objdump
(latter is optional but convenient).
For Mac, these are otool
and nm
.
stack build --profile
time stack exec --profile -- foxdec-exe -c ./config/config.dhall -d examples/wc_small/ -n wc -v -i BINARY --Gmetrics +RTS -p
less foxdec-exe.prof
(DEPRECATED)
Regrettably, the Haskell environment is not yet up-to-date wrt. ARM64 architectures such as the M1 chip in new MacBooks. We cannot use our preferred build-tool Stack
, but have a setup working using cabal
. A drawback of this approach is that it may interfere with an existing installation of the Haskell environment. Also, the installation is way more involved. Specifically, it requires an edit in a .h
file of MacOs’ XCode Command Line Tools, which is unstable and comes with risk. As soon as Stack
supports ARM64, we will revert to that approach. If there are any issues, do not hesitate to contact us.
The GitHub page is here.
Install the Xcode Command Line tools:
xcode-select --install
Confirm the pop-up message. There is no need to install XCode in its entirety.
dot
is accessible by updating the PATH
environment variable.ghc
and cabal
using ghcup. The curl
-command they provide interactively asks you which things to install; there is no need to install stack
as it it is ARM64 incompatible. We have installed ghc 8.10.7
.Install LLVM
(version between 9 and 13, we have installed version 13.0.1) using homebrew:
brew install llvm
PATH
variable: export PATH="/opt/homebrew/opt/llvm/bin:$PATH"
./make.sh
and then sudo ./make.sh install
.Open, using sudo, the file /Library/Developer/CommandLineTools/SDKs/MacOSX12.1.sdk/usr/include/mach/arm/_structs.h
Insert the following as line 443
typedef unsigned __uint128_t __attribute__ ((mode (TI)));
This will define the __uint128_t
type: TI is Tetra-integer, which is 4 times the width of int
.
git clone git@github.com:ssrg-vt/FoxDec.git
../foxdec/
.Run
cabal build
This builds the application.
Run
cabal haddock --haddock-option "--odir=docs/haddock"
This generates documentation.
Run
cabal install
This copies executables to ~/.cabal/bin/
. Be sure that this directory is in your PATH
.
foxdec-exe 1 examples/du du
. This runs FoxDec on the du
example.