Skip to content

Commit

Permalink
Fixed merging of transition field initialized state so that the inter…
Browse files Browse the repository at this point in the history
…section operation only depends on the state and field names, not on the ASTs.
  • Loading branch information
mcoblenz committed Jan 17, 2020
1 parent c177d39 commit c5bbb81
Showing 1 changed file with 15 additions and 1 deletion.
16 changes: 15 additions & 1 deletion src/main/scala/edu/cmu/cs/obsidian/typecheck/Checker.scala
Original file line number Diff line number Diff line change
Expand Up @@ -1183,10 +1183,24 @@ class Checker(globalTable: SymbolTable, verbose: Boolean = false) {
val mergedVariableMap = mergeMaps(packedContext1.underlyingVariableMap, packedContext2.underlyingVariableMap, packedContext2.isThrown, context2.isThrown, true)
val mergedThisFieldMap = mergeMaps(packedContext1.thisFieldTypes, packedContext2.thisFieldTypes, packedContext2.isThrown, context2.isThrown, false)

// This is an intersect operation that only depends on the state and field names, not on the ASTs.
def mergeTransitionFieldsInitialized(fields1: Set[(String, String, AST)], fields2: Set[(String, String, AST)]) : Set[(String, String, AST)] = {
var resultingFields = Set[(String, String, AST)]()
for (fieldInitialized <- fields1) {
if (fields2.exists( (otherFieldInitialized: (String, String, AST)) =>
otherFieldInitialized._1 == fieldInitialized._1 &&
otherFieldInitialized._2 == fieldInitialized._2))
{
resultingFields = resultingFields + fieldInitialized
}
}
resultingFields
}

Context(context1.contractTable,
mergedVariableMap,
packedContext1.isThrown,
packedContext1.transitionFieldsDefinitelyInitialized.intersect(packedContext2.transitionFieldsDefinitelyInitialized),
mergeTransitionFieldsInitialized(packedContext1.transitionFieldsDefinitelyInitialized, packedContext2.transitionFieldsDefinitelyInitialized),
packedContext1.transitionFieldsMaybeInitialized.union(packedContext2.transitionFieldsMaybeInitialized),
packedContext1.localFieldsInitialized.intersect(packedContext2.localFieldsInitialized),
mergedThisFieldMap,
Expand Down

0 comments on commit c5bbb81

Please sign in to comment.