@@ -4,6 +4,7 @@ import maf.core.Expression
44import maf .language .change .CodeVersion .*
55import maf .language .scheme .SchemeExp
66import maf .modular .*
7+ import maf .modular .scheme .FlowAddr
78import maf .util .ColouredFormatting .*
89import maf .util .Logger
910import maf .util .Logger .*
@@ -55,21 +56,22 @@ trait IncrementalLogging[Expr <: Expression] extends IncrementalDataFlowVisualis
5556 private def legend (): String =
5657 """ ***** LEGEND OF ABBREVIATIONS *****
5758 |ADEP An address value dependency is registered. Includes the "source" address and the address where the value flows to.
58- |ADP* Similar to ADEP, but the address dependency originates from an implicit value flow (e.g., due to a conditional).
5959 |ANLY Analysis of a component, indicating the step of the analysis and the number of times the current component is now analysed.
6060 |CINV Component invalidation: the given component is deleted.
6161 |COMI Indicates the component's analysis is committed.
6262 |DELA Indicates the removal of a given address.
6363 |DINV Dependency invalidation: the component is no longer dependent on the dependency.
6464 |ICFL The components called in a non-empty flow context.
65+ |IFLW The implicit flows added to compute the SCAs.
6566 |IUPD Incremental update of the given address, indicating the value now residing in the store and the value actually written.
6667 |NEWC Discovery of a new, not yet existing component.
6768 |PROV Registration of provenance, including the address and new provenance value, for values that did not cause store changes.
6869 |READ Address read, includes the address and value retrieved from the store.
6970 |RSAD Indicates the address dependencies for a given component are reset.
70- |RSCA Indicates (an address in) a SCA is refined. The number indicates the number of SCA refinement.
71+ |RSCA Indicates (an address in) an SCA is refined. The number indicates the number of SCA refinement.
7172 |SCAC Computed SCA. Shows the algorithm used for this computation.
7273 |SCAR Finds that an SCA needs to be refined and gives the addresses because of which.
74+ |SKIP SCA computation skipped (due to heuristic).
7375 |TRIG Indicates the given dependency has been triggered.
7476 |WRIT Address write, including the address, value written and value now residing in the store.
7577 |
@@ -226,6 +228,19 @@ trait IncrementalLogging[Expr <: Expression] extends IncrementalDataFlowVisualis
226228 if (mode != Summary && (mode != Step || stepSelect())) && ! visited(cmp) then logger.log(s " NEWC ${crop(cmp.toString)}" )
227229 super .spawn(cmp)
228230
231+ override def computeInformationFlow (): Map [W , Set [R ]] =
232+ // Combines the information stored on a per-component basis in dataFlowR.
233+ val flowsR : Map [W , Set [R ]] = dataFlowR.foldLeft(Map ().withDefaultValue(Set [R ]())) { case (res, (_, map)) =>
234+ map.foldLeft(res) { case (res, (w, rs)) => res + (w -> SmartUnion .sunion(res(w), rs)) }
235+ }
236+ val res = super .computeInformationFlow()
237+ res.foreach { (w, rs) =>
238+ rs.diff(flowsR.getOrElse(w, Set ())).foreach { r =>
239+ logger.log(s " IFLW $w ~> $r" )
240+ }
241+ }
242+ res
243+
229244 override def computeSCAs (fullComputation : Boolean ): Set [SCA ] =
230245 val res = super .computeSCAs(fullComputation)
231246 val algo = if fullComputation then " TARJAN" else " INCREMENTAL"
@@ -251,9 +266,24 @@ trait IncrementalLogging[Expr <: Expression] extends IncrementalDataFlowVisualis
251266 rs.exists { r => ! lattice.subsumes(store.getOrElse(r, lattice.bottom), oldStore.getOrElse(r, lattice.bottom)) }
252267 }
253268 if (mode != Summary || stepSelect()) && reasons.nonEmpty
254- then logger.log(s " SCAR $sca because of flows to ${reasons.keySet.mkString(" , " )}" )
269+ then
270+ reasons.foreach { (w, rs) =>
271+ val gone : Set [Addr ] = rs.diff(flowsR(w))
272+ val nonM : Set [Addr ] = rs.filter { r => ! lattice.subsumes(store.getOrElse(r, lattice.bottom), oldStore.getOrElse(r, lattice.bottom)) }
273+ gone.foreach { r =>
274+ logger.log(s " SCAR $r ~ \\ ~> $w: $sca" )
275+ }
276+ nonM.foreach { r =>
277+ logger.log(s " SCAR $r ( ${oldStore.getOrElse(r, lattice.bottom)} => ${store.getOrElse(r, lattice.bottom)}) ~> $w: $sca" )
278+ }
279+ }
255280 super .refiningNeeded(sca, oldStore, oldDataFlowR)
256281
282+ override def updateSCAs (oldStore : Map [Addr , Value ], oldDataFlowR : Map [Component , Map [W , Set [R ]]], cmp : Component ): Unit =
283+ val flowDeleted = oldDataFlowR(cmp).exists((w, rs) => rs.diff(dataFlowR(cmp).getOrElse(w, Set ())).nonEmpty)
284+ if ! (flowDeleted || nonIncrementalUpdate) then logger.log(" SKIP" )
285+ super .updateSCAs(oldStore, oldDataFlowR, cmp)
286+
257287 private var rSCAcount = 0
258288 override def refineSCA (sca : SCA , refinedEntries : Set [Addr ]): Unit =
259289 rSCAcount = rSCAcount + 1
@@ -297,10 +327,6 @@ trait IncrementalLogging[Expr <: Expression] extends IncrementalDataFlowVisualis
297327 if (mode != Select || focus(addr)) && (mode != Step || stepSelect()) then
298328 logger.log(s " ADEP ${crop(r.toString)} ~> ${crop(addr.toString)}" )
299329 )
300- // implicitFlows.flatten.foreach(f =>
301- // if (mode != Select || focus(addr)) && (mode != Step || stepSelect()) then
302- // logger.log(s"ADP* ${crop(f.toString)} ~> ${crop(addr.toString)}")
303- // )
304330 val b = super .writeAddr(addr, value)
305331 if mode == Fine || select(addr) || stepSelect() then
306332 logger.log(
0 commit comments