unknown reason of horn solver is Uninterpreted 'a2' in <null>

[QiongwenXu]

I am using z3 to do equivalence check. I try to use z3 horn solver to accelerate z3 solving time, and I met the following problem:

I would like to check whether two programs are the same or not. The logic of two programs is P1: a2 = a1 + 2, where a1 is the input, a2 is the output P2: b2 = b1 + 2, where b1 is the input, b2 is the output Type of a1, a2, b1, b2 is bit-vector 64. The formula is that forall (a1, b1), (a1 == b1) && (a2 == a1 + 2) && (b2 == b1 + 2) => (a2 == b2)

If I use a bv solver, the result is sat. However if I use a horn solver, the solve result is unknown, and the reason is

unknown
Uninterpreted 'a2' in <null>:
query!0(#1,#0) :- 
 (= a2 (bvadd (:var 1) #x0000000000000002)),
 (not (= a2 b2)),
 (= b2 (bvadd (:var 0) #x0000000000000002)),
 (= (:var 1) (:var 0)).

why these two solvers have different results? And why the reason of the horn solver is Uninterpreted 'a2' in <null>?

Here is the source code:

#include "z3++.h"
using namespace std;

int main() {
  z3::context ctx;
  z3::expr a1 = ctx.bv_const("a1", 64);
  z3::expr a2 = ctx.bv_const("a2", 64);
  z3::expr b1 = ctx.bv_const("b1", 64);
  z3::expr b2 = ctx.bv_const("b2", 64);

  z3::expr p1 = (a2 == a1 + 2);
  z3::expr p2 = (b2 == b1 + 2);
  z3::expr p_same_input = (a1 == b1);
  z3::expr p_post = (a2 == b2);
  z3::expr f = z3::implies(p_same_input && p1 && p2, p_post);

  z3::expr smt = z3::forall(a1, b1, f);
  z3::solver s(ctx, "HORN");  // set the solver as a horn solver
  s.add(smt);
  cout << s.check() << endl;
  cout << s.reason_unknown() << endl;
}

commit: 4643fdaa4e909d99e5888e4a6574d066c7516482

[NikolajBjorner]

It seems this query is formulated outside of the domain of Horn clauses. The Horn clause solver only accepts universally quantified implications (Horn clauses). These clauses cannot have free variables. The variables a2, b2 are free (they are existentially quantified). So the solver gives up.

There is also another question: do you want to check satisfiability of

exists a2 b2 . forall a1, b1 : same_input(a1, b1) & transform(a1,a2,b1,b2) => same_output(a2, b2)

or do you want to check validity, of say?

forall a2 b2 . forall a1, b1 : same_input(a1, b1) & transform(a1,a2,b1,b2) => same_output(a2, b2) 

To check validity of the latter, you should negate the formula and check for unsat of:

same_input(a1, b1) & transform(a1,a2,b1,b2) & not same_output(a2, b2) 

[QiongwenXu]

@NikolajBjorner Thanks for your reply. The target is that I would like to prove two programs have the same logic by proving that if two programs' inputs a1, b1 are the same, the two outputs a2, b2 should be the same. That is

forall a1, b1: same_input(a1, b1) && transform(a1, a2, b1, b2) => same output

The constrains on a2, b2 are in transform(a1, a2, b1, b2), which means that the values of a2, b2 depend on the inputs values and the transform formula.

I have tries two tests, still got error

  // a1, b1, a2, b2 are z3 bit-vector64 variables
  z3::expr p1 = (a2 == a1 + 2);
  z3::expr p2 = (b2 == b1 + 2);
  z3::expr p_same_input = (a1 == b1);
  z3::expr p_same_output = (a2 == b2);
  // if the result is sat, it is proved that two programs are equal.
  z3::expr smt = z3::forall(a1, b1, a2, b2, z3::implies(p_same_input && p1 && p2, p_same_output));
  z3::solver s(smt_c, "HORN");  // set the solver as a horn solver
  s.add(smt);
  cout << s.check() << endl;
  cout << s.reason_unknown() << endl;

result:
unknown
Rule contains infinite sorts in rule <null>:
query!0(#3,#2,#1,#0) :- 
 (= (:var 1) (bvadd (:var 3) #x0000000000000002)),
 (not (= (:var 1) (:var 0))),
 (= (:var 0) (bvadd (:var 2) #x0000000000000002)),
 (= (:var 3) (:var 2)).

  z3::expr p1 = (a2 == a1 + 2);
  z3::expr p2 = (b2 == b1 + 2);
  z3::expr p_same_input = (a1 == b1);
  z3::expr p_diff_output = (a2 != b2);
  // if the check result is sat, it means that the two programs are unequal.
  z3::expr smt = z3::exists(a1, a2, b1, b2, p_same_input && p1 && p2 && p_diff_output);
  z3::solver s(smt_c, "HORN");  // set the solver as a horn solver
  s.add(smt);
  cout << s.check() << endl;
  cout << s.reason_unknown() << endl;

result:
unknown
cannot process quantifier in rule <null>:
query!0() :- 
 (let ((a!1 (exists ((a1 (_ BitVec 64))
          (a2 (_ BitVec 64))
          (b1 (_ BitVec 64))
          (b2 (_ BitVec 64)))
       (and (= a1 b1)
         (= a2 (bvadd a1 #x0000000000000002))
         (= b2 (bvadd b1 #x0000000000000002))
         (distinct a2 b2)))))
 (not (= a!1 true))).

[NikolajBjorner]

I believe you don't want to use the Horn clause solver on this particular class of problems. The Horn solver is mainly suitable if you formulate problems over recursive or nested procedure calls. For your example, you have no nested procedure calls and you are just asking a query over bit-vectors.

The equivalence checking version with Horn clauses would be along the lines of encoding the Input/Output relation for two programs as Horn clauses. Then the query is then universally quantified. For your original example, you would create the formula forall(a1,a2,b1,b2, f), where f is z3::mk_implies(same_input & transform, same_output). As I say above, the Horn clause solver is really only useful, if writing the transform involves steps that can be summarized as procedures and these procedures can be formalized as uninterpreted predicates that are specified using Horn clauses.

[ngsrinivas]

Hi Nikolaj,

Thank you for your prompt reply! I'm replying on behalf of @QiongwenXu who is my student.

Setting some context to our question: we are using z3 to model programs in a domain-specific language (BPF) which includes memory access and library functions, but lacks loops. We are using the bitvector theory to formally model programs in first-order logic and are looking at ways to scale program equivalence checking in this language to the program sizes that we'd like our tool to handle.

We were wondering if the fast decision procedures available for Horn formulas (used in projects like network-optimized datalog, NSDI'15) might help us solve our formulas faster. We don't have procedures or nested calls in the language.

Do you see any reduction in solution time by using z3 Horn logic in our context? Or are we better off sticking to the bitvector logic?

Please let us know if you think there are better ways to go about optimizing for solver time. We would be happy to discuss more details of our specific FOL formula if you have questions.

Hope all is well, Srinivas

[NikolajBjorner]

At this point the questions seem around understanding the formalization domain. The use of exists/forall for an equivalence check seems to be contrary to the informally stated intent so part of the communication is around formalization intent. Best to settle on the intent for formalization and then the backend.

NoD is highly specialized to packet filter rules and specified in static router and static firewall configurations. You can select it by specifying the backend engine for the HORN clause solver. It will not be selected unless you use an option to use it. The default HORN backend solver is SPACER, which is more generally applicable. I don't think it is going to be adequate if you start performing bit-vector arithmetic. So a packet filter that may be performing a set of bit-vector arithmetic operations would be outside the scope of what NoD was designed for.

For a straight-line program you can sometimes expand and apply a one-shot solver. This will typically be more efficient. The SPACER HORN clause solver does allow some modularity during the solving process. In a nutshell it infers an interface specification of modules. Whether it has the right tools for inferring the adequate specification depends on whether the domain it is applied to is well handled. Bit-vector domains are not too well handled from the Horn clause solver, but it remains a steady target of interest. So as there are samples it can inspire progress on the modular benefits that comes with the Horn clause solver. (under the hood, the SPACER Horn clause solver applies an IC3 style algorithm that infers k-step inductive invariants obtained by unfolding the Horn clauses up to k steps. If it realizes that the k-step property holds also for k+1, k+2, .., infinity, it has obtained an inductive invariant. If the conjunctive of all learned inductive invariants imply the negation of the assertion in the head of the Horn clause(s), then it terminates).

Based on the sample, I would say try basic satisfiability checks. There are some papers on EBPF with Sagiv, Naradytska and Gurfinkel and others. They could be suggesting some encoding techniques. The solver design space is generally between the pre-unfolded constraints and some attempt to modularize them.

[ngsrinivas]

Hi Nikolaj, thank you for your timely and insightful response!

Your message gave me a chance to look up the underlying set of techniques in NoD, the IC3 algorithm, as well as the problems that SPACER and the Z3 horn solver might be suitable for. (I'm not trained as a formal methods person.) Your thoughts on this were really helpful, thanks.

Building on your suggestion to clarify our main method of formalization: what we're doing now is what I think you're referring to as a "one-shot solver." Assume we are given a straight line program (branches are present but no loops/induction). We formalize the input-output behavior of the program in first-order logic (bitvector domain) instruction-by-instruction using the semantics of the BPF instruction set. The language provides what are known as "helper functions," which can be thought of as library/procedure calls. Currently, we are modeling the input-output relationships of those functions explicitly in first-order logic and conjoin these encodings with the above. The BPF language also supports memory access (load/store instructions). Some part of memory (e.g., BPF maps) can be persistent across program invocations, and these, along with the program's input register and return value register, constitute the inputs/outputs for the entire program.

Given two programs, we use their input/output behavioral encoding to check equivalence between the two programs. We're attempting to hit equivalence check times of < 1 second for programs with a few hundred instructions. (Our attempt at using Horn clauses and the Horn solver was motivated by these efficiency concerns.)

Do you think such equivalence check times are at all feasible? I'm sure I can provide more context to the question, so please let me know your thoughts on what I can clarify. Thanks again for your kind help!

[NikolajBjorner]

z3 has been used for various forms of equivalence checking. The pex4fun web-site used the symbolic execution engine to check equivalence between programs. The idea was to give users a puzzle with just an empty function call to start with. Then the user fills in some possible code. The user's program is run together with the secret program on the same input and the output is checked for equality. If there is some input combination that produces different outputs it is listed as a counter-example. The user then corrects the program to ensure it doesn't hit the counter example and hopefully is fully correct. Pex's technology is based on path exploration. The cost of checking increases as different branches are explored so these path queries are typically much cheaper than unfolding branches into a formula. This is the typical place where practically all related tools (KLEE, CBMC, SAGE, etc) make performance tradeoffs.

There are some more recent developments of checking hyper-properties with Horn clauses (related to information flow). Delving into this area is possibly outside of your scope, so I would say you should consider first evaluating an unfolding based approach and possibly have to control path exploration outside of z3. A nice thing with Horn clauses is of course that it manages path exploration so you can of course revisit whether this avenue at some point.

[ngsrinivas]

Thank you, Nikolaj, for those very helpful suggestions!

Our current formula is a conjunction of clauses which resemble the form branch_condition => encoding_of_statement_body This formula encompasses all branch/path conditions with symbolic values (akin to a bounded model checking approach).

The idea of doing more "concrete" per-path solver queries by managing the path explosion outside z3 is quite interesting. We will explore this. We're learning more about "symbolic profiling" and containing the explosive growth in formula sizes through recent work by Emina Torlak's research group (James Bornholt et al).

Could you pls provide a pointer to work on using Horn clauses to check hyperproperties? Seems very interesting.

Btw, I was unable to reach a web demo page starting from https://www.microsoft.com/en-us/research/project/pex4fun/ but I may be missing something.

We are very grateful for all the helpful pointers!