Conversation
| (UnsignedLessThanOrEqual #x09))) | ||
|
|
||
| (spec (smin x y) | ||
| (spec (smin x y) |
There was a problem hiding this comment.
Sorry, there's lots of whitespace changes. My editor is cleaning up trailing whitespace on lines.
| ;; We will represent this with a msb shift bit | ||
| ;; and a 12 bit value | ||
| ;; TODO(mbm): what was intended here? the hard-coded model was 24 bits | ||
| (model Imm12 (type (bv 24))) |
There was a problem hiding this comment.
This appears in multiple of the "broken" tests. It would have had the 24-bit model from type inference, but the comment "msb shift bit and a 12 bit value" sounds to me like it would be modeled as a 13-bit value.
There was a problem hiding this comment.
We chose to model this as the range of immediates it could encode (with require blocks further restricting it to the representable subset), instead of the 12 bits and a shift.
There was a problem hiding this comment.
But the comment is out-of-date, right?
| (type u128 (primitive u128)) | ||
|
|
||
| (model usize (type (bv 64))) | ||
| (model usize (type (bv))) |
There was a problem hiding this comment.
This was annotation_ir::Type::BitVector in the code and bv 64 in the existing (ignored) model. I reverted to what was being used in the code.
There was a problem hiding this comment.
This file contains most of the interesting changes, I think.
| ;; We will represent this with a msb shift bit | ||
| ;; and a 12 bit value | ||
| ;; TODO(mbm): what was intended here? the hard-coded model was 24 bits | ||
| (model Imm12 (type (bv 24))) |
There was a problem hiding this comment.
We chose to model this as the range of immediates it could encode (with require blocks further restricting it to the representable subset), instead of the 12 bits and a shift.
| }; | ||
| model_map.insert(type_id, ir_type); | ||
| } | ||
| ast::ModelValue::EnumValues(vals) => { |
There was a problem hiding this comment.
Weird that the diff shows this all as changing, when it mostly has not.
There was a problem hiding this comment.
I believe this was a cargo fmt thing.
| annotation_info: &mut AnnotationTypeInfo, | ||
| annotation: annotation_ir::TermSignature, | ||
| ) { | ||
| let clif_to_ir_types = HashMap::from([ |
mmcloughlin
force-pushed
the
mbm/use-models
branch
from
fb9ef58 to
72eec46
Compare
Migrate the logic in the `veri` binary into a `Runner` class. This is intended to make testing a little easier by providing a library entry point into the verifier. Updates avanhatt#79
Provides basic support for file-based tests, with a single examples of passing and broken test cases. Updates avanhatt#79
…-zero wizer.h: handle the case when wasi command main function returns non-zero code
2 participants
Currently
(model ...)declarations in ISLE are ignored. This PR implements processing for them, and replaces hard-coded types inadd_isle_constraintswith equivalent model declarations.Tests pass: