IR Program Slicing #476
IR Program Slicing #476
Conversation
Better grouping of the different commands in the match.
Allows for the definition of IDE Analysis Edges without a Program so transfer functions can be reused in Objects
No longer needs callback eval instead gets pre/post separately.
Remove old methods etc
Phase2 of slicer completed
Based off Simp code but uses results already computed instead of doing a new live vars analysis.
Some statements weren't registered as having an impact if the variable was replace by an already existing one
--slice <blockName> --criterion list<variable_names> does not parse the flags into valid criterion yet
Old SC used to be applied after a statement ran, but now it will be applied for the given statement. This makes it closer to usage in literature
Converts index expressions of literals into Registers during analysis. Analyses called procedures to determine if these new index are also modified
Instead let the slicer strip away these methods. Maybe what the criterion is in is now unreachable. We can still verify it
There was a problem hiding this comment.
Good work, some comments in the code
I'd like to know how much it depends on the SSA+regions structure or if its semantically correct for any IR 'dialect'. Ideally I'd like the latter with just implicit precision gains from the earlier transforms. Obviously no need for major changes, I just want to get an idea of how strong the assumptions are.
Its good to have substantial tests including loops and everything.
Autoformater can be run ./mill scalafmt.reformat
| case i: IndirectCall => Set(i.target) | ||
| case r: Return => r.outParams.keys.toSet[Variable] ++ r.outParams.values.flatMap(_.variables) | ||
| case s: (NOP | GoTo | Unreachable) => Set() | ||
| } |
There was a problem hiding this comment.
This re-implements ir.allVarsPos() in IRCursor.scala
| case None => throw IllegalArgumentException("Slicer requires --dsa checks|standard") | ||
| case Some(Prereq) => throw IllegalArgumentException("Slicer requires --dsa checks|standard") | ||
| case _ => () | ||
| } |
There was a problem hiding this comment.
As far as I can tell, slicer doesn't directly use the results from DSA but implicitly benefits from the region separation, why is the region pass enforced here?
| try { | ||
| val targetedBlock = program.labelToBlock(slicerConfig.blockLabel) | ||
|
|
||
| val visited = mutable.Map[String, Boolean]().withDefaultValue(false) |
There was a problem hiding this comment.
This could be a set where membership means visited.
| None | ||
| } | ||
|
|
||
| } catch { |
There was a problem hiding this comment.
This try catch shouldn't need to enclose the whole function? It looks like only the first statement can throw, so its probably better to just check slicerConfig.blockLabel exists and return early. Scala return is allows if its not nested in a deeper closure/lambda.
| class Phase1 { | ||
| protected var nop: Option[NOP] = None | ||
|
|
||
| protected def insertNOP(): Unit = startingNode match { |
|
|
||
| if (conf.slicerConfig.isDefined) { | ||
| Slicer(ctx.program, conf.slicerConfig.get).run() | ||
| } |
There was a problem hiding this comment.
conf.slicerConfig.foreach(sc => Slicer(ctx.program, sc).run())
| } | ||
|
|
||
| /* Slicing criterion for a given position */ | ||
| protected def criterion(n: CFGPosition): Set[Variable] = { |
There was a problem hiding this comment.
Needs a comment what this is because I'm just guessing just the set of variables the initial criterion is transitively dependent on? Why not include memory etc?
| // Iff all out parameters impact criterion. | ||
| c.outParams.values.toSet.exists(crit.contains) | ||
| // Iff the criterion was directly modified by call. | ||
| || !crit.equals(results.getOrElse(c, Set())) |
There was a problem hiding this comment.
The phrasing of 'modifying the criterion' is unclear to me, e.g. if this is a recursive call and the criterion is a fixed point that already captures all its effects its not going to modify the criterion but will still be dependent due to the effects of the call intersecting the criterion?
| n match { | ||
| case c: DirectCall => | ||
| // Iff all out parameters impact criterion. | ||
| c.outParams.values.toSet.exists(crit.contains) |
There was a problem hiding this comment.
Comment says all but code is exists
| .flatMap( | ||
| _.statements.collect { case m: MemoryStore => transferFunctions.convertMemoryIndex(m.index) }.flatten | ||
| ) | ||
| .toSet |
There was a problem hiding this comment.
Probably don't need to fix this, but I suspect procedure frames will need to be calculated in a fixed point over the call graph?
3 participants
Adds a 2-phase program slicer into BASIL to reduce the IR based on a given criterion.
Introduces two new flags outlining where to begin slicing from and what the initial criterion variables are:
Uses 2 phases to reduce the provided program:
Adds a collection of slicer tests to ensure its expected functionality across different scenarios, ranging from:
Additionally, some basic tests were created that run a subset of the SystemTests with the slicer to ensure that the outputted Boogie file still verifies.
Additional Changes:
assume falsein the Boogie translation phase instead of generating invalid emptygoto.directCall(String, Option[String])to actually add label into the createdDirectCallstatement.BASILTestcheckVerifyto accurately return iff Boogie successfully verified instead of always returning false.