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.

Sign up for GitHub

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

Jump to bottom

Allow writing function contracts in webassembly code #407

Open
wants to merge 51 commits into
base: main
Choose a base branch
from
Open

Allow writing function contracts in webassembly code #407

wants to merge 51 commits into from

Commits on Aug 30, 2024

  1. add custom annotations in ast and parser

    @Laplace-Demon
    Laplace-Demon committed Aug 30, 2024
    Configuration menu
    Copy the full SHA
    b1c607c View commit details
    Browse the repository at this point in the history

  2. add test for custom annotations

    @Laplace-Demon
    Laplace-Demon committed Aug 30, 2024
    Configuration menu
    Copy the full SHA
    0aa2bfb View commit details
    Browse the repository at this point in the history

  3. remove misplaced test file

    @Laplace-Demon
    Laplace-Demon committed Aug 30, 2024
    Configuration menu
    Copy the full SHA
    18bcfe1 View commit details
    Browse the repository at this point in the history

  4. simplify code

    @Laplace-Demon
    Laplace-Demon committed Aug 30, 2024
    Configuration menu
    Copy the full SHA
    f75e388 View commit details
    Browse the repository at this point in the history

  5. use string equality test instead of polymorphic one

    @Laplace-Demon
    Laplace-Demon committed Aug 30, 2024
    Configuration menu
    Copy the full SHA
    2e137e7 View commit details
    Browse the repository at this point in the history

  6. add pretty-printer of annotations

    @Laplace-Demon
    Laplace-Demon committed Aug 30, 2024
    Configuration menu
    Copy the full SHA
    7fabad7 View commit details
    Browse the repository at this point in the history

  7. Adopt to Prelude

    @Laplace-Demon
    Laplace-Demon committed Aug 30, 2024
    Configuration menu
    Copy the full SHA
    9732b1d View commit details
    Browse the repository at this point in the history

  8. delete Fmt qualified name

    @Laplace-Demon
    Laplace-Demon committed Aug 30, 2024
    Configuration menu
    Copy the full SHA
    dcecb0b View commit details
    Browse the repository at this point in the history

  9. use hashmap to reord annotations

    @Laplace-Demon
    Laplace-Demon committed Aug 30, 2024
    Configuration menu
    Copy the full SHA
    f1c96d9 View commit details
    Browse the repository at this point in the history

  10. use s-expression to store annotations

    @Laplace-Demon
    Laplace-Demon committed Aug 30, 2024
    Configuration menu
    Copy the full SHA
    8fa8722 View commit details
    Browse the repository at this point in the history

  11. add function contract annotations

    @Laplace-Demon
    Laplace-Demon committed Aug 30, 2024
    Configuration menu
    Copy the full SHA
    2c6b5e6 View commit details
    Browse the repository at this point in the history

  12. replace let* with let+

    @Laplace-Demon
    Laplace-Demon committed Aug 30, 2024
    Configuration menu
    Copy the full SHA
    ff2ec9c View commit details
    Browse the repository at this point in the history

  13. definition of function contracts

    @Laplace-Demon
    Laplace-Demon committed Aug 30, 2024
    Configuration menu
    Copy the full SHA
    18bb3e1 View commit details
    Browse the repository at this point in the history

  14. add custom section to binary module

    @Laplace-Demon
    Laplace-Demon committed Aug 30, 2024
    Configuration menu
    Copy the full SHA
    76d7b53 View commit details
    Browse the repository at this point in the history

  15. add function contracts as one kind of annotation, to be parsed either… 

    … from s-expressions or directly from code
    @Laplace-Demon
    Laplace-Demon committed Aug 30, 2024
    Configuration menu
    Copy the full SHA
    240b77a View commit details
    Browse the repository at this point in the history

  16. remove duplicate pattern

    @Laplace-Demon
    Laplace-Demon committed Aug 30, 2024
    Configuration menu
    Copy the full SHA
    21b93f6 View commit details
    Browse the repository at this point in the history

  17. parse function contract

    @Laplace-Demon
    Laplace-Demon committed Aug 30, 2024
    Configuration menu
    Copy the full SHA
    08c3699 View commit details
    Browse the repository at this point in the history

  18. add annotations to text_to_binary

    @Laplace-Demon
    Laplace-Demon committed Aug 30, 2024
    Configuration menu
    Copy the full SHA
    9511220 View commit details
    Browse the repository at this point in the history

  19. fix parser

    @Laplace-Demon
    Laplace-Demon committed Aug 30, 2024
    Configuration menu
    Copy the full SHA
    7111a13 View commit details
    Browse the repository at this point in the history

  20. delete quantified variable name in the process of rewrite

    @Laplace-Demon
    Laplace-Demon committed Aug 30, 2024
    Configuration menu
    Copy the full SHA
    3187bd8 View commit details
    Browse the repository at this point in the history

  21. better pretty printer

    @Laplace-Demon
    Laplace-Demon committed Aug 30, 2024
    Configuration menu
    Copy the full SHA
    7f7f87b View commit details
    Browse the repository at this point in the history

  22. add unfinished test of spec

    @Laplace-Demon
    Laplace-Demon committed Aug 30, 2024
    Configuration menu
    Copy the full SHA
    e4920d4 View commit details
    Browse the repository at this point in the history

  23. add rewriting for function parameters

    @Laplace-Demon
    Laplace-Demon committed Aug 30, 2024
    Configuration menu
    Copy the full SHA
    8885690 View commit details
    Browse the repository at this point in the history

  24. small fixes

    @Laplace-Demon
    Laplace-Demon committed Aug 30, 2024
    Configuration menu
    Copy the full SHA
    8e916ab View commit details
    Browse the repository at this point in the history

  25. fix

    @Laplace-Demon
    Laplace-Demon committed Aug 30, 2024
    Configuration menu
    Copy the full SHA
    49909b7 View commit details
    Browse the repository at this point in the history

  26. rename Int32.to_string to Int32.to_string_exn 

    rename Int32.to_string_opt to Int32.to_string
same for Int64, Float32, Float64
    @Laplace-Demon
    Laplace-Demon committed Aug 30, 2024
    Configuration menu
    Copy the full SHA
    6c76976 View commit details
    Browse the repository at this point in the history

  27. replace optional arguments with labeled arguments in rewrite.ml

    @Laplace-Demon
    Laplace-Demon committed Aug 30, 2024
    Configuration menu
    Copy the full SHA
    8b79776 View commit details
    Browse the repository at this point in the history

  28. allow nicer symbols to be parsed

    @Laplace-Demon
    Laplace-Demon committed Aug 30, 2024
    Configuration menu
    Copy the full SHA
    ea5d14f View commit details
    Browse the repository at this point in the history

  29. deal with error when merging

    @Laplace-Demon
    Laplace-Demon committed Aug 30, 2024
    Configuration menu
    Copy the full SHA
    8632890 View commit details
    Browse the repository at this point in the history

  30. add cmdline option for code generation

    @Laplace-Demon
    Laplace-Demon committed Aug 30, 2024
    Configuration menu
    Copy the full SHA
    574dc99 View commit details
    Browse the repository at this point in the history

  31. add owi header

    @Laplace-Demon
    Laplace-Demon committed Aug 30, 2024
    Configuration menu
    Copy the full SHA
    fb31c05 View commit details
    Browse the repository at this point in the history

  32. framework for rac code generation

    @Laplace-Demon
    Laplace-Demon committed Aug 30, 2024
    Configuration menu
    Copy the full SHA
    3b19c74 View commit details
    Browse the repository at this point in the history

  33. fix some tests by adding proper exceptions

    @Laplace-Demon
    Laplace-Demon committed Aug 30, 2024
    Configuration menu
    Copy the full SHA
    81b0bf5 View commit details
    Browse the repository at this point in the history

  34. make rac a subcommand of owi

    @Laplace-Demon
    Laplace-Demon committed Aug 30, 2024
    Configuration menu
    Copy the full SHA
    ebf9a50 View commit details
    Browse the repository at this point in the history

  35. promote some tests

    @Laplace-Demon
    Laplace-Demon committed Aug 30, 2024
    Configuration menu
    Copy the full SHA
    4e96795 View commit details
    Browse the repository at this point in the history

  36. add 'unclosed annotation', 'unclosed comment' and 'unclosed string'

    @Laplace-Demon
    Laplace-Demon committed Aug 30, 2024
    Configuration menu
    Copy the full SHA
    77d1884 View commit details
    Browse the repository at this point in the history

  37. accomodate binary module simplification

    @Laplace-Demon
    Laplace-Demon committed Aug 30, 2024
    Configuration menu
    Copy the full SHA
    9aceccf View commit details
    Browse the repository at this point in the history

  38. fix

    @Laplace-Demon
    Laplace-Demon committed Aug 30, 2024
    Configuration menu
    Copy the full SHA
    5046234 View commit details
    Browse the repository at this point in the history

  39. add bounded quantification

    @Laplace-Demon
    Laplace-Demon committed Aug 30, 2024
    Configuration menu
    Copy the full SHA
    4c1795b View commit details
    Browse the repository at this point in the history

  40. fix operator tests

    @Laplace-Demon
    Laplace-Demon committed Aug 30, 2024
    Configuration menu
    Copy the full SHA
    dbdd1a2 View commit details
    Browse the repository at this point in the history

  41. add rac tests

    @Laplace-Demon
    Laplace-Demon committed Aug 30, 2024
    Configuration menu
    Copy the full SHA
    873d937 View commit details
    Browse the repository at this point in the history

  42. rename rac to instrument

    @Laplace-Demon
    Laplace-Demon committed Aug 30, 2024
    Configuration menu
    Copy the full SHA
    4d547f6 View commit details
    Browse the repository at this point in the history

  43. add option --symbolic to owi instrument

    @Laplace-Demon
    Laplace-Demon committed Aug 30, 2024
    Configuration menu
    Copy the full SHA
    711790c View commit details
    Browse the repository at this point in the history

  44. add options --rac and --srac

    @Laplace-Demon
    Laplace-Demon committed Aug 30, 2024
    Configuration menu
    Copy the full SHA
    3517a43 View commit details
    Browse the repository at this point in the history

Commits on Sep 2, 2024

  1. add memory instruction

    @Laplace-Demon
    Laplace-Demon committed Sep 2, 2024
    Configuration menu
    Copy the full SHA
    74fbb57 View commit details
    Browse the repository at this point in the history

Commits on Sep 6, 2024

  1. remove unused owi functions

    @Laplace-Demon
    Laplace-Demon committed Sep 6, 2024
    Configuration menu
    Copy the full SHA
    4ed6c6e View commit details
    Browse the repository at this point in the history

  2. changes.md

    @Laplace-Demon
    Laplace-Demon committed Sep 6, 2024
    Configuration menu
    Copy the full SHA
    e176356 View commit details
    Browse the repository at this point in the history

  3. add weasel example

    @Laplace-Demon
    Laplace-Demon committed Sep 6, 2024
    Configuration menu
    Copy the full SHA
    916ae44 View commit details
    Browse the repository at this point in the history

  4. readd owi run --rac

    @Laplace-Demon
    Laplace-Demon committed Sep 6, 2024
    Configuration menu
    Copy the full SHA
    681a2b4 View commit details
    Browse the repository at this point in the history

  5. link assert_i32 in cmd_run

    @Laplace-Demon
    Laplace-Demon committed Sep 6, 2024
    Configuration menu
    Copy the full SHA
    d0c7c95 View commit details
    Browse the repository at this point in the history

Commits on Sep 17, 2024

  1. add assert.wat in test

    @Laplace-Demon
    Laplace-Demon committed Sep 17, 2024
    Configuration menu
    Copy the full SHA
    f39e443 View commit details
    Browse the repository at this point in the history