Re: Consensus on unit tests?

[Florian Weimer <fweimer at redhat dot com>]

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

--  Simulat whole-address checks for _dl_addr_inside_object.

with Ada.Text_IO;

procedure Bug20292 is
   --  Our address space is just 6 bits large (so that we can easily
   --  print diagrams).  All arithmetic wraps around (unless type
   --  converions are applied).  There is no implicit promotion to
   --  another arithmetic type.
   type Address is mod 2**6;

   --  Approximation of struct link_map.
   type Link_Map is record
      L_Addr : Address;

      --  In the oringal, these fields are actually nested in an
      --  array.
      P_Vaddr : Address;
      P_Memsz : Address;
   end record;

   --  Return True if the link map described by the argument does not
   --  exceed beyond the end of the address space.  Used to filter out
   --  invalid test cases.
   function Valid_Link_Map (L : Link_Map) return Boolean
   is
      --  Perform the computations without wraparound.
      type Large_Address is range 0 .. 3 * Integer (Address'Last);
      Addr : constant Large_Address := Large_Address (L.L_Addr);
      Vaddr : constant Large_Address := Large_Address (L.P_Vaddr);
      Memsz : constant Large_Address := Large_Address (L.P_Memsz);
      Last : constant Large_Address := Large_Address (Address'Last);
   begin
      --  The sum is the logical address of the byte after the memory
      --  range covering the mapping.
      return Addr + Vaddr + Memsz <= Last + 1;
   end Valid_Link_Map;

   --  Ada translation of _dl_addr_inside_object (without the loop
   --  over l_phnum).
   function Address_Inside_Object (L : Link_Map; Addr : Address) return Boolean
   is
      Reladdr : constant Address := Addr - L.L_Addr;
   begin
      --  reladdr - l->l_phdr[n].p_vaddr < l->l_phdr[n].p_memsz
      return Reladdr - L.P_Vaddr < L.P_Memsz;
   end Address_Inside_Object;

   --  A vew of an address space where certain addresses are occupied
   --  (indicated by set bits).
   type Address_Map is array (Address'Range) of Boolean;

   --  Convert the link map to an explicit address space view where
   --  the covered bits are set.
   function Link_Map_To_Address_Space (L : Link_Map) return Address_Map is
      --  Perform the computations without wraparound.
      type Large_Address is range -1 .. 3 * Integer (Address'Last);
      Addr : constant Large_Address := Large_Address (L.L_Addr);
      Vaddr : constant Large_Address := Large_Address (L.P_Vaddr);
      Memsz : constant Large_Address := Large_Address (L.P_Memsz);

      First : constant Large_Address := Addr + Vaddr;
      Last : constant Large_Address := First + Memsz - 1;

      --  Initially, the address space is empty.
      Address_Space : Address_Map := (others => False);
   begin
      --  Populate the addresses which fall into the range.
      for J in First .. Last loop
         Address_Space (Address (J)) := True;
      end loop;
      return Address_Space;
   end Link_Map_To_Address_Space;

   --  Print out the address space.
   procedure Print_Map (Map : Address_Map) is
      use Ada.Text_IO;
   begin
      for J in Map'Range loop
         if Map (J) then
            Put ('X');
         else
            Put ('.');
         end if;
      end loop;
      New_Line;
   end Print_Map;

   --  Direction of the pointer.
   type Direction is (Upwards, Downwards);

   --  Print a pointer into the address space.
   procedure Print_Pointer (Addr : Address; Dir : Direction; Label : String) is
      use Ada.Text_IO;
   begin
      --  Leading white space to position the pointer.
      for J in 1 .. Addr loop
         Put (' ');
      end loop;

      --  The arrow.
      case Dir is
         when Upwards =>
            Put ('^');
         when Downwards =>
            Put ('v');
      end case;

      --  The label for the pointer.
      Put (' ');
      Put_Line (Label);
   end Print_Pointer;

   --  Used to indicate test failure.
   Test_Failure : exception;

   --  For each address in the address space, check that
   --  Address_Inside_Object returns the expected value.
   procedure Check_Link_Map (L : Link_Map) is
      Address_Space : constant Address_Map
        := Link_Map_To_Address_Space (L);
      Inside_Count : Integer := 0;
      use Ada.Text_IO;
   begin
      for Probe in Address'Range loop
         declare
            Actual : constant Boolean := Address_Inside_Object (L, Probe);
            Expected : constant Boolean := Address_Space (Probe);
         begin
            if Actual /= Expected then
               Put_Line ("Address_Inside_Object: " & Boolean'Image (Actual));
               Put_Line ("Expected: " & Boolean'Image (Expected));
               New_Line;
               Put_Line ("l_addr:" & Address'Image (L.L_Addr));
               Put_Line ("p_vaddr:" & Address'Image (L.P_Vaddr));
               Put_Line ("p_memsz:" & Address'Image (L.P_Memsz));
               New_Line;
               Print_Pointer (L.L_Addr, Downwards, "l_addr");
               Print_Map (Address_Space);
               Print_Pointer (Probe, Upwards, "test address");
               raise Test_Failure;
            end if;

            if Expected then
               Inside_Count := Inside_Count + 1;
            end if;
         end;
      end loop;

      --  Paranoia check to see if the addres space was consistent.
      if Inside_Count /= Integer (L.P_Memsz) then
         Put_Line ("Inside_Count:" & Integer'Image (Inside_Count));
         Put_Line ("p_memsz:" & Address'Image (L.P_Memsz));
         raise Test_Failure;
      end if;
   end Check_Link_Map;

begin
   for L_Addr in Address'Range loop
      for P_Vaddr in Address'Range loop
         for P_Memsz in Address'Range loop
            declare
               L : constant Link_Map := (L_Addr => L_Addr,
                                         P_Vaddr => P_Vaddr,
                                         P_Memsz => P_Memsz);
            begin
               if Valid_Link_Map (L) then
                  Check_Link_Map (L);
               end if;
            end;
         end loop;
      end loop;
   end loop;
end Bug20292;