Skip to content

Commit

Permalink
feat(analyzer.stateaccess): First working version of the analyzer
Browse files Browse the repository at this point in the history
  • Loading branch information
Leosimetti committed Apr 3, 2022
1 parent 3dde434 commit 665183a
Show file tree
Hide file tree
Showing 3 changed files with 165 additions and 0 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@ import org.polystat.odin.analysis.inlining.Inliner
import org.polystat.odin.analysis.logicalexprs.ExtractLogic
import org.polystat.odin.analysis.mutualrec.advanced.Analyzer.analyzeAst
import org.polystat.odin.analysis.mutualrec.naive.findMutualRecursionFromAst
import org.polystat.odin.analysis.stateaccess.DetectAccess
import org.polystat.odin.core.ast.EOProg
import org.polystat.odin.core.ast.astparams.EOExprOnly
import org.polystat.odin.parser.EoParser
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,93 @@
package org.polystat.odin.analysis.stateaccess

import cats.data.EitherNel
import org.polystat.odin.analysis.inlining.{Abstract, BndItself, Inliner, MethodInfo, ObjectInfo, ParentInfo}
import org.polystat.odin.core.ast.{EOAnyNameBnd, EOBndExpr, EOCopy, EODot, EONamedBnd, EOSimpleAppWithLocator, LazyName}
import org.polystat.odin.parser.eo.Parser

object DetectAccess {

type ObjInfo = ObjectInfo[ParentInfo[MethodInfo, ObjectInfo], MethodInfo]
case class State(container: EONamedBnd, states: Vector[EONamedBnd])
case class StateChange(method: EONamedBnd, state: EONamedBnd)

def accumulateParentState(tree: Map[EONamedBnd, Inliner.CompleteObjectTree])(
currentParentLink: Option[ParentInfo[MethodInfo, ObjectInfo]],
existingState: Vector[EONamedBnd] = Vector()
): List[State] = {
currentParentLink match {
case Some(parentLink) =>
val parentObj = parentLink.linkToParent.getOption(tree).get
val currentStates = parentObj
.info
.bnds
.collect {
case BndItself(EOBndExpr(bndName, EOSimpleAppWithLocator("memory", _)))
if !existingState.contains(bndName) =>
bndName
}

List(State(container = parentObj.info.name, states = currentStates)) ++
accumulateParentState(tree)(parentObj.info.parentInfo, existingState ++ currentStates)

case None => List()
}
}

def getAlteredState(method: (EONamedBnd, MethodInfo)): List[StateChange] = {
val binds = method._2.body.bndAttrs

Abstract.foldAst[List[StateChange]](binds) {
case EOCopy(EODot(EODot(EOSimpleAppWithLocator("self", x), state), "write"), _) if x == 0 =>
List(StateChange(method._1, EOAnyNameBnd(LazyName(state))))
}
}

def analyze[F[_]](
tree: Map[EONamedBnd, Inliner.CompleteObjectTree]
): EitherNel[String, List[String]] = {
Right(
tree
// Has a parent
.filter(_._2.info.parentInfo.nonEmpty)
.flatMap(obj => {
val availableParentStates =
accumulateParentState(tree)(obj._2.info.parentInfo)
val alteredStates = obj._2.info.methods.flatMap(getAlteredState)

for {
change <- alteredStates
State(container, states) <- availableParentStates
} yield
if (states.contains(change.state))
List(
f"Method '${change.method.name.name}' of object '${obj._1.name.name}' directly accesses state '${change.state.name.name}' of base class '${container.name.name}'"
)
else List()
})
.flatten
.toList
)
}

def main(args: Array[String]): Unit = {
val code = """[] > a
| memory > state
| [self new_state] > update_state
| self.state.write new_state > @
|[] > b
| a > @
| [self new_state] > change_state_plus_two
| self.state.write (new_state.add 2) > @
|""".stripMargin

println(
Parser
.parse(code)
.flatMap(Inliner.createObjectTree)
.flatMap(Inliner.resolveParents)
.flatMap(analyze)
)
}

}
Original file line number Diff line number Diff line change
@@ -0,0 +1,71 @@
package org.polystat.odin.analysis

import cats.effect._
import org.scalatest.wordspec.AnyWordSpec
import org.polystat.odin.parser.EoParser.sourceCodeEoParser
import cats.effect.unsafe.implicits.global
import org.polystat.odin.analysis.EOOdinAnalyzer.accessToBaseClassAnalyzer

class DetectAccessTests extends AnyWordSpec {
case class TestCase(label: String, code: String, expected: List[String])

def analyze(code: String): IO[List[String]] =
EOOdinAnalyzer
.analyzeSourceCode[String, IO](accessToBaseClassAnalyzer[IO])(code)(sourceCodeEoParser())
.compile
.toList
.map(_.map(_.value))

val testsWithDefect = List(
TestCase(
label = "Improper access to state",
code = """[] > a
| memory > state
| [self new_state] > update_state
| self.state.write new_state > @
|[] > b
| a > @
| [self new_state] > change_state_plus_two
| self.state.write (new_state.add 2) > @
|""".stripMargin,
expected = List("Method 'change_state_plus_two' of object 'b' directly accesses state 'state' of base class 'a'")
)
)

val testsWithoutDefect = List(
TestCase(
label = "Proper access to state",
code = """[] > a
| memory > state
| [self new_state] > update_state
| self.state.write new_state > @
|[] > b
| a > @
| [self new_state] > change_state_plus_two
| new_state.add 2 > tmp
| self.update_state self tmp > @
|""".stripMargin,
expected = List()
)
)

def runTests(tests: List[TestCase]) : Unit =
tests.foreach {
case TestCase(label, code, expected) =>
registerTest(label) {
val obtained = analyze(code).unsafeRunSync()
assert(obtained == expected)
}
}

"analyzer" should {
"find errors" should {
runTests(testsWithDefect)
}

"not find errors" should {
runTests(testsWithoutDefect)
}

}
}

0 comments on commit 665183a

Please sign in to comment.