Skip to content
Permalink
Browse files

produces factc instead of fact.byte

  • Loading branch information...
scauligi committed Feb 20, 2019
1 parent fb3e284 commit af9b2035b3d698728312dabee8f7c311e44e409a
Showing with 34 additions and 30 deletions.
  1. +1 −0 .gitignore
  2. +4 −0 Makefile
  3. +24 −26 README.md
  4. +1 −0 _oasis
  5. +1 −1 docker/README.md
  6. +2 −2 test/Makefile
  7. +1 −1 test/arrcopy_test/Makefile
@@ -57,3 +57,4 @@ setup.data
setup.ml
configure
*.pseudo.fact
factc
@@ -1,3 +1,7 @@
factc: setup.data
$(SETUP) -build -no-links
cp _build/src/fact.byte factc

# OASIS_START
# DO NOT EDIT (digest: a3c674b4239234cbbe53afe090018954)

@@ -17,17 +17,35 @@ that need to be free from timing side channels.

#### Basic Usage

Run ```./fact.byte ex.fact``` to compile a FaCT program where ```ex.fact``` is the name of your file.
Run ```./factc ex.fact``` to compile a FaCT program where ```ex.fact``` is the name of your file.

#### Link to a C library

FaCT is designed to be called from C code. In order to do so, write your FaCT functions and compile them. This will output an object file. This can then be linked to a C file. For example:

```./factc ex.fact```
Then we compile the calling C file:
```
clang -c main.c
```
Next, we link them together:
```clang -o final main.o ex.o```
Finally, we can run the executable:
```./final```
#### Debugging
Many debugging options and intermediate data structures are available. Run ```./fact.byte -help``` for all options.
Many debugging options and intermediate data structures are available. Run ```./factc -help``` for all options.
## Installation
To install you can either build the source or download ```fact.byte```. We recommend to build from source if possible.

```fact.byte``` is the executable used to compile FaCT programs. Execute ```./fact.byte -help``` for a list of the command line options.
To install you can either build the source or download ```factc```. We recommend to build from source if possible.
### Setting up the build environment
@@ -84,24 +102,4 @@ We can now build the compiler:
```make```
This will give us the ```fact.byte``` executable.
## Link to a C library
FaCT is designed to be called from C code. In order to do so, write your FaCT functions and compile them. This will output an object file. This can then be linked to a C file. For example:
```fact ex.fact```
Then we compile the calling C file:
```
clang -c main.c
```
Next, we link them together:
```clang -o final main.o ex.o```
Finally, we can run the executable:
```./final```
This will give us the ```factc``` executable.
1 _oasis
@@ -10,6 +10,7 @@ BuildDepends: llvm, llvm.analysis, llvm.bitwriter, llvm.executionengine, llvm.ta
OCamlVersion: >= 4.06
AlphaFeatures: ocamlbuild_more_args
XOCamlbuildPluginTags: package(cppo_ocamlbuild)
PostCleanCommand: rm -f factc

Executable fact
Path: src
@@ -12,6 +12,6 @@ oasis setup
make
```
This will produce `fact.byte`, the FaCT executable. If you're getting errors try running `make clean` and removing `setup.data` then running the above commands again.
This will produce `factc`, the FaCT executable. If you're getting errors try running `make clean` and removing `setup.data` then running the above commands again.
Additionally, to verify code as constant-time, the FaCT compiler uses [ct-verif](https://github.com/imdea-software/verifying-constant-time/) in a Docker container (warning: compressed image is 720 MB). It can be used regardless of whether the FaCT container is used.
@@ -25,7 +25,7 @@ all: $(TESTS) run failure

# test_%.fact --> test_%.o
%.o: %.fact
../fact.byte -debug -ast-out -core-ir-out -llvm-out -pseudocode -generate-header $<
../factc -debug -ast-out -core-ir-out -llvm-out -pseudocode -generate-header $<

# harness_%.c --> harness_%_runner.c
%_runner.c: %.c
@@ -40,7 +40,7 @@ run:

FAILURES_DIR=failures
failure:
@for x in $(FAILURES_DIR)/*.fact; do ../fact.byte $$x 2> /dev/null && { echo "ERROR: Build succeeded but should not have -- $$x"; exit 1; } || echo "Build failed as expected -- $$x" ; done
@for x in $(FAILURES_DIR)/*.fact; do ../factc $$x 2> /dev/null && { echo "ERROR: Build succeeded but should not have -- $$x"; exit 1; } || echo "Build failed as expected -- $$x" ; done

clean:
rm -f *.o *.bc *.s *_runner.c testbin* *.ast.ml *.tast.ml *.core.ml *.ll *.pseudo.fact *.xftast.ml *.h $(FAILURES_DIR)/*.o $(FAILURES_DIR)/*.bc $(FAILURES_DIR)/*.s
@@ -3,7 +3,7 @@ all: salsa.bin
.PRECIOUS: fact_%.h

fact_%.o: fact_%.fact
../../fact.byte -ast-out -pseudocode -generate-header -llvm-out -debug $^
../../factc -ast-out -pseudocode -generate-header -llvm-out -debug $^

fact_%.h: fact_%.o
touch $@

0 comments on commit af9b203

Please sign in to comment.
You can’t perform that action at this time.