[klee-dev] curiosity question about runtime procedure range_check

[David Lightstone]

I am curious to know the reason for the type conversions to unsigned in
range_check (code provided below)

Everything is probably fine if klee_make_symbolic is known to a priori
always return a quantity greater than 0 when start == 0
Things are a bit dicey when klee_make_symbolic has coding errors.
 
The apparent optimization has to side effects:
(1) It creates a coupling between range_check and klee_make_symbolic which
might not be desirable 
(2) It defeats the entire purpose of assume type checking (to allow
reasoning about behavior)

My guess it is a covert attempt to achieve polymorphism in a language not
designed to support polymorphism.

Comments

Dave Lightstone


#include <assert.h>
#include <klee/klee.h>

int klee_range(int start, int end, const char* name) {
  int x;

  if (start >= end)
    klee_report_error(__FILE__, __LINE__, "invalid range", "user");

  if (start+1==end) {
    return start;
  } else {
    klee_make_symbolic(&x, sizeof x, name); 

    /* Make nicer constraint when simple... */
    if (start==0) {
      klee_assume((unsigned) x < (unsigned) end);
    } else {
      klee_assume(start <= x);
      klee_assume(x < end);
    }

    return x;
  }
}