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

Measure inference #721

Merged
merged 67 commits into from
Jan 29, 2020
Merged

Measure inference #721

merged 67 commits into from
Jan 29, 2020

Commits on Jan 21, 2020

  1. Add phase semantics to every phase

    @romac
    romac committed Jan 21, 2020
    Configuration menu
    Copy the full SHA
    501fae9 View commit details
    Browse the repository at this point in the history

  2. Remove termination package

    @romac
    romac committed Jan 21, 2020
    Configuration menu
    Copy the full SHA
    b5bdb70 View commit details
    Browse the repository at this point in the history

  3. Port over @RJaya's work on measure inference

    @romac
    romac committed Jan 21, 2020
    Configuration menu
    Copy the full SHA
    cb78fa9 View commit details
    Browse the repository at this point in the history

  4. Update copyright year

    @romac
    romac committed Jan 21, 2020
    Configuration menu
    Copy the full SHA
    5816cd1 View commit details
    Browse the repository at this point in the history

  5. Refactor MeasureAnnotation phase

    @romac
    romac committed Jan 21, 2020
    Configuration menu
    Copy the full SHA
    f272ce5 View commit details
    Browse the repository at this point in the history

  6. Fix user-defined decreases

    @romac
    romac committed Jan 21, 2020
    Configuration menu
    Copy the full SHA
    91ee0bd View commit details
    Browse the repository at this point in the history

Commits on Jan 27, 2020

  1. Attempt to fix ChainProcessor

    @romac
    romac committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    81155a4 View commit details
    Browse the repository at this point in the history

  2. Re-add --termination option and only enforce measures when on

    @romac
    romac committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    f0c20ea View commit details
    Browse the repository at this point in the history

  3. Rename MeasureAnnotation phase to MeasureInference

    @romac
    romac committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    f99696c View commit details
    Browse the repository at this point in the history

  4. Remove unused SizeInjection phase

    @romac
    romac committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    e59c1d0 View commit details
    Browse the repository at this point in the history

  5. Make TypeChecker more lenient when a measure is missing (ie. do not c… 

    …rash)
    @romac
    romac committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    cb04f97 View commit details
    Browse the repository at this point in the history

  6. Staged decrease inference in ChainProcessor

    @romac
    romac committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    9efb1d8 View commit details
    Browse the repository at this point in the history

  7. Add --infer-measures option to toggle measure inference phase

    @romac
    romac committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    4bd32f5 View commit details
    Browse the repository at this point in the history

  8. Rename --termination to --check-measures

    @romac
    romac committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    4535670 View commit details
    Browse the repository at this point in the history

  9. Annotate non-terminating functions with @nonTerminating(reason, msg)

    @romac
    romac committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    d21a07a View commit details
    Browse the repository at this point in the history

  10. Initial work on measure-based TerminationSuite

    @romac
    romac committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    fb2a556 View commit details
    Browse the repository at this point in the history

  11. Add VC filter to TypeChecker

    @romac
    romac committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    3d0657f View commit details
    Browse the repository at this point in the history

  12. Fix small bug in typechecker

    @romac
    romac committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    bf8582c View commit details
    Browse the repository at this point in the history

  13. Record time spent inferring measures

    @romac
    romac committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    fcb2eb3 View commit details
    Browse the repository at this point in the history

  14. Add missing paren in help message

    @romac
    romac committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    a217923 View commit details
    Browse the repository at this point in the history

  15. Cleanup ChainProcessor

    @romac
    romac committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    29dabb7 View commit details
    Browse the repository at this point in the history

  16. Change --check-measures to take "yes", "no", or "only". 

    The latter option instructs the type-checker to only emit VCs related to measures.
    @romac
    romac committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    08a583b View commit details
    Browse the repository at this point in the history

  17. Rework the termination test suite to work with the type-checker

    @romac
    romac committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    8ee670d View commit details
    Browse the repository at this point in the history

  18. Annotate functions in termination benchmarks for which we cannot infe… 

    …r a measure
    @romac
    romac committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    33e51db View commit details
    Browse the repository at this point in the history

  19. Add inference rules for foralls and chooses

    @romac
    romac committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    34b30de View commit details
    Browse the repository at this point in the history

  20. Skip a few benchmarks which are not compatible with System FR type-ch… 

    …ecker
    @romac
    romac committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    3ada88a View commit details
    Browse the repository at this point in the history

  21. Disable reporting

    @romac
    romac committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    907c913 View commit details
    Browse the repository at this point in the history

  22. Fix termination test suite

    @romac
    romac committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    475b417 View commit details
    Browse the repository at this point in the history

  23. Make sure to add all required size functions to the symbols

    @romac
    romac committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    da97483 View commit details
    Browse the repository at this point in the history

  24. Cleanup

    @romac
    romac committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    cfd2dbb View commit details
    Browse the repository at this point in the history

  25. Add stub typechecking rule for Passes

    @romac
    romac committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    3b59c55 View commit details
    Browse the repository at this point in the history

  26. Fix IntSetProp benchmark for type checker

    @romac
    romac committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    c6e4893 View commit details
    Browse the repository at this point in the history

  27. Skip benchmarks which fail termination checks because of various bugs

    @romac
    romac committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    3a5b34c View commit details
    Browse the repository at this point in the history

  28. Run TypeCheckerSuite on standard valid verification benchmarks

    @romac
    romac committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    c51bf5f View commit details
    Browse the repository at this point in the history

  29. Add measures to BottomUpMergeSort

    @romac
    romac committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    5acfe0f View commit details
    Browse the repository at this point in the history

  30. Cleanup HOTermination benchmark

    @romac
    romac committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    3bc0ae2 View commit details
    Browse the repository at this point in the history

  31. Add ListOps.sum

    @romac
    romac committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    b24f752 View commit details
    Browse the repository at this point in the history

  32. Mark broken termination benchmarks as Ignore instead of Skip

    @romac
    romac committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    c49e5d4 View commit details
    Browse the repository at this point in the history

  33. Fix 'adt invariant' VC emitted by typechecker

    @romac
    romac committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    933807e View commit details
    Browse the repository at this point in the history

  34. Small refactor of parts of TypeChecker

    @romac
    romac committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    7187d2d View commit details
    Browse the repository at this point in the history

  35. Fix issue with laws and typechecker

    @romac
    romac committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    f1d92ce View commit details
    Browse the repository at this point in the history

  36. Emit choose satisfiability VC in typechecker

    @romac
    romac committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    43cc4b3 View commit details
    Browse the repository at this point in the history

  37. Fix bug where duplicated super methods were wrongly considered to be … 

    …abstract
    @romac
    romac committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    3140add View commit details
    Browse the repository at this point in the history

  38. Enable typechecker on invalid benchmarks in TypeCheckerSuite

    @romac
    romac committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    36ac021 View commit details
    Browse the repository at this point in the history

  39. Better handling of @unchecked expressions in typechecker

    @romac
    romac committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    69a5066 View commit details
    Browse the repository at this point in the history

  40. Do not infer measure during ExtractionSuite

    @romac
    romac committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    952f797 View commit details
    Browse the repository at this point in the history

  41. Add missing benchmarks to SMTCVC4TypeCheckerSuite's ignored benchmarks

    @romac
    romac committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    a6455fb View commit details
    Browse the repository at this point in the history

  42. Improve error message raised when calling non-visible mutually recurs… 

    …ive function
    @romac
    romac committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    b46351d View commit details
    Browse the repository at this point in the history

  43. Skip termination benchmarks already correctly rejected by the type ch… 

    …ecker
    @romac
    romac committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    aa50f3b View commit details
    Browse the repository at this point in the history

  44. Add inference rule for require clauses 

    This is needed to type-check lambdas with preconditions.
    @romac
    romac committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    a5f4375 View commit details
    Browse the repository at this point in the history

  45. Add TypeCheckerLibrarySuite with measure inference

    @romac
    romac committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    2e35953 View commit details
    Browse the repository at this point in the history

  46. Make bin/ scripts work on macOS

    @romac
    romac committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    259b084 View commit details
    Browse the repository at this point in the history

  47. Add missing serializers for termination status annotation

    @romac
    romac committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    6f64887 View commit details
    Browse the repository at this point in the history

  48. Do not run actors test suite twice unnecessarily

    @romac
    romac committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    ebffd46 View commit details
    Browse the repository at this point in the history

  49. Move measure inference out of extraction pipeline

    @romac
    romac committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    ec16c39 View commit details
    Browse the repository at this point in the history

  50. Add a couple comments

    @romac
    romac committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    d1c344a View commit details
    Browse the repository at this point in the history

  51. Fix or ignore more failing benchmarks

    @romac
    romac committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    d3a833a View commit details
    Browse the repository at this point in the history

  52. Remove slow/fast discrimination for benchmarks

    @romac
    romac committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    3552dff View commit details
    Browse the repository at this point in the history

  53. Update ignored benchmarks

    @romac
    romac committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    53f1463 View commit details
    Browse the repository at this point in the history

  54. Link related issue to ignored termination benchmarks

    @romac
    romac committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    f19a9e3 View commit details
    Browse the repository at this point in the history

  55. Add a bit more logging to MeasureInference phase

    @romac
    romac committed Jan 27, 2020
    Configuration menu
    Copy the full SHA
    3b2469a View commit details
    Browse the repository at this point in the history

Commits on Jan 28, 2020

  1. Fix bug in VC generation within the typechecker 

    Term variables which were bound to a value were
incorrectly treated as truth values instead of
let equalities, which meant that those variables
were not turned into lets, but rather equalities which
could be disproven by the solver.

For example:

val a = 1
val b = 2
a == b

would yield

    (a == 1 && b == 2) ==> (a == b)

instead of

    val a = 1
    val b = 2
    ==>
    a == b

And thus in the first case, the solver was at liberty of
picking a = 1 and b = 1, which would make the VC valid.
    @romac
    romac committed Jan 28, 2020
    Configuration menu
    Copy the full SHA
    729e43f View commit details
    Browse the repository at this point in the history

  2. Cleanup

    @romac
    romac committed Jan 28, 2020
    Configuration menu
    Copy the full SHA
    39e6994 View commit details
    Browse the repository at this point in the history

  3. Relax mutual recursion check for functions/ADTs enough for TypeEncoding

    @romac
    romac committed Jan 28, 2020
    Configuration menu
    Copy the full SHA
    f72c3b7 View commit details
    Browse the repository at this point in the history

  4. Enable --type-checker by default

    @romac
    romac committed Jan 28, 2020
    Configuration menu
    Copy the full SHA
    cbbad05 View commit details
    Browse the repository at this point in the history

  5. Remove redundant check of postcondition type

    @romac
    romac committed Jan 28, 2020
    Configuration menu
    Copy the full SHA
    fab2861 View commit details
    Browse the repository at this point in the history

  6. Update documentation on termination checking

    @romac
    romac committed Jan 28, 2020
    Configuration menu
    Copy the full SHA
    defba07 View commit details
    Browse the repository at this point in the history