in Sources/SolToBoogie/TransUtils.cs [125:212]
public static bool IsUintConst(this TypeDescription typeDescription, Expression constant, out BigInteger value, out uint sz)
{
sz = 256;
try
{
var type = typeDescription.ToString();
if (type.StartsWith("int_const"))
{
if (constant is Literal)
{
string constStr = ((Literal)constant).Value;
value = BigInteger.Parse(constStr);
int res = GetConstantSize(value);
if (res == -1)
{
// Constant > 2^256:
Console.WriteLine($"Warning: uint constant > 2**256");
sz = 256;
return true;
}
else
{
sz = (uint)res;
return true;
}
}
else if (constant is BinaryOperation)
{
BinaryOperation binaryConstantExpr = (BinaryOperation)constant;
if (binaryConstantExpr.LeftExpression is Literal && binaryConstantExpr.RightExpression is Literal)
{
// Get expression value from TypeDescriptions (but not if the constant is too big)
string typeStr = binaryConstantExpr.TypeDescriptions.TypeString;
if (typeDescription.TypeString.Contains("omitted"))
{
// Large constant which is abbreviated in the typeDescription:
// This would probably never happen, because Solidity compiler reports type errors for such constants
Console.WriteLine($"Warning: constant expression contains large constant(s);");
Console.WriteLine($"if the large constant is an operand in a power operation,");
Console.WriteLine($"modulo arithmetic check will not work correctly");
value = 0;
sz = 256;
return false;
}
else
{
value = BigInteger.Parse(GetNumberFromEnd(typeStr));
sz = 256;
return true;
}
}
else
{
// TODO: The warning below could probably be suppressed:
// this is the case of exprs like (2+2+2...), where left and right expressions are BinaryOperation;
// in these cases, "value" is never used (it is only used for power operation on two literals)
Console.WriteLine($"Warning in IsUintConst: constant expression is neither Literal nor BinaryOperation with Literal operands; hint: use temps for subexpressions");
value = 0;
sz = 256;
return false;
}
}
else
{
// TODO: constant is TupleExpression:
Console.WriteLine($"Warning in IsUintConst: constant expression is neither Literal nor BinaryOperation; hint: use temps for subexpressions");
value = 0;
sz = 256;
return false;
}
}
else
{
sz = 256;
value = 0;
return false;
}
}
catch (Exception e)
{
Console.WriteLine($"VeriSol translation error: exception in IsUintConst: {e.Message}");
value = 0;
sz = 256;
return false;
}
}