Skip to content

Commit 5c39db0

Browse files
CatarinaGamboaCatarinaGamboa
committed
add shared field rule and cleanup repo
1 parent 3830998 commit 5c39db0

8 files changed

Lines changed: 164 additions & 201 deletions

File tree

‎latte-umbrella/src/main/java/context/PermissionEnvironment.java‎

Lines changed: 22 additions & 37 deletions
Original file line numberDiff line numberDiff line change
@@ -31,7 +31,7 @@ public void add(SymbolicValue symb, UniquenessAnnotation ann) {
3131
* Removes the symbolic value in the key from the environment
3232
* @param symb
3333
*/
34-
public void remove(SymbolicValue symb) {
34+
private void remove(SymbolicValue symb) {
3535
for (Map<SymbolicValue, UniquenessAnnotation> innerMap : permEnv) {
3636
if (innerMap.containsKey(symb)) {
3737
innerMap.remove(symb);
@@ -59,7 +59,7 @@ public UniquenessAnnotation get(SymbolicValue symb) {
5959
* Get all symbolic values with Unique as the permission
6060
* @return
6161
*/
62-
public List<SymbolicValue> getUniqueValues() {
62+
List<SymbolicValue> getUniqueValues() {
6363
List<SymbolicValue> values = new ArrayList<SymbolicValue>();
6464
permEnv.forEach( innerMap -> {
6565
innerMap.keySet().forEach(key -> {
@@ -75,7 +75,7 @@ public List<SymbolicValue> getUniqueValues() {
7575
* Remove the values of the given list from the environment
7676
* @param removed
7777
*/
78-
public void removeValues(List<SymbolicValue> removed) {
78+
void removeValues(List<SymbolicValue> removed) {
7979
for (SymbolicValue symbolicValue : removed)
8080
remove(symbolicValue);
8181
}
@@ -94,30 +94,6 @@ public void exitScope() {
9494
permEnv.removeFirst();
9595
}
9696

97-
/**
98-
* String representation of the Permission Environment
99-
*/
100-
@Override
101-
public String toString() {
102-
StringBuilder sb = new StringBuilder();
103-
sb.append("Symbolic Value to Uniqueness Annotations:\n");
104-
105-
for (int i = 0; i < permEnv.size(); i++) {
106-
Map<SymbolicValue, UniquenessAnnotation> currentMap = permEnv.get(i);
107-
sb.append(" Map ").append(i + 1).append(":\n");
108-
109-
for (Map.Entry<SymbolicValue, UniquenessAnnotation> entry : currentMap.entrySet()) {
110-
sb.append(" ")
111-
.append(entry.getKey().toString()) // Key
112-
.append(" -> ")
113-
.append(entry.getValue().toString()) // Value
114-
.append("\n");
115-
}
116-
}
117-
118-
return sb.toString();
119-
}
120-
12197
/**
12298
* Uses the current permission of a symbolic value as another permission
12399
* @return returns true if the permission of vvPerm can be used as fieldPerm
@@ -173,18 +149,27 @@ public PermissionEnvironment cloneLast() {
173149
return clone;
174150
}
175151

176-
public boolean contains(SymbolicValue v) {
177-
return permEnv.stream()
178-
.map(innerMap -> innerMap.containsKey(v))
179-
.reduce(false, (a, b) -> a || b);
180-
}
152+
/**
153+
* String representation of the Permission Environment
154+
*/
155+
@Override
156+
public String toString() {
157+
StringBuilder sb = new StringBuilder();
158+
sb.append("Symbolic Value to Uniqueness Annotations:\n");
181159

182-
public void update(SymbolicValue v, UniquenessAnnotation ua) {
183-
for (Map<SymbolicValue, UniquenessAnnotation> innerMap : permEnv) {
184-
if (innerMap.containsKey(v)) {
185-
innerMap.put(v, ua);
186-
return;
160+
for (int i = 0; i < permEnv.size(); i++) {
161+
Map<SymbolicValue, UniquenessAnnotation> currentMap = permEnv.get(i);
162+
sb.append(" Map ").append(i + 1).append(":\n");
163+
164+
for (Map.Entry<SymbolicValue, UniquenessAnnotation> entry : currentMap.entrySet()) {
165+
sb.append(" ")
166+
.append(entry.getKey().toString()) // Key
167+
.append(" -> ")
168+
.append(entry.getValue().toString()) // Value
169+
.append("\n");
187170
}
188171
}
172+
173+
return sb.toString();
189174
}
190175
}

‎latte-umbrella/src/main/java/context/SymbolicEnvironment.java‎

Lines changed: 32 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -144,26 +144,26 @@ SymbolicValue get(VariableHeapLoc var) {
144144
return null;
145145
}
146146

147-
public Set<VariableHeapLoc> keySet(){
147+
Set<VariableHeapLoc> keySet(){
148148
return symbEnv.stream()
149149
.map(Map::keySet)
150150
.flatMap(Set::stream)
151151
.collect(Collectors.toSet());
152152
}
153153

154-
public void remove(VariableHeapLoc key){
154+
void remove(VariableHeapLoc key){
155155
for( Map<VariableHeapLoc, SymbolicValue> map : symbEnv)
156156
if(map.containsKey(key))
157157
map.remove(key);
158158
}
159159

160-
public boolean hasValue(SymbolicValue v) {
160+
boolean hasValue(SymbolicValue v) {
161161
return symbEnv.stream()
162162
.map(innerMap -> innerMap.containsValue(v))
163163
.reduce(false, (a, b) -> a || b);
164164
}
165165

166-
public boolean hasFieldWithValue(SymbolicValue v){
166+
boolean hasFieldWithValue(SymbolicValue v){
167167
return symbEnv.stream()
168168
.map(innerMap -> innerMap.entrySet().stream()
169169
.anyMatch(entry -> entry.getKey() instanceof FieldHeapLoc && entry.getValue().equals(v)))
@@ -175,7 +175,7 @@ public boolean hasFieldWithValue(SymbolicValue v){
175175
* Remove unreachable values
176176
* @return List of removed symbolic values
177177
*/
178-
public List<SymbolicValue> removeUnreachableValues() {
178+
List<SymbolicValue> removeUnreachableValues() {
179179
// 1) get all symbolic values in the keys that are part of fields in the heap
180180
List<FieldHeapLoc> keys = new ArrayList<>();
181181
List<SymbolicValue> returns = new ArrayList<>();
@@ -216,27 +216,11 @@ public void exitScope() {
216216
symbEnv.removeFirst();
217217
}
218218

219-
@Override
220-
public String toString() {
221-
StringBuilder sb = new StringBuilder();
222-
sb.append("Symbolic Environment:\n");
223-
224-
for (int i = 0; i < symbEnv.size(); i++) {
225-
Map<VariableHeapLoc, SymbolicValue> map = symbEnv.get(i);
226-
sb.append(" Map ").append(i + 1).append(":\n");
227-
228-
for (Map.Entry<VariableHeapLoc, SymbolicValue> entry : map.entrySet()) {
229-
sb.append(" ")
230-
.append(entry.getKey().toString()) // Key
231-
.append(" -> ")
232-
.append(entry.getValue().toString()) // Value
233-
.append("\n");
234-
}
235-
}
236-
237-
return sb.toString();
238-
}
239-
219+
/**
220+
* Checks if all the symbolic values are distinct
221+
* @param paramSymbValues
222+
* @return
223+
*/
240224
public boolean distinct(List<SymbolicValue> paramSymbValues) {
241225
if (paramSymbValues.size() < 2) return true;
242226
List<Pair<SymbolicValue, SymbolicValue>> lp =
@@ -311,6 +295,28 @@ public boolean isEmpty() {
311295
return symbEnv.stream().allMatch(Map::isEmpty);
312296
}
313297

298+
@Override
299+
public String toString() {
300+
StringBuilder sb = new StringBuilder();
301+
sb.append("Symbolic Environment:\n");
302+
303+
for (int i = 0; i < symbEnv.size(); i++) {
304+
Map<VariableHeapLoc, SymbolicValue> map = symbEnv.get(i);
305+
sb.append(" Map ").append(i + 1).append(":\n");
306+
307+
for (Map.Entry<VariableHeapLoc, SymbolicValue> entry : map.entrySet()) {
308+
sb.append(" ")
309+
.append(entry.getKey().toString()) // Key
310+
.append(" -> ")
311+
.append(entry.getValue().toString()) // Value
312+
.append("\n");
313+
}
314+
}
315+
316+
return sb.toString();
317+
}
318+
319+
314320
}
315321

316322

‎latte-umbrella/src/main/java/context/Variable.java‎

Lines changed: 0 additions & 28 deletions
This file was deleted.

‎latte-umbrella/src/main/java/context/VariableHeapLoc.java‎

Lines changed: 36 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,13 @@
11
package context;
22

3+
/**
4+
* Represents a variable or a field in the heap
5+
*/
36
public abstract class VariableHeapLoc {}
47

8+
/**
9+
* Represents a field in the heap
10+
*/
511
class FieldHeapLoc extends VariableHeapLoc{
612

713
SymbolicValue heapLoc;
@@ -34,3 +40,33 @@ public String toString() {
3440
return heapLoc.toString() + "." + field.toString();
3541
}
3642
}
43+
44+
/*
45+
* Represents a variable
46+
*/
47+
class Variable extends VariableHeapLoc{
48+
49+
String name;
50+
51+
public Variable(String name) {
52+
this.name = name;
53+
}
54+
55+
@Override
56+
public String toString() {
57+
return "Variable{" +
58+
"name='" + name + '\'' +
59+
'}';
60+
}
61+
62+
@Override
63+
public int hashCode() {
64+
return name.hashCode();
65+
}
66+
67+
@Override
68+
public boolean equals(Object obj) {
69+
return obj instanceof Variable && ((Variable) obj).name.equals(name);
70+
}
71+
72+
}

‎latte-umbrella/src/main/java/context/VariableT.java‎

Lines changed: 0 additions & 63 deletions
This file was deleted.

‎latte-umbrella/src/main/java/typechecking/LatteException.java‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,9 @@ public LatteException(String message, CtElement ce) {
99
this.ce = ce;
1010
}
1111

12+
/*
13+
* Retain the element that caused the exception
14+
*/
1215
public CtElement getElement(){
1316
return ce;
1417
}

‎latte-umbrella/src/main/java/typechecking/LatteProcessor.java‎

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,10 @@ abstract class LatteProcessor extends CtScanner{
1717

1818
final String THIS = "this";
1919

20+
// * Metadata keys:
21+
// * EVAL_KEY -> SymbolicValue
22+
final String EVAL_KEY = "symbolic_value";
23+
2024
int loggingSpaces = 0;
2125

2226
public LatteProcessor( SymbolicEnvironment symbEnv,
@@ -64,11 +68,10 @@ protected void logError(String text, CtElement ce) throws LatteException {
6468
.append("\tFile: ")
6569
.append(filePath).append(":").append(line).append(":").append(column).append("\n"); // Clickable format
6670

67-
throw new LatteException(sb.toString(), ce);
68-
71+
throw new LatteException(sb.toString(), ce);
6972
}
7073

71-
/**
74+
/**
7275
* Enter scopes from all environments
7376
*/
7477
protected void enterScopes(){

0 commit comments

Comments
 (0)