AV: Problem with generalization of repetead fields

[rcastano]

Steps to reproduce:

1. Create the file input.bpl with the following contents:

type Ref;

const unique r1 : Ref;
const unique r2 : Ref;
const unique r3 : Ref;
const unique r4 : Ref;
const unique r5 : Ref;
const unique null : Ref;
var m : [Ref] Ref;

procedure Foo(r : Ref) {
  assert m[r] != r1;
  assert m[r] != r2;
  assert m[r] != r3;
  assert m[r] != r4;
  assert m[r] != r5;
}

2. run AvHarnessInstrumentation.exe input.bpl input_inst.bpl /unknownType:Ref /unknownType:int
3. run AngelicVerifierNull.exe .\input_inst.bpl /nodup /traceSlicing /copt:recursionBound:5 /copt:k:1 /copt:tryCTr ace /EE:noFilters /EE:onlyDisplayAliasingInPre- /sdv > AvnOutput
   The output contains the following:

[TAG: AV_DEBUG] Generalizing field block expression for m[alloc_r_Foo__14] != r5 to (forall _z: Ref :: m[_z] > 0)
[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall _z: Ref :: m[_z] > 0)
[...]
PersistentProgram(129,91): Error: invalid argument types (Ref and int) to binary operator >
Corral took: 0.01 seconds
Corral call terminates inconclusively with Type errors...

The code involved is the following:

corral/AddOns/AngelicVerifierNull/AngelicVerifierNull/Program.cs

Lines 1682 to 1714 in b3b26bb

	private static Expr AbstractRepeatedMapsInBlock(Expr expr, HashSet<Variable> supportVars)
	{
	var repeatedFields = new HashSet<Variable>();
	//once a field has been generalized, we should not see blocks over it
	supportVars.Iter(x =>
	{
	if (x.TypedIdent.Type.IsMap && x.TypedIdent.Type.AsMap.MapArity == 1)
	{
	var xstr = x.ToString();
	if (fieldInBlockCount.ContainsKey(xstr))
	fieldInBlockCount[xstr]++;
	else
	fieldInBlockCount[xstr] = 1;
	if (fieldInBlockCount[xstr] > MAX_REPEATED_FIELDS_IN_BLOCKS)
	repeatedFields.Add(x);
	}
	}
	);
	if (repeatedFields.Count == 0) return null;
	Expr returnExpr = null;
	foreach (var m in repeatedFields)
	{
	var bvar = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "_z", m.TypedIdent.Type.AsMap.Arguments[0]));
	var fexpr = Expr.Gt(BoogieAstFactory.MkMapAccessExpr(m, IdentifierExpr.Ident(bvar)),
	new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(0)));
	var forallExpr = new ForallExpr(Token.NoToken, new List<Variable>() { bvar }, fexpr);
	if (returnExpr == null)
	returnExpr = forallExpr;
	else
	returnExpr = Expr.And(returnExpr, forallExpr);
	}
	return returnExpr;
	}

Note: Unrelated to this issue due to how and when the Corral exception is caught, another exception is thrown. The following message in the output appears after the type error:

Corral call terminates inconclusively with The process cannot access the file 'C:\Users\Doc\repos\test_null_check\bug_gt_0\error.bpl' because it is being used by another process....

I'm not sure what the desired behavior in these cases would be and if a separate issue should be created.

[rcastano]

Another similar input file that triggers the problem without the type error:

type Ref;

var m : [Ref] int;
const unique null : Ref;
procedure Foo(r : Ref) {
  assert m[r] != -1;
  assert m[r] != -2;
  assert m[r] != -3;
  assert m[r] != -4;
  assert m[r] != -5;
}

The generalized expression does not imply the other assertions.