Start conversion to easy-smt by sampsyo · Pull Request #45 · avanhatt/wasmtime

sampsyo · 2023-01-21T03:11:59Z

As discussed on Slack, here's a first attempt to move from rsmt2 to easy-smt. Here are the high-level takeaways:

The actual interaction with the solver was easy to move over. No problem! Just had to fiddle around with the APIs to line them up.
The real work here is the drudgery of changing from plain ol' strings for the SMT expressions to the library's SExpr type.

I got everything in solver.rs converted, including all the SMT generation and the interaction with the solver. This took me about 3 hours to move everything over—almost all of that was replacing calls to format! with explicit S-expression construction calls. It's not exactly fun, but it's not exactly hard either.

There is more drudgery ahead: the files in encoded_ops have a lot of raw SMT strings in them and will be a lot of work to convert.

There is a chance I have made a terrible mistake and I should not have tried to do all this annoying conversion at all: instead, we could try to parse the strings we're already generating and turn them into SExprs. Or we could attempt to hack easy-smt to allow us to shove strings directly into the solver, which it doesn't currently allow (you have to provide an SExpr). Both of those seem very reasonable in retrospect, but now I wonder if either of them would be simpler than just forging ahead and finishing the conversion. I'd be interested in others' opinions, given what the code looks like in solver.rs after the conversion.

I tried to do this as fast as I could, not trying to clean anything up after the transition, and just get the replacement done as quickly as possible. (And it still took me about 3 hours.) The main work, of course, is replacing all the raw string manipulation (mainly `format!` calls) with S-expression builder calls.

There is a lot of typing to be done here!

avanhatt · 2023-01-23T20:24:41Z

cranelift/isle/veri/veri_engine/src/solver.rs

    }

-    let assumption_str = format!("(and {})", assumptions.join(" "));
+    let assumption_conjunction = solver.and_many(assumptions);


I'm trying to get to a place where the crate compiles, even though the encoded ops don't work at all.

sampsyo · 2023-01-24T04:43:37Z

As we discussed synchronously today, I've mucked things up so that our crate builds. That meant temporarily:

removing the files under encoded_ops
replacing the calls into their SMT-generating functions with todo!()

It works! I haven't tried running any tests, because I don't feel qualified to know which tests should be runnable in this semi-broken state. (I could probably figure that out, but I'm going to move on to trying to rewrite the encoded ops stuff instead of spending time on that.)

Now using the builder to construct contexts. And there's a cool new `numeral` helper for building number literals of all kinds!

avanhatt · 2023-01-24T16:24:32Z

cranelift/isle/veri/veri_engine/src/solver.rs

    }

-    pub fn vir_to_rsmt2_constant_ty(&self, ty: &Type) -> String {
+    pub fn vir_to_rsmt2_constant_ty(&self, ty: &Type) -> SExpr {


nit: remove rsmt2 from name

Thanks; addressed!

Apparently, `findall` returns a list of strings (not tuples) when there is only one subgroup.

To match clz*.

avanhatt · 2023-01-25T15:01:07Z

Other important TODO before this becomes the default: easy-smt's debugging doesn't list the actual values. We should make sure things like this get displayed in a more useful way:

Assertion list is feasible
LHS and RHS equality condition:
        SExpr::List(14853)            // <- this should have named values

avanhatt · 2023-01-25T15:05:43Z

^ Doing a pass to add ctx.smt.display(...) calls.

avanhatt · 2023-01-25T15:29:57Z

Currently failing tests:

failures:
2363
test_broken_uextend
2364
test_clz
2365
test_ctz
2366
test_ctz_broken
2367
test_sextend
2368
test_uextend

avanhatt · 2023-01-25T17:42:34Z

cranelift/isle/veri/veri_engine/src/solver.rs

                    }
-                    Type::Int => i.to_string(),
+                    Type::Int => self.smt.numeral(i),
                    Type::Bool => {


Aha, I think this is causing the failing tests! Will fix.

Oh Lordy, that is obviously wrong!! Nice catch!

@mpardeshi

Based on @mpardeshi's advice, this is just a copy of `rev32` but with an extra extract at the top. I hope this works.

That's the last one, hopefully!

avanhatt · 2023-01-26T16:36:26Z

Ok, I think the clz and ctz encodings might actually be broken. Investigating!

mpardesh · 2023-01-30T21:31:26Z

cranelift/isle/veri/encodings/clz16.smt2

+
+(assert (= y1_{id} (bvlshr x2_{id} #x0001)))
+(assert (ite (not (= y1_{id} (_ bv0 16))) (= ret5_{id} ret4_{id}) (= ret5_{id} (bvadd ret4_{id} (_ bv1 16)))))
+(assert (ite (not (= y1_{id} (_ bv0 16))) (= x1_{id} y1_{id}) (= x1_{id} x2_{id})))


after this line, try adding

; last round (declare-fun ret6_{id} () (_ BitVec 16)) (assert (ite (not (= x1_{id} (_ bv0 16))) (= ret6_{id} ret5_{id}) (= ret6_{id} (bvadd ret5_{id} (_ bv1 16)))))

and then regenerating?

Aha, good catch! Trying this now

mpardesh · 2023-01-30T21:33:10Z

cranelift/isle/veri/encodings/clz32.smt2

+
+(assert (= y1_{id} (bvlshr x2_{id} #x00000001)))
+(assert (ite (not (= y1_{id} (_ bv0 32))) (= ret5_{id} ret4_{id}) (= ret5_{id} (bvadd ret4_{id} (_ bv1 32)))))
+(assert (ite (not (= y1_{id} (_ bv0 32))) (= x1_{id} y1_{id}) (= x1_{id} x2_{id})))


after this line try adding:

; last round (declare-fun ret6_{id} () (_ BitVec 32)) (assert (ite (not (= x1_{id} (_ bv0 32))) (= ret6_{id} ret5_{id}) (= ret6_{id} (bvadd ret5_{id} (_ bv1 32)))))

and then regenerating?

mpardesh · 2023-01-30T21:34:28Z

cranelift/isle/veri/encodings/clz64.smt2

+
+(assert (= y1_{id} (bvlshr x2_{id} #x0000000000000001)))
+(assert (ite (not (= y1_{id} (_ bv0 64))) (= ret6_{id} ret5_{id}) (= ret6_{id} (bvadd ret5_{id} (_ bv1 64)))))
+(assert (ite (not (= y1_{id} (_ bv0 64))) (= x1_{id} y1_{id}) (= x1_{id} x2_{id})))


after this line try adding

; last round (declare-fun ret7_{id} () (_ BitVec 64)) (assert (ite (not (= x1_{id} (_ bv0 64))) (= ret7_{id} ret6_{id}) (= ret7_{id} (bvadd ret6_{id} (_ bv1 64)))))

and then regenerating?

* implement `wasi-filesystem::readdir` and related functions This adds a `directory_list` test and provides the required host implementation. I've also added a file length check to the `file_read` test, just to cover a bit more of the API. Signed-off-by: Joel Dice <joel.dice@fermyon.com> * fix memory corruption in `fd_readdir` polyfill We were copying `name.len() * 256` bytes instead of just `name.len()` bytes, which was overwriting other parts of `State` and causing untold havoc. Signed-off-by: Joel Dice <joel.dice@fermyon.com> * check type of entry in `Table::delete` Signed-off-by: Joel Dice <joel.dice@fermyon.com> Signed-off-by: Joel Dice <joel.dice@fermyon.com>

Add support for fetching models containing unspecified values. With the addition of declared sorts in bytecodealliance#141, this broke the code that parses constants from SMT models. The backend solvers differ on how they implement this. This PR deals with the CVC5 format only, in which unspecified values are represented as something like `(as @Unspecified_0 Unspecified)`. Updates avanhatt#45

Since the addition of enum type instantiations bytecodealliance#167 the counter-example printing is bloated with a lot of enum variants. These convey little information if they are constants (unit enums). This PR skips them in printing. Updates avanhatt#45

sampsyo added 4 commits January 20, 2023 18:49

Try attempting to convert clz encoding...

a948e7e

There is a lot of typing to be done here!

Try pre-declaring some atoms

3742367

Add a declare helper

b978079

avanhatt mentioned this pull request Jan 23, 2023

Investigate replacing rsmt2 with easy-smt #29

Closed

avanhatt reviewed Jan 23, 2023

View reviewed changes

sampsyo added 2 commits January 23, 2023 20:25

Temporarily disable encoded ops

7ca7a25

I'm trying to get to a place where the crate compiles, even though the encoded ops don't work at all.

Satisfy the borrow checker

a2e766f

sampsyo added 5 commits January 23, 2023 21:04

Try converting one rev function

8ac0ab2

Add a simple assume helper

9aec52c

Update to latest easy-smt

2b9fd74

Now using the builder to construct contexts. And there's a cool new `numeral` helper for building number literals of all kinds!

Add back rev with one working function & test

103fa21

More reusable test framework

d67216c

avanhatt reviewed Jan 24, 2023

View reviewed changes

sampsyo added 15 commits January 24, 2023 08:51

Add encoding files from @mpardesh

37af828

Minor Python cleanup

1ad8b53

Generate easy-smt code for declarations

68b2b87

Convert assertions to easy-smt

be72950

Slight Python cleanup

7c07a46

Bind Rust variables for SMT variable names (atoms)

d1c2147

Slightly simplify some generated Rust

d4edcba

Finish test for rev1

975c3df

Fix variable names

25db314

Apparently, `findall` returns a list of strings (not tuples) when there is only one subgroup.

Use generated code for rev1

0cf6d5e

Generate code for remaining rev*

3109690

Re-enable calls to rev*

f13bb5b

Rename cls* SMT files for consistency

b5aaaeb

To match clz*.

Clean up test SMT declarations

14c338d

Use proper convention for return variables

ea07cdb

better printing/logging

66fa584

avanhatt reviewed Jan 25, 2023

View reviewed changes

avanhatt and others added 8 commits January 25, 2023 13:51

fix boolean literals, better model display

5666d38

Add rev tests that hit the solver

8d3e129

Try writing rbit32 in raw SMT

f16dd94

Based on @mpardeshi's advice, this is just a copy of `rev32` but with an extra extract at the top. I hope this works.

Generate rbit32

7cf19e1

That's the last one, hopefully!

Run tests with timeout and retry attempt

bd270c5

actually retry, longer timeout

77945ba

Merge branch 'verify-main' into easy-smt

57f8717

fix test output on failed test

e536a4c

avanhatt added 2 commits January 30, 2023 12:04

Add more encoding tests (some failing)

0577aa0

more

a7f63a9

mpardesh reviewed Jan 30, 2023

View reviewed changes

avanhatt added 3 commits January 30, 2023 22:36

final rounds for clzs

bb478d7

Merge branch 'verify-main' into easy-smt

87a54fb

fix 64 case, add tests for cls encoding

a8b074e

avanhatt marked this pull request as ready for review January 31, 2023 15:26

avanhatt approved these changes Jan 31, 2023

View reviewed changes

avanhatt merged commit 61c88f5 into verify-main Jan 31, 2023

Conversation

sampsyo commented Jan 21, 2023

Uh oh!

Choose a reason for hiding this comment

Uh oh!

sampsyo commented Jan 24, 2023

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

avanhatt commented Jan 25, 2023

Uh oh!

avanhatt commented Jan 25, 2023

Uh oh!

avanhatt commented Jan 25, 2023

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

avanhatt commented Jan 26, 2023

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants