Consensus on unit tests?

[Florian Weimer]

On 07/04/2016 10:44 PM, Carlos O'Donell wrote:
> On 07/04/2016 03:06 PM, Florian Weimer wrote:
>>> There is no precondition that I am aware of. I have clarified the
>>> new patch to say "loadable segment" where I previously said
>>> "segment" to make it more clear.
>>
>> Not even things like “a segment must not cover more than half of the
>> address space” or “a segment must not cross the middle of the address
>> space”?  Or addr >= l->l_addr?
>
> I see no reason why a segment can't cover more than half the address space
> or cross the middle of the address space.
>
> Equally there is nothing wrong with addr being greater than l->l_addr,
> perhaps you meant less than or equal to, which would result in the reladdr
> being wrapped.

Right, I meant less than l_addr.

I wrote a simulator with 6-bit addresses to check my theory that the 
checks were incorrect.  It turns out I was wrong.  I'm attaching it 
nevertheless.  It is written in Ada because it is one of the few 
languages which have a suitable built-in arithmetic type.  (Using 8-bit 
addresses (unsigned char) in C would result in arithmetic being promoted 
to int, giving different results.)

I also verified this with Z3 in two different ways.  The first one gives 
a garbage result (false positive) with the Z3 version in Fedora, but 
correctly reports unsatisfiable with the master branch.

(declare-const l_addr (_ BitVec 4))
(declare-const p_vaddr (_ BitVec 4))
(declare-const p_memsz (_ BitVec 4))
(declare-const addr (_ BitVec 4))
(assert (<= (+ (bv2int l_addr) (bv2int p_vaddr) (bv2int p_memsz)) 15))
(assert (not (= (and (<= (+ (bv2int l_addr) (bv2int p_vaddr))
			 (bv2int addr))
		     (< (bv2int addr)
			(+ (bv2int l_addr) (bv2int p_vaddr)
			   (bv2int p_memsz))))
		(bvult (bvsub (bvsub addr l_addr) p_vaddr) p_memsz))))
(check-sat)

This one appears to work with older versions, too:

(declare-const l_addr (_ BitVec 8))
(declare-const p_vaddr (_ BitVec 8))
(declare-const p_memsz (_ BitVec 8))
(declare-const addr (_ BitVec 8))

(define-fun no-overflow ((a (_ BitVec 8)) (b (_ BitVec 8))) bool
   (bvuge (bvadd a b) a))

(assert (no-overflow l_addr p_vaddr))
(assert (no-overflow (bvadd l_addr p_vaddr) p_memsz))

(define-fun widen ((a (_ BitVec 8))) (_ BitVec 12)
   (concat #x0 a))

(assert (not (= (and (bvule (bvadd (widen l_addr) (widen p_vaddr))
			    (widen addr))
		     (bvult (widen addr)
			    (bvadd (bvadd (widen l_addr) (widen p_vaddr))
				   (widen p_memsz))))
		(bvult (bvsub (bvsub addr l_addr) p_vaddr) p_memsz))))
(check-sat)

I suspect that this boils down to exhaustive search for Z3 as well; the 
run times go up pretty quickly if you increase the bit vector size.

In all cases, the lingering question is whether the translation is 
correct.  It is more obvious with the ACSL translation (due to Pascal Cuoq):

/*@
   requires (a + v + m) ≤ 0x100000000;
   ensures \result == 1 <==> a + v ≤ x < a + v + m;
*/
int f(unsigned a, unsigned v, unsigned m, unsigned x) {
   unsigned r = x - a;
   return r - v < m;
}

But none of the ACSL provers we tried could handle this.

Anyway, I now believe your patch is correct.

Florian
-------------- next part --------------
A non-text attachment was scrubbed...
Name: bug20292.adb
Type: text/x-adasrc
Size: 6023 bytes
Desc: not available
URL: <http://sourceware.org/pipermail/libc-alpha/attachments/20160815/aa9acc52/attachment.bin>