UQ-PAC / BASIL

Apache License 2.0
8 stars 0 forks source link

No MemoryModelMap entry for 'main' for 'complex' example #96

Open l-kent opened 1 year ago

l-kent commented 1 year ago

When the example 'complex' is run with the analysis enabled, an exception is thrown at the start of the VSA, caused by there not being an entry for 'main' in allStacks in the MemoryModelMap. This happens in the pushContext method in the MemoryModelMap. as it is called with the parameter 'main' early in the VSA.

When allStacks is populated by convertMemoryRegions before the VSA is run, it does not end up creating an entry for 'main' in this instance, as exitNodes does not contain a CfgFunctionExitNode for the main procedure here. I have not investigated enough to determine why this is the case.

This is the stack trace:

[error] java.util.NoSuchElementException: key not found: main
[error]         at scala.collection.MapOps.default(Map.scala:274)
[error]         at scala.collection.MapOps.default$(Map.scala:273)
[error]         at scala.collection.AbstractMap.default(Map.scala:405)
[error]         at scala.collection.mutable.HashMap.apply(HashMap.scala:425)
[error]         at analysis.MemoryModelMap.pushContext(MemoryModelMap.scala:72)
[error]         at analysis.MemoryRegionValueSetAnalysis.localTransfer(VSA.scala:160)
[error]         at analysis.MemoryRegionValueSetAnalysis.localTransfer$(VSA.scala:30)
[error]         at analysis.ValueSetAnalysis.localTransfer(VSA.scala:172)
[error]         at analysis.ValueSetAnalysis.transfer(VSA.scala:185)
[error]         at analysis.IntraprocValueSetAnalysisWorklistSolver.transfer(VSA.scala:189)
[error]         at analysis.solvers.MapLatticeSolver.funsub(FixPointSolver.scala:44)
[error]         at analysis.solvers.MapLatticeSolver.funsub$(FixPointSolver.scala:22)
[error]         at analysis.IntraprocValueSetAnalysisWorklistSolver.funsub(VSA.scala:189)
[error]         at analysis.solvers.SimpleMonotonicSolver.process(MonotonicSolver.scala:29)
[error]         at analysis.solvers.SimpleMonotonicSolver.process$(MonotonicSolver.scala:16)
[error]         at analysis.IntraprocValueSetAnalysisWorklistSolver.process(VSA.scala:189)
[error]         at analysis.solvers.ListSetWorklist.run(FixPointSolver.scala:97)
[error]         at analysis.solvers.ListSetWorklist.run$(FixPointSolver.scala:83)
[error]         at analysis.IntraprocValueSetAnalysisWorklistSolver.run(VSA.scala:189)
[error]         at analysis.solvers.SimpleMonotonicSolver.analyze(MonotonicSolver.scala:46)
[error]         at analysis.solvers.SimpleMonotonicSolver.analyze$(MonotonicSolver.scala:16)
[error]         at analysis.IntraprocValueSetAnalysisWorklistSolver.analyze(VSA.scala:189)
[error]         at util.RunUtils$.analyse(RunUtils.scala:165)
[error]         at util.RunUtils$.loadAndTranslate(RunUtils.scala:96)
[error]         at Main$.main(Main.scala:66)
[error]         at Main.main(Main.scala
l-kent commented 1 year ago

This bug seems to be because the example 'complex' has a loop in it.

yousifpatti commented 7 months ago

Resolved with irreducible loops?