Strange error with primitive types and casts

Nov 16, 2012 at 2:41 PM

Hi,


Consider the following simple code:

 

#include <vcc.h>
#include <math.h>
float Distance(float *x, float *y, int n)
  _(requires n > 0)
{
    int i;
    float sum = 0.0f;

    for (i = 0; i < n; i++) 
    {
        sum = sum + (x[i] - y[i])*(x[i] - y[i]);
    }
    return (float) sqrt(sum);
}

 

 

The current version of vcc yields: 

e:\strange-error-1.c(13,25) : error VC9600: OOPS: unhandled expr (Microsoft.Research.Vcc.CAST+PrimKind)sum
Verification errors in 3 function(s)
Exiting with 3 (1 error(s).)

 

I have another version with read and write clauses, etc. It makes no difference. The detailed Boogie code dump (obtained with /d) is below. The error seems related to the cast from double to float (in bold above in C and below in Boogie)

 

Microsoft.Research.Vcc.CAST+PrimKind Distance(Microsoft.Research.Vcc.CAST+PrimKi
nd* x, Microsoft.Research.Vcc.CAST+PrimKind* y, int32_t n)
  requires >(n, 0);
{
  // assume true
  // assume true
  assume @in_range_i4(n);
  assume @decreases_level_is(2147483647);
  // assume true
  Microsoft.Research.Vcc.CAST+PrimKind* x;
  Microsoft.Research.Vcc.CAST+PrimKind* y;
  int32_t n;
  Microsoft.Research.Vcc.CAST+PrimKind sum;
  int32_t i;
  // var int32_t i
  sum := @float_literal(userdata(0) : Single);
  i := 0;
  loop
    {
      assume @_vcc_meta_eq(old(@prestate, @state), @state);
      if (<(i, n))
        {
          // assert true
          // assert true
          // assert true
          assert @reads_check_normal(x[i]);
          assert @reads_check_normal(y[i]);
          // assert true
          assert @reads_check_normal(x[i]);
          assert @reads_check_normal(y[i]);
          sum := +(sum, *(-(*(x[i]), *(y[i])), -(*(x[i]), *(y[i]))));
        }
      else
        {
          assert @_vcc_possibly_unreachable;
          goto #break_1;
        }
      #continue_1:
      assert @in_range_i4(+(i, 1));
      i := +(i, 1);
    }
  #break_1:
  Microsoft.Research.Vcc.CAST+PrimKind res_sqrt#4;
  res_sqrt#4 := sqrt((Microsoft.Research.Vcc.CAST+PrimKind)sum);
  return (Microsoft.Research.Vcc.CAST+PrimKind)res_sqrt#4;
  skip;
}


 

I should avoid mixing float and double in the current version of VCC, I guess? 

Thanks. Best,

Eduardo 

Nov 16, 2012 at 4:31 PM

Actually there seems to be lack of reliable support for simple operations using type float or double. For instance, given:

#include <vcc.h>

extern
float _(pure) foo(float v);

int foo2() 
{
  int x = 0;
  float a = 0.0f;
  float b = 1.0f;

  if ( foo(a) < foo(b))
    x = 1;
  return x;
}

vcc yields 

OOPS: pruning: cannot find _Bool op_LessThan()
 : Microsoft.Research.Vcc.CAST+Function
Exiting with 3 (1 error(s).)

If I change the type to double, then I get a different error. Given: 

#include <vcc.h>

extern
double _(pure) foo(double v);

int foo2()
{
  int x = 0;
  double a = 0.0;
  double b = 1.0;

  if ( foo(a) < foo(b))
    x = 1;
  return x;
}

 

vcc this time yields 

 

(0,0) : error : invalid argument types ($primitive and $primitive) to binary operator <
(0,0) : error : invalid argument types ($primitive and $primitive) to binary operator <=
attempting to dump BPL to buggy.bpl
Verification errors in 1 function(s)
Exiting with 3 (1 error(s).)

The relevant part of the  buggy.bpl file is

 

function F#foo(P#v: $primitive) : $primitive;

const unique cf#foo: $pure_function;

axiom $function_arg_type(cf#foo, 0, ^^f8);

axiom $function_arg_type(cf#foo, 1, ^^f8);

procedure foo(P#v: $primitive) returns ($result: $primitive);
  free ensures $result == F#foo(P#v);
  free ensures $call_transition(old($s), $s);


procedure foo2() returns ($result: int);
  modifies $s, $cev_pc;
  free ensures $in_range_i4($result);
  free ensures $writes_nothing(old($s), $s);
  free ensures $call_transition(old($s), $s);


implementation foo2() returns ($result: int)
{
  var res_foo#2: $primitive;
  var res_foo#1: $primitive;
  var L#x: int where $in_range_i4(L#x);
  var L#a: $primitive;
  var L#b: $primitive;
  var #wrTime$1^7.1: int;
  var #stackframe: int;

  anon3:
    assume $function_entry($s);
    assume $full_stop_ext(#tok$1^7.1, $s);
    assume $can_use_all_frame_axioms($s);
    assume #wrTime$1^7.1 == $current_timestamp($s);
    assume $def_writes($s, #wrTime$1^7.1, (lambda #p: $ptr :: false));
    // assume @decreases_level_is(2147483647);
    assume 2147483647 == $decreases_level;
    // Microsoft.Research.Vcc.CAST+PrimKind b;
    // Microsoft.Research.Vcc.CAST+PrimKind a;
    // int32_t x;
    // x := 0;
    L#x := 0;
    // a := @float_literal(userdata(0) : Double);
    L#a := floatLiteral#3;
    // b := @float_literal(userdata(1) : Double);
    L#b := floatLiteral#4;
    // Microsoft.Research.Vcc.CAST+PrimKind res_foo#1;
    // res_foo#1 := foo(a);
    call res_foo#1 := foo(L#a);
    assume $full_stop_ext(#tok$1^13.8, $s);
    // Microsoft.Research.Vcc.CAST+PrimKind res_foo#2;
    // res_foo#2 := foo(b);
    call res_foo#2 := foo(L#b);
    assume $full_stop_ext(#tok$1^13.17, $s);
    assume true;
    // if (<(res_foo#1, res_foo#2)) ...
    if (res_foo#1 < res_foo#2)
    {
      anon1:
        // x := 1;
        L#x := 1;
    }
    else
    {
      anon2:
        // assert @_vcc_possibly_unreachable;
        assert {:PossiblyUnreachable true} true;
    }

  anon4:
    // return x;
    $result := L#x;
    assume true;
    assert $position_marker();
    goto #exit;

  anon5:
    // skip

  #exit:
}

 

Developer
Jan 21, 2013 at 10:45 PM

Yes, VCC essentially doesn't support floating point, and probably won't until the next version.