Unused C struct fields causing saw to enter possible infinite loop

[weaversa]

Here is another example that I think exercises the same underlying issue. The first proof goes through in about 1 second. But, simply adding an extra field to the struct causes the proof to fall into an abyss.

Another oddity is this --- changing the prover for the second proof from abc to z3 still exhibits the slow down, but if I change the solver to offline_smtlib2, z3 can solve the resulting smt2 files in less than a second.

#include <stdint.h>

typedef struct example_struct_t {
  uint32_t a[4];
} example_struct_t;

typedef struct example_struct_2_t {
  uint32_t a[4];
  uint32_t b[4];
} example_struct_2_t;

uint32_t mult(uint32_t data[], example_struct_t *s, uint32_t i) {
  return data[i] * s->a[i];
}

uint32_t mult2(uint32_t data[], example_struct_2_t *s, uint32_t i) {
  return data[i] * s->a[i];
}

let alloc_init var_type v = do {
  p <- crucible_alloc var_type;
  crucible_points_to p v;
  return p;
};

let ptr_to_fresh n var_type = do {
  x <- crucible_fresh_var n var_type;
  p <- alloc_init var_type (crucible_term x);
  return (x, p);
};

let {{

  type State = [4][32]
  type example_struct_t = { a : [4][32] }
  type example_struct_2_t = { a: [4][32], b : [4][32] }

  mult : State -> example_struct_t -> [32] -> [32]
  mult data s i = data@i * s.a@i

  mult2 : State -> example_struct_2_t -> [32] -> [32]
  mult2 data s i = data@i * s.a@i

}};


let mult_spec = do {
  (data, data_p) <- ptr_to_fresh "data" (llvm_array 4 (llvm_int 32));

  (a, a_p) <- ptr_to_fresh "a" (llvm_array 4 (llvm_int 32));
  i <- crucible_fresh_var "i" (llvm_int 32);

  crucible_precond {{ (i >= 0) /\ (i <= 3) }};

  let s = crucible_struct [crucible_term a];
  s_p <- alloc_init (llvm_struct "struct.example_struct_t") s;

  crucible_execute_func [data_p, s_p, crucible_term i];

  crucible_return (crucible_term {{ mult data {a=a} i }});
};

let mult2_spec = do {
  (data, data_p) <- ptr_to_fresh "data" (llvm_array 4 (llvm_int 32));

  (a, a_p) <- ptr_to_fresh "a" (llvm_array 4 (llvm_int 32));
  (b, b_p) <- ptr_to_fresh "b" (llvm_array 4 (llvm_int 32));
  i <- crucible_fresh_var "i" (llvm_int 32);

  crucible_precond {{ (i >= 0) /\ (i <= 3) }};

  let s = crucible_struct [crucible_term a, crucible_term b];
  s_p <- alloc_init (llvm_struct "struct.example_struct_2_t") s;

  crucible_execute_func [data_p, s_p, crucible_term i];

  crucible_return (crucible_term {{ mult2 data {a=a, b=b} i }});
};

mult_bc <- llvm_load_module "mult.bc";

mult_ov <- crucible_llvm_verify mult_bc "mult" [] false mult_spec abc;

mult2_ov <- crucible_llvm_verify mult_bc "mult2" [] false mult2_spec abc;

$ make
clang -emit-llvm -c mult.c -o mult.bc
saw mult.saw
[15:53:57.297] Loading file "test/mult.saw"
[15:53:57.335] Verifying mult ...
[15:53:57.347] Simulating mult ...
[15:53:57.348] Checking proof obligations mult ...
[15:53:58.433] Proof succeeded! mult
[15:53:58.454] Verifying mult2 ...
[15:53:58.474] Simulating mult2 ...
[15:53:58.476] Checking proof obligations mult2 ...

Originally posted by @weaversa in #517 (comment)

[weaversa]

Since I don't really know what is going on, the title may be misleading.

[brianhuffman]

The proof of mult2 seems to hang not just with abc, but also with other provers, e.g. w4, z3, or yices. With these backends it seems that the CPU time is spent running the external solver.

One interesting data point: If you switch all the datatypes in the C source from uint32_t to uint8_t (and change the Cryptol spec to match) then all the proofs finish quickly. The only real difference I can think of is that with uint32_t, the address calculations involve multiplication by 4.

[weaversa]

@brianhuffman when changing the backend for mult2 to offline_smtlib2, z3 can solve the resulting smt2 files via the command line in less than a second. So, I don't think this is a solver performance issue.

[brianhuffman]

I suspected that maybe offline_smtlib2 was actually generating different input that what the other prover backends (e.g. z3, yices) do when they are talking directly to a solver. So I swapped out the yices-smt2 binary in my path for a script that tees the output to a file, while piping it on to the real yices-smt2 binary.

The smt output is different. The offline_smtlib2 command produces this:

; Automatically created by SBV on 2019-11-08 16:17:04.258124 PST
(set-option :smtlib2_compliant true)
(set-option :diagnostic-output-channel "stdout")
(set-option :produce-models true)
(set-logic BV)
; --- uninterpreted sorts ---
; --- tuples ---
; --- sums ---
; --- literal constants ---
(define-fun s89 () (_ BitVec 1) #b0)
(define-fun s26 () (_ BitVec 2) #b00)
(define-fun s13 () (_ BitVec 32) #x00000003)
(define-fun s17 () (_ BitVec 32) #x00000000)
(define-fun s15 () (_ BitVec 64) #x0000000000000010)
(define-fun s16 () (_ BitVec 64) #x0000000000000004)
(define-fun s35 () (_ BitVec 64) #x0000000000000000)
(define-fun s41 () (_ BitVec 64) #x0000000000000008)
(define-fun s45 () (_ BitVec 64) #x000000000000000c)
(define-fun s50 () (_ BitVec 64) #x0000000000000020)
(define-fun s63 () (_ BitVec 64) #x0000000000000014)
(define-fun s67 () (_ BitVec 64) #x0000000000000018)
(define-fun s71 () (_ BitVec 64) #x000000000000001c)
; --- skolem constants ---
; --- constant tables ---
; --- skolemized tables ---
; --- arrays ---
; --- uninterpreted constants ---
; --- user given axioms ---
; --- formula ---
(assert (forall ((s0 (_ BitVec 32))
                 (s1 (_ BitVec 32))
                 (s2 (_ BitVec 32))
                 (s3 (_ BitVec 32))
                 (s4 (_ BitVec 32))
                 (s5 (_ BitVec 32))
                 (s6 (_ BitVec 32))
                 (s7 (_ BitVec 32))
                 (s8 (_ BitVec 32))
                 (s9 (_ BitVec 32))
                 (s10 (_ BitVec 32))
                 (s11 (_ BitVec 32))
                 (s12 (_ BitVec 32)))
            (let ((s14 (bvult s13 s12)))
            (let ((s18 (concat s17 s12)))
            (let ((s19 (bvmul s16 s18)))
            (let ((s20 (bvult s15 s19)))
[...200 lines omitted...]
            (let ((s221 (or s76 s220)))
            (let ((s222 (or s14 s221)))
            (not s222))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(check-sat)

while the actual input to the yices-smt2 binary was like this:

(set-option :print-success true)
(set-option :produce-models true)
(set-logic QF_BV)
(define-fun s89 () (_ BitVec 1) #b0)
(define-fun s26 () (_ BitVec 2) #b00)
(define-fun s13 () (_ BitVec 32) #x00000003)
(define-fun s17 () (_ BitVec 32) #x00000000)
(define-fun s15 () (_ BitVec 64) #x0000000000000010)
(define-fun s16 () (_ BitVec 64) #x0000000000000004)
(define-fun s35 () (_ BitVec 64) #x0000000000000000)
(define-fun s41 () (_ BitVec 64) #x0000000000000008)
(define-fun s45 () (_ BitVec 64) #x000000000000000c)
(define-fun s50 () (_ BitVec 64) #x0000000000000020)
(define-fun s63 () (_ BitVec 64) #x0000000000000014)
(define-fun s67 () (_ BitVec 64) #x0000000000000018)
(define-fun s71 () (_ BitVec 64) #x000000000000001c)
(declare-fun s0 () (_ BitVec 32)) ; tracks user variable "x0"
(declare-fun s1 () (_ BitVec 32)) ; tracks user variable "x1"
(declare-fun s2 () (_ BitVec 32)) ; tracks user variable "x2"
(declare-fun s3 () (_ BitVec 32)) ; tracks user variable "x3"
(declare-fun s4 () (_ BitVec 32)) ; tracks user variable "x4"
(declare-fun s5 () (_ BitVec 32)) ; tracks user variable "x5"
(declare-fun s6 () (_ BitVec 32)) ; tracks user variable "x6"
(declare-fun s7 () (_ BitVec 32)) ; tracks user variable "x7"
(declare-fun s8 () (_ BitVec 32)) ; tracks user variable "x8"
(declare-fun s9 () (_ BitVec 32)) ; tracks user variable "x9"
(declare-fun s10 () (_ BitVec 32)) ; tracks user variable "x10"
(declare-fun s11 () (_ BitVec 32)) ; tracks user variable "x11"
(declare-fun s12 () (_ BitVec 32)) ; tracks user variable "x12"
(define-fun s14 () Bool (bvult s13 s12))
(define-fun s18 () (_ BitVec 64) (concat s17 s12))
(define-fun s19 () (_ BitVec 64) (bvmul s16 s18))
(define-fun s20 () Bool (bvult s15 s19))
[...200 lines omitted...]
(define-fun s221 () Bool (or s76 s220))
(define-fun s222 () Bool (or s14 s221))
(define-fun s223 () Bool (not s222))
(assert s223)
(check-sat)

I checked and all the same variable names s0-s223 are used, and the right-hand sides are the same in both, except the offline_smtlib2 version uses a single assert with a forall, while the direct-to-solver version uses separate declare-fun and define-fun commands.

z3 handles the offline_smtlib2 version with no trouble, but on the other version it seems to hang with 100% cpu usage (as does yices-smt2). I don't know why.

[brianhuffman]

As far as the weirdness related to offline_smtlib2, this is apparently due to #613. z3 has an easy time with the offline_smtlib2-generated files because they contain a much-too-weak version of the proof goal (universal quantifiers are switched to existentials).