-checksafety option: improving the safety analysis in loops

[tfaoliveira]

Consider the following code, where function f1_while_scale adds all elements from global array c. The safety checker does not find any violation for this example.

u16[16] c = 
{ 1,1,1,1,
  2,2,2,2,
  3,3,3,3,
  4,4,4,4
};

inline fn f1_while_scale() -> reg u16
{
  reg u64 i;
  reg u16 r;
  reg ptr u16[16] cp;
  
  i = 0;
  r = 0;
  cp = c;
  while(i < 16)
  { r += cp[(int) i];
    i += 1;
  }
  
  return r;
}

export fn e1_while_scale() -> reg u16
{
  reg u16 r;
  r = f1_while_scale();
  return r;
}

Now consider a different implementation of the previous program where cp[(int) i] is replaced by cp.[(int) i] (no scale factor) and variable i is incremented by 2. The loop condition is also changed accordingly.

u16[16] c = 
{ 1,1,1,1,
  2,2,2,2,
  3,3,3,3,
  4,4,4,4
};

inline fn f2_while_no_scale() -> reg u16
{
  reg u64 i;
  reg u16 r;
  reg ptr u16[16] cp;
  
  i = 0;
  r = 0;
  cp = c;
  // i < 32           : *** Possible Safety Violation(s): line 23: in_bound: cp.[U16 ((int of u64) i) ] (length 32 U8)
  // i < 31           : *** No Safety Violation
  // i < (32-1)       : *** No Safety Violation
  // i < ((16*2) - 1) : *** Possible Safety Violation(s): line 23: in_bound: cp.[U16 ((int of u64) i) ] (length 32 U8)
  while(i < 32 )
  { r += cp.[(int) i]; 
    i += 2;
  }
  
  return r;
}

export fn e2_while_no_scale() -> reg u16
{
  reg u16 r;
  r = f2_while_no_scale();
  return r;
}

In this last example, when the condition of the loop is i < 32, a "possible safety violation" warning is printed, which makes sense if we assume that, and in this case, only the loop condition taken into consideration during the analysis (i < 32) and thus, using just that information, i could actually be 31. If i is 31, the u16 read from the expression cp.[(int) i] is invalid.

If we change the condition to i < 31 (which does not change the computation since i is pair) the warning disappears. It would be interesting if the safety analysis could take into account how loop variables get incremented/decremented.

I pushed some files here: https://github.com/tfaoliveira/jasmin/tree/master/safetycheck-u16

• In safetycheck-u16 folder, there is a sequence of examples (1..7.jazz) that can be used to test the safety checker for the described issue. Examples that currently fail are: 2.jazz (shown here); and 5.jazz, 6.jazz and 7.jazz (unrolled versions of the previous examples that also include an external pointer in the computation).
• It should be enough to run make if jasminc is in the PATH.
• For the examples that fail there should be a *.FIXME file and the outputs of the safety analysis are redirected to *.cs files.