Re: buffer sizes and null pointers

[David Richard Larochelle]

Null pointers and buffer sizes are a tricky issue.

The bounds checking code isn't to detect bounds accesses of null pointers.  
(There is of course separate null terminated checking in splint.)  

There are enough library function that use the convention maxSet(ptr) > N or 
ptr == NULL.

I think that the patch you submitted is probably reasonable solution.  

We need to do some house cleaning with the splint code first, but I should be 
able to add the patch to the cvs tree soon.

The maxSet(NULL) = 0 and maxRead(NULL) = 0 probably makes more sense since 
other splint checking would catches cases of dereferencing a null pointer.


> I wrote:
> > I don't see a way to indicate that a maxSet relationship need only
> > hold if the size is nonzero.  Perhaps maxSet(NULL) == 0 should be
> > assumed?
> 
> Nope, silly me, I keep thinking "how many" when I should be thinking
> "max index", so 0 is no good, it means one location can be set.
> Perhaps -1?  Changing the literal value constructed in my patch still
> produces a version that accepts my test case.
> 
> Ken
> 

buffer sizes and null pointers

[Ken Raeburn]

I'm trying to annotate getnameinfo, which takes among its inputs two
buffer pointers and their lengths.  Each buffer pointer can be null if
the supplied length for it is zero.

I don't see a way to indicate that a maxSet relationship need only
hold if the size is nonzero.  Perhaps maxSet(NULL) == 0 should be
assumed?

The patch below seems to do it.

Ken

 file m3.c
#include 
struct sockaddr;
typedef size_t socklen_t;
extern int getnameinfo (const struct sockaddr *addr, socklen_t addrsz,
/*@out@*/ /*@null@*/ char *h, socklen_t hsz,
/*@out@*/ /*@null@*/ char *s, socklen_t ssz, int flags)
/*@requires (maxSet(h)+1) >= hsz /\ (maxSet(s)+1) >= ssz @*/
/*@modifies *h, *s@*/;

void f (struct sockaddr *sa, socklen_t salen) {
char hbuf[2000];
int r;
 /*13*/ r = getnameinfo (sa, salen, hbuf, (socklen_t) sizeof (hbuf), 0, 0, 0);
if (r == 0) printf ("%s\n", hbuf);
}
 output
% splint +bounds m3.c
Splint 3.0.1.6 --- 25 May 2002

m3.c: (in function f)
m3.c:13:9: Possible out-of-bounds store:
getnameinfo(sa, salen, hbuf, (socklen_t)sizeof((hbuf)), 0, 0, 0)
Unable to resolve constraint:
requires maxSet(0) >= -1
 needed to satisfy precondition:
requires maxSet(0) >= -1
 derived from getnameinfo precondition:
requires maxSet() + 1 >= 
  A memory write may write to an address beyond the allocated buffer. (Use
  -boundswrite to inhibit warning)

Finished checking --- 1 code warning
%
 patch
--- constraintExpr.c~   Wed Jan  9 01:07:43 2002
+++ constraintExpr.cSun May 26 03:25:00 2002
@@ -1359,6 +1359,21 @@
  BADEXIT;
}
 
+  if (constraintTerm_isIntLiteral(cterm) )
+   {
+ if (constraintTerm_getValue(cterm) == 0)
+   {
+ /* Null pointers indicate no readable or settable storage.  */
+ constraintExpr temp;
+
+ temp = constraintExpr_makeIntLiteral (0);
+ constraintExpr_free(c);
+ constraintExpr_free(exp);
+
+ return temp;
+   }
+   }
+
   /* slight Kludge to hanlde var [] = { , , };
   ** type syntax  I don't think this is sounds but it should be good
   ** enough.  The C stanrad is very confusing about initialization

Re: buffer sizes and null pointers

[Ken Raeburn]

I wrote:
> I don't see a way to indicate that a maxSet relationship need only
> hold if the size is nonzero.  Perhaps maxSet(NULL) == 0 should be
> assumed?

Nope, silly me, I keep thinking "how many" when I should be thinking
"max index", so 0 is no good, it means one location can be set.
Perhaps -1?  Changing the literal value constructed in my patch still
produces a version that accepts my test case.

Ken