Native Z3 interface #848

manasij7479 · 2021-06-12T00:01:51Z

*.with.overflow encoding seems mysteriously broken.
Other things work, and is about 20-30% faster than our klee+smtlib interface.
Don't merge yet.

manasij7479 · 2021-06-12T00:03:37Z

If any of you want to look:
./souper-check -souper-use-z3 filename.opt

%x:i25 = var
%y:i25 = var
%z = sadd.with.overflow %x, %y
%ov = extractvalue %z, 1
pc %ov 0:i1
%r = extractvalue %z, 0
infer %r
%r2 = addnsw %x, %y
result %r2

manasij7479 · 2021-06-12T00:59:54Z

Another weird bug, documenting here to pick up later

%A:i3 = var
%B:i3 = var
%X:i3 = var
%s = shl 1, %A
%Y = lshr %s, %B
%r = udiv %X, %Y
infer %r
%sub = sub %A, %B
%Y2 = shl 1, %sub
%r2 = udiv %X, %Y2
result %r2

z3 exprs generated:

LHS:(bvudiv %var_X (bvlshr (bvshl #b001 %var_A) %var_B))
RHS:(bvudiv %var_X (bvshl #b001 (bvsub %var_A %var_B)))
(define-fun %var_X () (_ BitVec 3)
  #b011)
(define-fun %var_A () (_ BitVec 3)
  #b101)
(define-fun %var_B () (_ BitVec 3)
  #b100)
  Invalid

regehr · 2021-06-12T01:12:46Z

nice!!
should I start to read and give feedback? I'm out hiking Sat but around other than that

manasij7479 · 2021-06-12T02:01:11Z

Another simple looking transform which doesn't verify.

%X:i8 = var
%Y:i8 = var
%c:i1 = var
%sel = select %c, %Y, 0
%r = udiv %X, %sel
infer %r
%r2 = udiv %X, %Y
result %r2

regehr · 2021-06-13T19:40:51Z

it might make you feel better to know that the problem with overflow intrinsics isn't related to path conditions, this can't be verified either:

%x:i25 = var
%y:i25 = var
%z = sadd.with.overflow %x, %y
%r = extractvalue %z, 0
infer %r
%r2 = add %x, %y
result %r2

regehr · 2021-06-13T19:51:24Z

ok so your add.with.overflow isn't computing the right result when there's overflow.

remember: always simplify the circumstances surrounding a failing test.

%x:i4 = var
%y:i4 = var
%z = sadd.with.overflow 15:i4, 2:i4
%r = extractvalue %z, 0
infer %r
result 1:i4

(this verifies using the old backend and using Alive2, but not using your new one)

regehr · 2021-06-13T20:44:50Z

this one does verify

regehr@home:~/souper-manasij$ cat foo.opt
%X:i8 = var
%Y:i8 = var
%c:i1 = var
%sel = select %c, %Y, 0
%r = udiv %X, %sel
infer %r
%r2 = udiv %X, %Y
result %r2
regehr@home:~/souper-manasij$ ./build/souper-check foo.opt -souper-double-check 
; LGTM
regehr@home:~/souper-manasij$ ./build/souper-check foo.opt -souper-double-check -souper-use-z3
PC: #b1
LHS:(bvudiv %var_X (ite (= %var_c #b1) %var_Y #x00))
RHS:(bvudiv %var_X %var_Y)
; LGTM
regehr@home:~/souper-manasij$

regehr · 2021-06-13T20:46:44Z

so does this one

regehr@home:~/souper-manasij$ cat foo.opt
%A:i3 = var
%B:i3 = var
%X:i3 = var
%s = shl 1, %A
%Y = lshr %s, %B
%r = udiv %X, %Y
infer %r
%sub = sub %A, %B
%Y2 = shl 1, %sub
%r2 = udiv %X, %Y2
result %r2
regehr@home:~/souper-manasij$ ./build/souper-check foo.opt -souper-double-check -souper-use-z3
PC: #b1
LHS:(bvudiv %var_X (bvlshr (bvshl #b001 %var_A) %var_B))
RHS:(bvudiv %var_X (bvshl #b001 (bvsub %var_A %var_B)))
; LGTM
regehr@home:~/souper-manasij$ ./build/souper-check foo.opt -souper-double-check 
; LGTM
regehr@home:~/souper-manasij$

regehr · 2021-06-13T22:02:23Z

-souper-use-z3 isn't a very informative option since we already have 2 different ways to uses Z3 and you're adding a third, please change this a bit

manasij7479 · 2021-06-13T23:46:43Z

concat order was wrong, everything seems to be working now.
This isn't integrated with synthesis yet, but all the solver checks pass.

regehr · 2021-06-14T04:22:04Z

ok, nice work!

I want a test case for timeouts using this API. do like a 1024 bit division or something like that where it has no chance whatsoever of completing.

have you tried turning off the KLEE code entirely? does everything still work in that case?

regehr · 2021-06-14T20:30:15Z

include/souper/Infer/Z3Driver.h

+  }
+  bool verify(Inst *RHS, Inst *RHSAssumptions = nullptr) {
+    Translate(RHS);
+    if (RHSAssumptions) AddConstraint(RHSAssumptions);


put the "then" part on another line please

regehr · 2021-06-14T20:31:30Z

so @manasij7479 do you want to land this and then do models in a separate pr? if so, that's fine

I want you to support (and test) Z3 timeouts in this PR though

regehr · 2021-06-14T20:35:36Z

include/souper/Infer/Z3Driver.h

+  }
+
+  bool Translate(souper::Inst *I) {
+    if (!I) return true;


on a new line

regehr · 2021-06-14T20:37:33Z

include/souper/Infer/Z3Driver.h

+
+    }
+
+    std::string Name = "";


remove unnecessary initializer

regehr · 2021-06-14T20:38:01Z

include/souper/Infer/Z3Driver.h

+      case souper::Inst::Var: {
+        Put(I, ctx.bv_const(Name.c_str(), W));
+        auto DFC = getDataflowConditions(I, IC);
+        if (DFC) AddConstraint(DFC);


put the then part on a new line

include/souper/Infer/Z3Driver.h

regehr · 2021-06-14T20:44:49Z

@manasij7479 can you explain what the changes to the alive driver are doing?

regehr · 2021-06-14T20:47:25Z

lib/Infer/Z3Driver.cpp

+
+namespace souper {
+bool isTransformationValidZ3(souper::Inst *LHS, souper::Inst *RHS,
+                           const std::vector<InstMapping> &PCs,


fix indentation

manasij7479 · 2021-06-14T20:49:23Z

AliveDriver changes are just splitting out reusable code into a separate TU.

manasij7479 · 2021-06-14T20:49:46Z

I want you to support (and test) Z3 timeouts in this PR though

Will do.

manasij7479 · 2021-06-21T05:59:12Z

Implemented but not yet tested support for timeouts.
Even for larger bitwidths, z3 tactics seem to be taking care of solving things fast.
Have to find a weird valid transformation which escapes simplification.

fvrmatteo · 2021-06-21T15:40:44Z

@manasij7479 the "weird valid transformation which escapes simplification" could be here: #738. Most likely the timeout will kick in before the synthesis candidate is verified as correct. I hope this helps and is not out of scope.

regehr · 2021-06-21T20:06:45Z

very wide division by non-constant should do it

manasij7479 · 2021-09-08T17:57:07Z

See the newer PR

manasij7479 force-pushed the z3builder branch from 8a21277 to 77bb1da Compare June 13, 2021 23:53

manasij7479 marked this pull request as ready for review June 13, 2021 23:54

regehr reviewed Jun 14, 2021

View reviewed changes

include/souper/Infer/Z3Driver.h Outdated

}

bool Translate(souper::Inst *I) {

if (!I) return true;

Copy link

Collaborator

regehr Jun 14, 2021

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

on a new line

regehr reviewed Jun 14, 2021

View reviewed changes

include/souper/Infer/Z3Driver.h Outdated

}

std::string Name = "";

Copy link

Collaborator

regehr Jun 14, 2021

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

remove unnecessary initializer

regehr reviewed Jun 14, 2021

View reviewed changes

include/souper/Infer/Z3Driver.h Outdated Show resolved Hide resolved

regehr reviewed Jun 14, 2021

View reviewed changes

manasij7479 force-pushed the z3builder branch from 77bb1da to 51add98 Compare June 21, 2021 05:57

Native Z3 interface

774c79b

manasij7479 force-pushed the z3builder branch from 51add98 to 774c79b Compare June 21, 2021 17:06

manasij7479 closed this Sep 8, 2021

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Native Z3 interface #848

Native Z3 interface #848

manasij7479 commented Jun 12, 2021

manasij7479 commented Jun 12, 2021

manasij7479 commented Jun 12, 2021

regehr commented Jun 12, 2021

manasij7479 commented Jun 12, 2021

regehr commented Jun 13, 2021

regehr commented Jun 13, 2021 •

edited

Loading

regehr commented Jun 13, 2021

regehr commented Jun 13, 2021 •

edited

Loading

regehr commented Jun 13, 2021

manasij7479 commented Jun 13, 2021

regehr commented Jun 14, 2021

regehr Jun 14, 2021

regehr commented Jun 14, 2021

regehr Jun 14, 2021

regehr Jun 14, 2021

regehr Jun 14, 2021

regehr commented Jun 14, 2021

regehr Jun 14, 2021

manasij7479 commented Jun 14, 2021

manasij7479 commented Jun 14, 2021

manasij7479 commented Jun 21, 2021

fvrmatteo commented Jun 21, 2021

regehr commented Jun 21, 2021

manasij7479 commented Sep 8, 2021

Native Z3 interface #848

Native Z3 interface #848

Conversation

manasij7479 commented Jun 12, 2021

manasij7479 commented Jun 12, 2021

manasij7479 commented Jun 12, 2021

regehr commented Jun 12, 2021

manasij7479 commented Jun 12, 2021

regehr commented Jun 13, 2021

regehr commented Jun 13, 2021 • edited Loading

regehr commented Jun 13, 2021

regehr commented Jun 13, 2021 • edited Loading

regehr commented Jun 13, 2021

manasij7479 commented Jun 13, 2021

regehr commented Jun 14, 2021

regehr Jun 14, 2021

Choose a reason for hiding this comment

regehr commented Jun 14, 2021

regehr Jun 14, 2021

Choose a reason for hiding this comment

regehr Jun 14, 2021

Choose a reason for hiding this comment

regehr Jun 14, 2021

Choose a reason for hiding this comment

regehr commented Jun 14, 2021

regehr Jun 14, 2021

Choose a reason for hiding this comment

manasij7479 commented Jun 14, 2021

manasij7479 commented Jun 14, 2021

manasij7479 commented Jun 21, 2021

fvrmatteo commented Jun 21, 2021

regehr commented Jun 21, 2021

manasij7479 commented Sep 8, 2021

regehr commented Jun 13, 2021 •

edited

Loading

regehr commented Jun 13, 2021 •

edited

Loading