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

Fix SMTLib2 syntax for floating-point conversions #190

Merged
merged 8 commits into from
Apr 11, 2019
Merged

Fix SMTLib2 syntax for floating-point conversions #190

merged 8 commits into from
Apr 11, 2019

Commits on Apr 9, 2019

  1. Fix the syntax of the parameterized SMTLib2 functions 

    `fp.to_sbv` and `fp.to_ubv`.
    @robdockins
    robdockins committed Apr 9, 2019
    Configuration menu
    Copy the full SHA
    6ee9bcb View commit details
    Browse the repository at this point in the history

  2. Add a new crucible statement for constructing fresh floating point va… 

    …lues.

These cannot use the ordinary `fresh` construct because the base type
underlying the interpreted floating point values is not known at
CFG construction time, as it depends on the symbolic backend.
    @robdockins
    robdockins committed Apr 9, 2019
    Configuration menu
    Copy the full SHA
    51df64f View commit details
    Browse the repository at this point in the history

  3. Add crucible-syntax support for floating-point types and 

    some of the conversions to and from floating point types.
    @robdockins
    robdockins committed Apr 9, 2019
    Configuration menu
    Copy the full SHA
    82d3a75 View commit details
    Browse the repository at this point in the history

  4. Add a new convenience println statement to the crucible concrete sy… 

    …ntax.

It simply appends a newline to the string to be printed.
    @robdockins
    robdockins committed Apr 9, 2019
    Configuration menu
    Copy the full SHA
    f51836f View commit details
    Browse the repository at this point in the history

Commits on Apr 10, 2019

  1. Provide additional support for floats in crucible-syntax (equality,… 

    … if/then/else, show),

and improve error messages for float casts that fail type-checking.
    @robdockins
    robdockins committed Apr 10, 2019
    Configuration menu
    Copy the full SHA
    82f1e48 View commit details
    Browse the repository at this point in the history

  2. Tweak error message

    @robdockins
    robdockins committed Apr 10, 2019
    Configuration menu
    Copy the full SHA
    f93e44a View commit details
    Browse the repository at this point in the history

  3. Have the simulator tests in crucible-syntax attempt to discharge each 

    proof obligation, and print the result (PROVED, COUNTEREXAMPLE, or UNKNOWN).

Fix up the test golden files to match.

In addition, add a test exercising floating-point conversions.
    @robdockins
    robdockins committed Apr 10, 2019
    Configuration menu
    Copy the full SHA
    d986943 View commit details
    Browse the repository at this point in the history

Commits on Apr 11, 2019

  1. Minor tweak to error message, and code style

    @robdockins
    robdockins committed Apr 11, 2019
    Configuration menu
    Copy the full SHA
    743cb86 View commit details
    Browse the repository at this point in the history