act/Makefile at main · argotorg/act · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
.DEFAULT_GOAL := compiler
.PHONY: parser compiler docs

parser: src/Act/Lex.hs src/Act/Parse.hs

src/Act/Parse.hs: src/Act/Parse.y src/Act/Syntax/Untyped.hs
	happy src/Act/Parse.y

src/Act/Lex.hs: src/Act/Lex.x
	alex src/Act/Lex.x

# builds the rest of the haskell files (compiler)
bin/act: src/CLI/*.hs src/Act/*.hs
	cabal v2-install --installdir=bin --overwrite-policy=always

repl: src/Act/Lex.hs src/Act/Parse.hs
	cabal v2-repl

compiler: bin/act

docs:
	cd doc && mdbook build

docs-serve:
	cd doc && mdbook serve

frontend_pass=$(wildcard tests/typing/pass/*/*.act)
frontend_fail=$(wildcard tests/typing/fail/*/*.act)

parser_pass=$(filter-out $(failing_parser), $(frontend_pass))
typing_pass=$(filter-out $(failing_typing), $(frontend_pass))

# supposed to fail
parser_fail=$() # no tests that are supposed to fail parsing
typing_fail=$(filter-out $(passing_typing), $(frontend_fail))

# supposed to pass, but fail
failing_parser=tests/typing/pass/dss/vat.act
failing_typing=tests/typing/pass/dss/vat.act tests/typing/pass/creation/createMultiple.act tests/typing/pass/staticstore/staticstore.act
# supposed to fail, but pass
passing_typing=tests/typing/fail/array/out_of_bounds_inv.act tests/typing/fail/array/out_of_bounds_post.act tests/typing/fail/array/out_of_bounds_preupdate.act tests/typing/fail/array/out_of_bounds_postupdate.act \
	       tests/typing/fail/array/const_array.act

invariant_specs=$(wildcard tests/invariants/*/*.act)
invariant_pass=$(filter-out $(invariant_buggy), $(wildcard tests/invariants/pass/*.act) $(typing_pass))
invariant_fail=$(wildcard tests/invariants/fail/*.act)

postcondition_specs=$(wildcard tests/postconditions/*/*.act)
postcondition_pass=$(wildcard tests/postconditions/pass/*.act) $(typing_pass)
postcondition_fail=$(wildcard tests/postconditions/fail/*.act)

# supposed to pass, but timeout
hevm_buggy=tests/hevm/pass/transfer/transfer.act tests/hevm/pass/multisource/amm/sol_vyper.json tests/hevm/pass/multisource/amm/vyper_sol.json tests/hevm/pass/cast-3/cast-3.act
# supposed to pass
hevm_pass=$(filter-out $(hevm_buggy), $(wildcard tests/hevm/pass/*/*.act))
hevm_vy_pass=$(wildcard tests/hevm/pass/vyper/*/*.act)
hevm_multi_pass=$(filter-out $(hevm_buggy), $(wildcard tests/hevm/pass/multisource/*/*.json))
# supposed to fail
hevm_fail=$(wildcard tests/hevm/fail/*/*.act)
# supposed to pass
hevm_slow=tests/hevm/pass/amm/amm.act tests/hevm/pass/amm-2/amm-2.act
hevm_multi_slow=$(wildcard tests/hevm/pass/multisource/amm/*.json) $(wildcard tests/hevm/pass/multisource/erc20/*.json)
# supposed to pass, no slow tests
hevm_fast=$(filter-out $(hevm_slow), $(hevm_pass))
hevm_multi_fast=$(filter-out $(hevm_multi_slow), $(hevm_multi_pass))


rocq-examples = tests/rocq/multi tests/rocq/transitions tests/rocq/safemath tests/rocq/exponent tests/rocq/token tests/rocq/ERC20-simple tests/rocq/ERC20  tests/rocq/amm tests/rocq/pointers

.PHONY: test-rocq $(rocq-examples)
test-rocq: compiler $(rocq-examples)
$(rocq-examples):
	make -C $@ clean
	make -C $@

test-parse: parser compiler $(parser_pass:=.parse.pass) $(parser_fail:=.parse.fail)
test-type: parser compiler $(typing_pass:=.type.pass) $(typing_fail:=.type.fail)
test-invariant: parser compiler $(invariant_pass:=.invariant.pass) $(invariant_fail:=.invariant.fail)
test-postcondition: parser compiler $(postcondition_pass:=.postcondition.pass) $(postcondition_fail:=.postcondition.fail)
test-equiv: parser compiler $(hevm_pass:=.hevm.pass) $(hevm_vy_pass:=.hevm.vy.pass) $(hevm_multi_pass:=.hevm.multi.pass) $(hevm_fail:=.hevm.fail)
test-equiv-fast: parser compiler $(hevm_fast:=.hevm.pass.fast) $(hevm_vy_pass:=.hevm.vy.pass) $(hevm_multi_fast:=.hevm.multi.pass) $(hevm_fail:=.hevm.fail)
test-cabal: src/*.hs
	cabal v2-run test

# Just checks parsing
tests/%.parse.pass:
	./bin/act parse --file tests/$* > tests/$*.parsed.hs.out
	diff tests/$*.parsed.hs.out tests/$*.parsed.hs
	rm tests/$*.parsed.hs

tests/%.parse.fail:
	./bin/act parse --file tests/$* && exit 1 || echo 0

tests/%.type.pass:
	./bin/act type --file tests/$* | jq . > tests/$*.typed.json.out
	diff tests/$*.typed.json.out tests/$*.typed.json
	rm tests/$*.typed.json.out

tests/%.type.fail:
	./bin/act type --file tests/$* && exit 1 || echo 0

tests/%.invariant.pass:
	./bin/act prove --file tests/$*
	./bin/act prove --solver cvc5 --file tests/$*

tests/%.invariant.fail:
	./bin/act prove --file tests/$* && exit 1 || echo 0
	./bin/act prove --solver cvc5 --file tests/$* && exit 1 || echo 0

tests/%.postcondition.pass:
	./bin/act prove --file tests/$*
	./bin/act prove --solver cvc5 --file tests/$*

tests/%.postcondition.fail:
	./bin/act prove --file tests/$* && exit 1 || echo 0
	./bin/act prove --solver cvc5 --file tests/$* && exit 1 || echo 0

tests/hevm/pass/%.act.hevm.pass:
	$(eval CONTRACT := $(shell awk '/contract/{ print $$2 }' tests/hevm/pass/$*.sol))
	./bin/act equiv --spec tests/hevm/pass/$*.act --sol tests/hevm/pass/$*.sol --solver bitwuzla --smttimeout 100000000

tests/hevm/pass/%.act.hevm.vy.pass:
	$(eval CONTRACT := $(shell awk '/contract/{ print $$2 }' tests/hevm/pass/$*.vy))
	./bin/act equiv --spec tests/hevm/pass/$*.act --vy tests/hevm/pass/$*.vy --solver bitwuzla --smttimeout 100000000
tests/hevm/pass/%.json.hevm.multi.pass:
	./bin/act equiv --json tests/hevm/pass/$*.json --solver bitwuzla --smttimeout 100000000

tests/hevm/fail/%.act.hevm.fail:
	$(eval CONTRACT := $(shell awk '/contract/{ print $$2 }' tests/hevm/fail/$*.sol))
	./bin/act equiv --spec tests/hevm/fail/$*.act --sol tests/hevm/fail/$*.sol --solver bitwuzla && exit 1 || echo 0

tests/hevm/pass/%.act.hevm.pass.fast:
	$(eval CONTRACT := $(shell awk '/contract/{ print $$2 }' tests/hevm/pass/$*.sol))
	./bin/act equiv --spec tests/hevm/pass/$*.act --sol tests/hevm/pass/$*.sol --solver bitwuzla --smttimeout 100000000

test-ci: test-parse test-type test-rocq test-equiv-fast
test: test-ci test-cabal