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.

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

Invalid model generated without warning #740

Closed
delcypher opened this issue Sep 16, 2016 · 15 comments

Comments

@delcypher
Copy link
Contributor

commented Sep 16, 2016

I've been trying to track down an issue I've been getting where Z3 seems to be generating invalid models. I became suspicious when my tool tried to use Z3 generated models in the tool's expression language and finding that they didn't seem to satisfy the constraints I had passed to Z3.

I'm currently using Z3 via its C API.

I thought doing Z3_global_param_set("model_validate", "true") would detect problems like this but no warnings or errors seem to fire. Seeing as I was very suspicious of this I decided to implement manual checking of a Z3_model in my tool (see https://github.com/delcypher/klee/blob/z3_debugging/lib/Solver/Z3Solver.cpp#L347 ).

Basically I iterate over the assertions in the solver and try evaluating the expressions using the model. Each assertion should evaluate to Z3_L_TRUE. However when running my tool I've come across a scenario where one of the assertions in the model evaluates to false in the provided model.

When this occurs I have my tool dump the query and the model and this is what it shows.

Validating model failed:
The expression:
Z3ASTHandle:
(let ((a!1 (concat (select f_0x607000022ae0 #x00000003)
                   (concat (select f_0x607000022ae0 #x00000002)
                           (concat (select f_0x607000022ae0 #x00000001)
                                   (select f_0x607000022ae0 #x00000000))))))
(let ((a!2 (bvsle #x00000005
                  (to_ieee_bv (fp.add roundNearestTiesToEven
                                      ((_ to_fp 8 24) a!1)
                                      (fp #b0 #x7f #b00000000000000000000000))))))
  (not (bvsle (ite a!2 #x00000000 #x00000001) #x00000000))))
evaluated to 
Z3ASTHandle:
false
But should be true
Solver state:
(declare-fun f_0x607000022ae0 () (Array (_ BitVec 32) (_ BitVec 8)))
(assert (let ((a!1 (concat (select f_0x607000022ae0 #x00000003)
                   (concat (select f_0x607000022ae0 #x00000002)
                           (concat (select f_0x607000022ae0 #x00000001)
                                   (select f_0x607000022ae0 #x00000000))))))
(let ((a!2 (bvsle #x00000005
                  (to_ieee_bv (fp.add roundNearestTiesToEven
                                      ((_ to_fp 8 24) a!1)
                                      (fp #b0 #x7f #b00000000000000000000000))))))
  (not (bvsle (ite a!2 #x00000000 #x00000001) #x00000000)))))

Model:
(define-fun f_0x607000022ae0 () (Array (_ BitVec 32) (_ BitVec 8))
  (_ as-array k!52))
(define-fun k!52 ((x!0 (_ BitVec 32))) (_ BitVec 8)
  (ite (= x!0 #x00000002) #x88
  (ite (= x!0 #x00000000) #x10
  (ite (= x!0 #x00000003) #x7f
  (ite (= x!0 #x00000001) #x80
    #x88)))))

I'm running a slightly old build of Z3 (so I can use ASan) but I'm going to try with a newer build.

Any suggestions on what I can do to help you debug this?

@wintersteiger

This comment has been minimized.

Copy link
Member

commented Sep 16, 2016

This is quite possibly a real bug. Model validation doesn't work for arrays yet (those as-array functions are a bit tricky; see https://github.com/Z3Prover/z3/blob/master/src/cmd_context/cmd_context.cpp#L1672).

I've added the array declaration to get a test case:

(set-option :model_validate true)

(declare-fun f_0x607000022ae0 () (Array (_ BitVec 32) (_ BitVec 8)))

(assert (let ((a!1 (concat (select f_0x607000022ae0 #x00000003)
                       (concat (select f_0x607000022ae0 #x00000002)
                           (concat (select f_0x607000022ae0 #x00000001)
                               (select f_0x607000022ae0 #x00000000))))))
            (let ((a!2 (bvsle #x00000005
                           (to_ieee_bv (fp.add roundNearestTiesToEven
                                           ((_ to_fp 8 24) a!1)
                                           (fp #b0 #x7f #b00000000000000000000000))))))
                (not (bvsle (ite a!2 #x00000000 #x00000001) #x00000000))))
)

(check-sat)
(get-model)

However, I get a different model. Could you perhaps create an API interaction log, so I can replay exactly what you get (Via Z3_open_log(...))?

Just a note: this part of the problem: (bvsle #x00000005 (to_ieee_bv ...)) looks rather suspicious to me; it checks whether some floating-point number is within the first 5 denormal numbers. Was that the intention?

@delcypher

This comment has been minimized.

Copy link
Contributor Author

commented Sep 16, 2016

I've recorded an interaction log ( z3.log.zip ). I'm not sure how much this will help because no crash in Z3 is triggered. This is using a recent (5290cd1) release build of Z3.

The interaction ends when my tool determines that the model returned by Z3 is not correct and the tool dumps this.

Validating model failed:
The expression:
Z3ASTHandle:
(let ((a!1 (concat (select f_0x27f12a0 #x00000003)
                   (concat (select f_0x27f12a0 #x00000002)
                           (concat (select f_0x27f12a0 #x00000001)
                                   (select f_0x27f12a0 #x00000000))))))
(let ((a!2 (bvsle (to_ieee_bv (fp.add roundNearestTiesToEven
                                      ((_ to_fp 8 24) a!1)
                                      (fp #b0 #x7f #b00000000000000000000000)))
                  #x00000005)))
  (not (bvsle (ite a!2 #x00000001 #x00000000) #x00000000))))
evaluated to 
Z3ASTHandle:
false
But should be true
Solver state:
(declare-fun f_0x27f12a0 () (Array (_ BitVec 32) (_ BitVec 8)))
(assert (let ((a!1 (concat (select f_0x27f12a0 #x00000003)
                   (concat (select f_0x27f12a0 #x00000002)
                           (concat (select f_0x27f12a0 #x00000001)
                                   (select f_0x27f12a0 #x00000000))))))
(let ((a!2 (bvsle (to_ieee_bv (fp.add roundNearestTiesToEven
                                      ((_ to_fp 8 24) a!1)
                                      (fp #b0 #x7f #b00000000000000000000000)))
                  #x00000005)))
  (not (bvsle (ite a!2 #x00000001 #x00000000) #x00000000)))))

Model:
(define-fun f_0x27f12a0 () (Array (_ BitVec 32) (_ BitVec 8))
  (_ as-array k!46))
(define-fun k!46 ((x!0 (_ BitVec 32))) (_ BitVec 8)
  (ite (= x!0 #x00000002) #x80
  (ite (= x!0 #x00000000) #x40
  (ite (= x!0 #x00000003) #x7f
  (ite (= x!0 #x00000001) #x00
    #x80)))))

z3.log.zip

@delcypher

This comment has been minimized.

Copy link
Contributor Author

commented Sep 16, 2016

@wintersteiger

Just a note: this part of the problem: (bvsle #x00000005 (to_ieee_bv ...)) looks rather suspicious to me; it checks whether some floating-point number is within the first 5 denormal numbers. Was that the intention?

I believe the expression I'm passing to Z3 is correct but the intention is different to what you guessed. This constraint comes from a C program that basically does this:

int main() {
  float f; // Unknown value

  f = f + 1;

  int x = 0;
  memcpy(&x, &f, sizeof(float));

  if ( x < 5 ) {
     abort(); // Is this reachable?
  }
}

Use of to_ieee_bv comes in because the program copies the bit representation of a floating point number into a integer using memcpy and then does a computation on it. This is not a representative real world C program but it is meant to stress test my tool by doing weird things with floating point numbers.

Side note: The C program is actually more complicated than this and tests many different integer operations applied to bits that come from a symbolic floating point number so in the log you will probably see many calls to the solver before an invalid model was generated.

@wintersteiger

This comment has been minimized.

Copy link
Member

commented Sep 16, 2016

I see, thanks for the context! This is indeed a "weird thing", that's why it looked strange to me. We should definitely get a correct model for this though.

@delcypher

This comment has been minimized.

Copy link
Contributor Author

commented Sep 22, 2016

@wintersteiger Was the log useful to you? Did it help in tracking down a bug?

@delcypher

This comment has been minimized.

Copy link
Contributor Author

commented Oct 10, 2016

@wintersteiger (@afd @ccadar). I've been thinking about this problem some more and I think the problem may be related to the use of the to_ieee_bv function and NaNs.

I've made some changes to my tool so for this particular query the arrays are removed however I'm still seeing the problem.

Anyway here are three example failures I've seen where my code tries to check the model returned by Z3 and evaluation fails. I have a few observations that might be helpful.

First example

Validating model failed:
The expression:
Z3ASTHandle:
(let ((a!1 (bvsle (to_ieee_bv (fp.add roundNearestTiesToEven
                                      ((_ to_fp 8 24) f_ackermann_0)
                                      (fp #b0 #x7f #b00000000000000000000000)))
                  #x00000005)))
  (bvsle (ite a!1 #x00000000 #x00000001) #x00000000))
evaluated to
Z3ASTHandle:
false
But should be true
Solver state:
(declare-fun f_ackermann_0 () (_ BitVec 32))
(assert (let ((a!1 (bvsle (to_ieee_bv (fp.add roundNearestTiesToEven
                                      ((_ to_fp 8 24) f_ackermann_0)
                                      (fp #b0 #x7f #b00000000000000000000000)))
                  #x00000005)))
  (bvsle (ite a!1 #x00000000 #x00000001) #x00000000)))

Model:
(define-fun f_ackermann_0 () (_ BitVec 32)
  #xff800080)

It turns out 0xff800080 is one of many possible representations for NaN. Creating a new query from this and giving this to the Z3 executable gives unsat (as it should).

(define-fun f_ackermann_0 () (_ BitVec 32) #xff800080)
(assert (let ((a!1 (bvsle (to_ieee_bv (fp.add roundNearestTiesToEven
                                      ((_ to_fp 8 24) f_ackermann_0)
                                      (fp #b0 #x7f #b00000000000000000000000)))
                  #x00000005)))
  (bvsle (ite a!1 #x00000000 #x00000001) #x00000000)))
(check-sat)

Side note, if I ask Z3 for the value to the (to_ieee_bv ...) in the above query it gives 0x7f800001
which is a different bit representation for NaN than 0xff800080.

Second example

Validating model failed:
The expression:
Z3ASTHandle:
(let ((a!1 (bvsle #x00000005
                  (to_ieee_bv (fp.add roundNearestTiesToEven
                                      ((_ to_fp 8 24) f_ackermann_0)
                                      (fp #b0 #x7f #b00000000000000000000000))))))
  (bvsle (ite a!1 #x00000001 #x00000000) #x00000000))
evaluated to
Z3ASTHandle:
false
But should be true
Solver state:
(declare-fun f_ackermann_0 () (_ BitVec 32))
(assert (let ((a!1 (bvsle #x00000005
                  (to_ieee_bv (fp.add roundNearestTiesToEven
                                      ((_ to_fp 8 24) f_ackermann_0)
                                      (fp #b0 #x7f #b00000000000000000000000))))))
  (bvsle (ite a!1 #x00000001 #x00000000) #x00000000)))

Model:
(define-fun f_ackermann_0 () (_ BitVec 32)
  #x7f810000)

Again 0x7f81000 is another representation for NaN. Feeding this into the Z3 executable gives unsat.

(define-fun f_ackermann_0 () (_ BitVec 32) #x7f810000)
(assert (let ((a!1 (bvsle #x00000005
                  (to_ieee_bv (fp.add roundNearestTiesToEven
                                      ((_ to_fp 8 24) f_ackermann_0)
                                      (fp #b0 #x7f #b00000000000000000000000))))))
  (bvsle (ite a!1 #x00000001 #x00000000) #x00000000)))
(check-sat)                

Third example

validating model failed:
The expression:
Z3ASTHandle:
(let ((a!1 (bvmul #x00000003
                  (to_ieee_bv (fp.add roundNearestTiesToEven
                                      ((_ to_fp 8 24) f_ackermann_1)
                                      (fp #b0 #x7f #b00000000000000000000000))))))
  (bvsle a!1 #x00000000))
evaluated to
Z3ASTHandle:
false
But should be true
Solver state:
(declare-fun action_ackermann_0 () (_ BitVec 32))
(declare-fun f_ackermann_1 () (_ BitVec 32))
(assert (= #x00000003 action_ackermann_0))
(assert (let ((a!1 (bvmul #x00000003
                  (to_ieee_bv (fp.add roundNearestTiesToEven
                                      ((_ to_fp 8 24) f_ackermann_1)
                                      (fp #b0 #x7f #b00000000000000000000000))))))
  (bvsle a!1 #x00000000)))

Model:
(define-fun f_ackermann_1 () (_ BitVec 32)
  #xff800080)
(define-fun action_ackermann_0 () (_ BitVec 32)
  #x00000003)

Again 0xff800080 is yet another representation for NaN. Again giving the solver state and model to the Z3 executable gives unsat

(define-fun f_ackermann_1 () (_ BitVec 32)
  #xff800080)
(define-fun action_ackermann_0 () (_ BitVec 32)
  #x00000003)
(assert (= #x00000003 action_ackermann_0))
(assert (let ((a!1 (bvmul #x00000003
                  (to_ieee_bv (fp.add roundNearestTiesToEven
                                      ((_ to_fp 8 24) f_ackermann_1)
                                      (fp #b0 #x7f #b00000000000000000000000))))))
  (bvsle a!1 #x00000000)))
(check-sat)

Thoughts

So what I seem to be observing is that all the invalid models I'm getting involve the use of to_ieee_bv and the invalid model containing bit patterns that represent NaN.

It also seems that giving the solver state reported (without the invalid model) to the Z3 executable gives different models that are correct. Why would Z3 give different models in this case? Does Z3 store any state between solver calls (e.g. the state of random number generators)?

@wintersteiger

This comment has been minimized.

Copy link
Member

commented Oct 10, 2016

Yes, the problem is definitely in the vicinity of (to_ieee_bv NaN), which is partially unspecified. That part is OK, but for some reason the interpretation of to_ieee_bv_unspecified is not added to the model and I haven't figured out why yet. Obviously, we'll need that to check whether models are correct.

If you don't need those unspecified semantics (at least for now), you can disable them by setting rewriter.hi_fp_unspecified to true. This enables the "hardware interpretation", in which (to_ieee_bv NaN) is always #x7f000001 (and similar for other FP sizes), and that should behave more predictable.

The "solver state" in this example is only the list of assertions held by a solver object. It's not the same as "everything the solver knows or remembers", so yes, we can not assume that both of us would get the same models, especially when we are running different versions/commits of Z3 on different platforms, and possibly incremental vs non-incremental solver usage (e.g. I'm running non-incremental SMT2 files here).

@delcypher

This comment has been minimized.

Copy link
Contributor Author

commented Oct 10, 2016

Thanks, I had forgotten about rewriter.hi_fp_unspecified. How do I actually set that option from the C API?

I tried basically doing this

::Z3_config cfg = Z3_mk_config();$
::Z3_context ctx = Z3_mk_context_rc(cfg);$
::Z3_del_config(cfg);
::Z3_params solverParameters = Z3_mk_params(ctx);
Z3_params_inc_ref(ctx, solverParameters);
::Z3_symbol hardwareIEEE754InterpStrSymbol = Z3_mk_string_symbol(ctx, "rewriter.hi_fp_unspecified");
Z3_params_set_bool(ctx, solverParameters, hardwareIEEE754InterpStrSymbol, true);
Z3_solver theSolver = Z3_mk_simple_solver(ctx);
Z3_solver_inc_ref(ctx, theSolver);
Z3_solver_set_params(ctx, theSolver, solverParameters);

but this fails with Z3's error handler firing

Incorrect use of Z3. [12] unknown parameter 'rewriter.hi_fp_unspecified'
Legal parameters are:
  arith.branch_cut_ratio (unsigned int) (default: 2)
  arith.dump_lemmas (bool) (default: false)
  arith.euclidean_solver (bool) (default: false)
  arith.greatest_error_pivot (bool) (default: false)
  arith.ignore_int (bool) (default: false)
  arith.int_eq_branch (bool) (default: false)
  arith.nl (bool) (default: true)
  arith.nl.branching (bool) (default: true)
  arith.nl.gb (bool) (default: true)
  arith.nl.rounds (unsigned int) (default: 1024)
  arith.propagate_eqs (bool) (default: true)
  arith.propagation_mode (unsigned int) (default: 2)
  arith.random_initial_value (bool) (default: false)
  arith.solver (unsigned int) (default: 2)
  array.extensional (bool) (default: true)
  array.weak (bool) (default: false)
  auto_config (bool) (default: true)
  bv.enable_int2bv (bool) (default: true)
  bv.reflect (bool) (default: true)
  case_split (unsigned int) (default: 1)
  core.minimize (bool) (default: false)
  core.validate (bool) (default: false)
  dack (unsigned int) (default: 1)
  dack.eq (bool) (default: false)
  dack.factor (double) (default: 0.1)
  dack.gc (unsigned int) (default: 2000)
  dack.gc_inv_decay (double) (default: 0.8)
  dack.threshold (unsigned int) (default: 10)
  delay_units (bool) (default: false)
  delay_units_threshold (unsigned int) (default: 32)
  ematching (bool) (default: true)
  logic (symbol) (default: )
  macro_finder (bool) (default: false)
  max_conflicts (unsigned int) (default: 4294967295)
  mbqi (bool) (default: true)
  mbqi.force_template (unsigned int) (default: 10)
  mbqi.id (string) (default: )
  mbqi.max_cexs (unsigned int) (default: 1)
  mbqi.max_cexs_incr (unsigned int) (default: 0)
  mbqi.max_iterations (unsigned int) (default: 1000)
  mbqi.trace (bool) (default: false)
  model (bool) (default: true)
  pb.conflict_frequency (unsigned int) (default: 1000)
  pb.enable_compilation (bool) (default: true)
  pb.enable_simplex (bool) (default: false)
  pb.learn_complements (bool) (default: true)
  phase_selection (unsigned int) (default: 3)
  proof (bool) (default: false)
  pull_nested_quantifiers (bool) (default: false)
  qi.cost (string) (default: (+ weight generation))
  qi.eager_threshold (double) (default: 10.0)
  qi.lazy_threshold (double) (default: 20.0)
  qi.max_instances (unsigned int) (default: 4294967295)
  qi.max_multi_patterns (unsigned int) (default: 0)
  qi.profile (bool) (default: false)
  qi.profile_freq (unsigned int) (default: 4294967295)
  random_seed (unsigned int) (default: 0)
  refine_inj_axioms (bool) (default: true)
  relevancy (unsigned int) (default: 2)
  restart_factor (double) (default: 1.1)
  restart_strategy (unsigned int) (default: 1)
  rlimit (unsigned int) (default: 0)
  timeout (unsigned int) (default: 4294967295)
  unsat_core (bool) (default: false)

Do I need to make a custom tactic or something and set the parameter on that?

@delcypher

This comment has been minimized.

Copy link
Contributor Author

commented Oct 10, 2016

Okay. So for anyone reading this needs to be set as a global parameter which can be done like so from the C API.

Z3_global_param_set("rewriter.hi_fp_unspecified", "true");

For at least the example I'm working with this seems to have fixed invalid models being generated by Z3.

@wintersteiger

This comment has been minimized.

Copy link
Member

commented Oct 15, 2016

This is hopefully fixed now. All the various unspecified values behave as intended on our regression tests.

Strange that the rewriter options are missing in the solver. That may depend on which solver exactly is constructued, as not all of them support/use the same settings.

@delcypher

This comment has been minimized.

Copy link
Contributor Author

commented Oct 15, 2016

@wintersteiger Thanks for trying to fix the problem. I'll test the changes over the next few days and will report back.

@wintersteiger

This comment has been minimized.

Copy link
Member

commented Oct 16, 2016

@delcypher Don't worry just yet. Looks like I messed up the reference counts somewhere, so there are non-deterministic assertion violations currently.

@wintersteiger wintersteiger reopened this Oct 16, 2016

wintersteiger added a commit that referenced this issue Oct 17, 2016
wintersteiger added a commit to wintersteiger/z3 that referenced this issue Oct 18, 2016
@wintersteiger

This comment has been minimized.

Copy link
Member

commented Oct 19, 2016

Those other issues have now been resolved and everything should work as expected. @delcypher: would be fantastic if you could run some of your own tests to see whether all of this aligns now.

@delcypher

This comment has been minimized.

Copy link
Contributor Author

commented Oct 20, 2016

@wintersteiger Testing now. I will report back once I've done a few runs. I'll also try an ASan debug build too.

@delcypher

This comment has been minimized.

Copy link
Contributor Author

commented Oct 21, 2016

@wintersteiger Okay I tried running the test I was having problems and I'm not getting errors due to Z3's generated model being invalid. I also did an ASan build and didn't find any problems.

A problem I am hitting though is a disagreement between KLEE's expression language and Z3's when using the model generated by Z3. This is an issue I had before and which I'm currently investigating. We use LLVM's APFloat class for evaluating concrete expressions and it looks like when the bits from Z3's model represent a NaN the behaviour differs. This is really a separate issue though so I'll close this one.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
2 participants
You can’t perform that action at this time.