Re: [Valgrind-developers] V-Bit Verification

[Lok K. Y. <lo...@sy...>]

Unforunately, we cannot automatically generate a set of cases. On the other hand, we don't think that it is necessary. I think it might be best to use an example to illustrate how we can do the verification:

1. Convert the rule to SMT2. Here is some representative SMT code/declarations for the expensive add rule.
  
(bvor 
  (bvor qaa qbb)
  (bvxor
    (bvadd a_min b_min)
    (bvadd a_max b_max)
  )
)

The original code from mc_translate.c is:

      // result = (qaa | qbb) | ((a_min + b_min) ^ (a_max + b_max))
      return
      assignNew('V', mce,ty,
         binop( opOR,
                assignNew('V', mce,ty, binop(opOR, qaa, qbb)),
                assignNew('V', mce,ty, 
                   binop( opXOR, 
                          assignNew('V', mce,ty, binop(opADD, a_min, b_min)),
                          assignNew('V', mce,ty, binop(opADD, a_max, b_max))
                   )
                )
         )
      );

I think the similarities should be evident. e.g., bvadd = opADD, bvor = opOR and etc.

2. Once the rule has been modeled, we use an SMT solver to verify that the rule is correct, i.e. defined means defined - no false negatives. 

3. If the rule is not valid, then the SMT solver will provide a counter example, which can be considered as one single test case. For example, if I excluded the first part (qaa | qbb) from the rule above, we get the counter example below. Presuming that the counter example is correct (that is our verification model is correct) then we only have one single test case for this single rule. This test case might not apply to other rules at all. 

aa = 0x81780200
qaa = 0xcdff1f83
bb = 0x008c0000
qbb = 0x31ec6105


Lok
________________________________________
From: Julian Seward [js...@ac...]
Sent: Thursday, August 02, 2012 5:02 AM
To: val...@li...
Cc: Lok Kwong Yan
Subject: Re: [Valgrind-developers] V-Bit Verification

> improved and and the add rules are sound. We are currently working on
> verifying the rest of the rules as well. Verifying rules involves first
> converting the rules to SMT and then using a SMT solver to prove its
> correctness against the model.

Is it possible to use your machinery to generate sets of test cases, maybe
pseudo-random, that can be used to test the code?  As I mentioned before,
formal proofs are nice, but by themselves are of limited usefulness in the
scenario where the validated code base is in a state of change / maintenance.

J