1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
|
//-----------------------------------------------------------------------------
//
// Copyright (C) Microsoft Corporation. All Rights Reserved.
//
//-----------------------------------------------------------------------------
using System;
using System.Text;
using System.IO;
using System.Collections;
using System.Collections.Generic;
using Microsoft.Contracts;
using Microsoft.Basetypes;
// Code for replacing large integer literals in VCExpr with
// constants. This is necessary for Simplify, which cannot deal with
// literals larger than 32 bits
namespace Microsoft.Boogie.VCExprAST
{
public class BigLiteralAbstracter : MutatingVCExprVisitor<bool>, ICloneable {
public BigLiteralAbstracter(VCExpressionGenerator! gen) {
base(gen);
DummyVar = gen.Variable("x", Type.Int);
IncAxioms = new List<VCExpr!> ();
Literals = new List<KeyValuePair<BigNum, VCExprVar!>> ();
}
private BigLiteralAbstracter(BigLiteralAbstracter! abstracter) {
base(abstracter.Gen);
DummyVar = abstracter.DummyVar;
IncAxioms = new List<VCExpr!> (abstracter.IncAxioms);
Literals = new List<KeyValuePair<BigNum, VCExprVar!>> (abstracter.Literals);
}
public Object! Clone() {
return new BigLiteralAbstracter(this);
}
private static readonly BigNum ConstantDistance = BigNum.FromLong(100000);
private static readonly BigNum NegConstantDistance = BigNum.FromLong(-100000);
// distance twice plus one
private static readonly BigNum ConstantDistanceTPO = BigNum.FromLong(200001);
private static readonly BigNum ConstantDistancePO = BigNum.FromLong(100001);
public VCExpr! Abstract(VCExpr! expr) {
return Mutate(expr, true);
}
////////////////////////////////////////////////////////////////////////////
// list in which axioms are incrementally collected
private readonly List<VCExpr!>! IncAxioms;
private void AddAxiom(VCExpr! axiom) {
IncAxioms.Add(axiom);
}
// Return all axioms that were added since the last time NewAxioms
// was called
public VCExpr! GetNewAxioms() {
VCExpr! res = Gen.NAry(VCExpressionGenerator.AndOp, IncAxioms);
IncAxioms.Clear();
return res;
}
////////////////////////////////////////////////////////////////////////////
// All named integer literals known to the visitor, in ascending
// order. Such literals are always positive, and the distance
// between two literals is always more than ConstantDistance.
private readonly List<KeyValuePair<BigNum, VCExprVar!>>! Literals;
private class EntryComparerC : IComparer<KeyValuePair<BigNum, VCExprVar!>> {
public int Compare(KeyValuePair<BigNum, VCExprVar!> a,
KeyValuePair<BigNum, VCExprVar!> b) {
return a.Key.CompareTo(b.Key);
}
}
private static readonly EntryComparerC EntryComparer = new EntryComparerC ();
// variable used when searching for entries in the literal list
private readonly VCExprVar! DummyVar;
////////////////////////////////////////////////////////////////////////////
// Construct an expression to represent the given (large) integer
// literal. Constants are defined and axiomatised if necessary
private VCExpr! Represent(BigNum lit)
requires NegConstantDistance > lit || lit > ConstantDistance; {
if (lit.IsNegative)
return Gen.Function(VCExpressionGenerator.SubOp,
Gen.Integer(BigNum.ZERO), RepresentPos(lit.Neg));
else
return RepresentPos(lit);
}
private VCExpr! RepresentPos(BigNum lit)
requires lit > ConstantDistance; {
int index = GetIndexFor(lit);
if (index >= 0)
// precise match
return Literals[index].Value;
// check whether a constant is defined that is at most
// ConstantDistance away from lit
index = ~index;
VCExpr res = null;
BigNum resDistance = ConstantDistancePO;
if (index > 0) {
BigNum dist = lit - Literals[index - 1].Key;
if (dist < resDistance) {
resDistance = dist;
res = Gen.Function(VCExpressionGenerator.AddOp,
Literals[index - 1].Value, Gen.Integer(dist));
}
}
if (index < Literals.Count) {
BigNum dist = Literals[index].Key - lit;
if (dist < resDistance) {
resDistance = dist;
res = Gen.Function(VCExpressionGenerator.SubOp,
Literals[index].Value, Gen.Integer(dist));
}
}
if (res != null)
return res;
// otherwise, define a new constant to represent this literal
return AddConstantFor(lit);
}
private VCExpr! AddConstantFor(BigNum lit)
requires lit > ConstantDistance; {
VCExprVar! res = Gen.Variable("int#" + lit, Type.Int);
int index = GetIndexFor(lit);
assert index < 0;
index = ~index;
Literals.Insert(index, new KeyValuePair<BigNum, VCExprVar!>(lit, res));
// relate the new constant to the predecessor and successor
if (index > 0)
DefineRelationship(Literals[index - 1].Value, Literals[index - 1].Key,
res, lit);
else
DefineRelationship(Gen.Integer(BigNum.ZERO), BigNum.ZERO, res, lit);
if (index < Literals.Count - 1)
DefineRelationship(res, lit,
Literals[index + 1].Value, Literals[index + 1].Key);
return res;
}
private void DefineRelationship(VCExpr! aExpr, BigNum aValue,
VCExpr! bExpr, BigNum bValue)
requires aValue < bValue; {
BigNum dist = bValue - aValue;
VCExpr! distExpr = Gen.Function(VCExpressionGenerator.SubOp, bExpr, aExpr);
if (dist <= ConstantDistanceTPO)
// constants that are sufficiently close to each other are put
// into a precise relationship
AddAxiom(Gen.Eq(distExpr, Gen.Integer(dist)));
else
AddAxiom(Gen.Function(VCExpressionGenerator.GtOp,
distExpr, Gen.Integer(ConstantDistanceTPO)));
}
private int GetIndexFor(BigNum lit) {
return Literals.BinarySearch(new KeyValuePair<BigNum, VCExprVar!>
(lit, DummyVar),
EntryComparer);
}
////////////////////////////////////////////////////////////////////////////
public override VCExpr! Visit(VCExprLiteral! node, bool arg) {
VCExprIntLit intLit = node as VCExprIntLit;
if (intLit != null) {
if (NegConstantDistance > intLit.Val || intLit.Val > ConstantDistance)
return Represent(intLit.Val);
}
return node;
}
}
}
|
