Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Allow writing function contracts in webassembly code #407

Merged
merged 51 commits into from
Nov 16, 2024
Merged
Changes from 1 commit
Commits
Show all changes
51 commits
Select commit Hold shift + click to select a range
b1c607c
add custom annotations in ast and parser
Laplace-Demon Jul 18, 2024
0aa2bfb
add test for custom annotations
Laplace-Demon Jul 18, 2024
18bcfe1
remove misplaced test file
Laplace-Demon Jul 19, 2024
f75e388
simplify code
Laplace-Demon Jul 19, 2024
2e137e7
use string equality test instead of polymorphic one
Laplace-Demon Jul 19, 2024
7fabad7
add pretty-printer of annotations
Laplace-Demon Jul 19, 2024
9732b1d
Adopt to Prelude
Laplace-Demon Jul 23, 2024
dcecb0b
delete Fmt qualified name
Laplace-Demon Jul 23, 2024
f1c96d9
use hashmap to reord annotations
Laplace-Demon Jul 26, 2024
8fa8722
use s-expression to store annotations
Laplace-Demon Jul 27, 2024
2c6b5e6
add function contract annotations
Laplace-Demon Jul 29, 2024
ff2ec9c
replace let* with let+
Laplace-Demon Jul 29, 2024
18bb3e1
definition of function contracts
Laplace-Demon Jul 31, 2024
76d7b53
add custom section to binary module
Laplace-Demon Jul 31, 2024
240b77a
add function contracts as one kind of annotation, to be parsed either…
Laplace-Demon Aug 2, 2024
21b93f6
remove duplicate pattern
Laplace-Demon Aug 12, 2024
08c3699
parse function contract
Laplace-Demon Aug 12, 2024
9511220
add annotations to text_to_binary
Laplace-Demon Aug 12, 2024
7111a13
fix parser
Laplace-Demon Aug 12, 2024
3187bd8
delete quantified variable name in the process of rewrite
Laplace-Demon Aug 12, 2024
7f7f87b
better pretty printer
Laplace-Demon Aug 12, 2024
e4920d4
add unfinished test of spec
Laplace-Demon Aug 12, 2024
8885690
add rewriting for function parameters
Laplace-Demon Aug 13, 2024
8e916ab
small fixes
Laplace-Demon Aug 13, 2024
49909b7
fix
Laplace-Demon Aug 13, 2024
6c76976
rename Int32.to_string to Int32.to_string_exn
Laplace-Demon Aug 13, 2024
8b79776
replace optional arguments with labeled arguments in rewrite.ml
Laplace-Demon Aug 13, 2024
ea5d14f
allow nicer symbols to be parsed
Laplace-Demon Aug 13, 2024
8632890
deal with error when merging
Laplace-Demon Aug 13, 2024
574dc99
add cmdline option for code generation
Laplace-Demon Aug 13, 2024
fb31c05
add owi header
Laplace-Demon Aug 15, 2024
3b19c74
framework for rac code generation
Laplace-Demon Aug 18, 2024
81b0bf5
fix some tests by adding proper exceptions
Laplace-Demon Aug 21, 2024
ebf9a50
make rac a subcommand of owi
Laplace-Demon Aug 21, 2024
4e96795
promote some tests
Laplace-Demon Aug 21, 2024
77d1884
add 'unclosed annotation', 'unclosed comment' and 'unclosed string'
Laplace-Demon Aug 21, 2024
9aceccf
accomodate binary module simplification
Laplace-Demon Aug 22, 2024
5046234
fix
Laplace-Demon Aug 22, 2024
4c1795b
add bounded quantification
Laplace-Demon Aug 26, 2024
dbdd1a2
fix operator tests
Laplace-Demon Aug 27, 2024
873d937
add rac tests
Laplace-Demon Aug 27, 2024
4d547f6
rename rac to instrument
Laplace-Demon Aug 27, 2024
711790c
add option `--symbolic` to `owi instrument`
Laplace-Demon Aug 27, 2024
3517a43
add options --rac and --srac
Laplace-Demon Aug 27, 2024
4ed6c6e
remove unused owi functions
Laplace-Demon Aug 27, 2024
74fbb57
add memory instruction
Laplace-Demon Sep 2, 2024
e176356
changes.md
Laplace-Demon Sep 6, 2024
916ae44
add weasel example
Laplace-Demon Sep 6, 2024
681a2b4
readd owi run --rac
Laplace-Demon Sep 6, 2024
d0c7c95
link assert_i32 in cmd_run
Laplace-Demon Sep 6, 2024
f39e443
add assert.wat in test
Laplace-Demon Sep 17, 2024
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
deal with error when merging
Laplace-Demon committed Aug 30, 2024
commit 86328903f1444662e9f82714fabfe3d5a14ef0f8
4 changes: 2 additions & 2 deletions src/text_to_binary/rewrite.ml
Original file line number Diff line number Diff line change
@@ -511,10 +511,10 @@ let modul (modul : Assigned.t) : Binary.modul Result.t =
let* types = rewrite_named (rewrite_types modul) modul.typ in
let* start =
match modul.start with
| None -> None
| None -> Ok None
| Some id ->
let (Raw id) = find func id in
Some id
Ok (Some id)
in

let id = modul.id in