Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Simplification pass #256

Open
wants to merge 142 commits into
base: main
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
142 commits
Select commit Hold shift + click to select a range
182c9e8
refactor call to a statement & add unreachable and return jumps
ailrst Aug 19, 2024
3711e4d
move transforms out of RunUtils.scala
ailrst Aug 19, 2024
fd56c9a
remove old cfg
ailrst Aug 9, 2024
bd6b2ad
update docs
ailrst Aug 19, 2024
96b9028
pe based expr evaluator
ailrst Aug 19, 2024
d264b97
interpreter test
ailrst Aug 19, 2024
a3bf83b
rewrite interpreter in functional style
ailrst Aug 22, 2024
74c4bc2
cleanup call/return
ailrst Aug 22, 2024
9e23558
cleanup memory ops to enter effects
ailrst Aug 22, 2024
7571aa3
tracing interpreter
ailrst Aug 26, 2024
f36c13e
compile with state monad
ailrst Aug 27, 2024
2c16c83
fix state monad interp
ailrst Aug 28, 2024
dd11175
indirect calls
ailrst Aug 28, 2024
c7b4a56
tracing interpreter
ailrst Aug 28, 2024
f64f904
breakpoints
ailrst Aug 28, 2024
897c565
improve breakpoints
ailrst Aug 29, 2024
cc97052
reorg
ailrst Aug 29, 2024
695b2d2
refactor with statemonad[s, either[v]]
ailrst Aug 29, 2024
00b482a
redo error handling
ailrst Aug 29, 2024
1a139d2
refactor call to a statement & add unreachable and return jumps
ailrst Aug 19, 2024
7e94536
move transforms out of RunUtils.scala
ailrst Aug 19, 2024
aae0064
remove old cfg
ailrst Aug 9, 2024
e2c0cd4
update docs
ailrst Aug 19, 2024
a3adee3
fix
ailrst Aug 30, 2024
4a92c99
fix externals
ailrst Aug 30, 2024
b994c99
disable IDE analyses if mainproc is external
ailrst Aug 30, 2024
b83c9ff
Merge branch 'call-statement' into interpreter
ailrst Aug 30, 2024
d6c5767
work on differential testing
ailrst Aug 30, 2024
2a03a23
hook for dynlinking
ailrst Sep 2, 2024
8b694c0
load full symtab
ailrst Sep 2, 2024
57ca6b3
update relf grammar
ailrst Sep 3, 2024
b276981
init bss
ailrst Sep 3, 2024
888d360
cleanup
ailrst Sep 3, 2024
0abf654
cleanup init trace
ailrst Sep 3, 2024
9192ce3
intrinsic stub and cleanup errors
ailrst Sep 3, 2024
5342358
init relocation table
ailrst Sep 3, 2024
87b0f86
pull stepper outside effects to fix interpreter composition again
ailrst Sep 4, 2024
f5a0590
cleanup
ailrst Sep 4, 2024
a6b58e8
cleanup
ailrst Sep 4, 2024
dd64c14
constprop test with interpreter
ailrst Sep 4, 2024
8be5cb6
interpreter docs
ailrst Sep 4, 2024
d2a2486
fix list
ailrst Sep 4, 2024
d06e268
paragraph
ailrst Sep 4, 2024
4ae3997
trap eval exceptions to monadic errors
ailrst Sep 4, 2024
4fc8ed2
improve interpretOne
ailrst Sep 4, 2024
8f966ce
notes on initialisation
ailrst Sep 4, 2024
f00b44b
simplify invoc funcs
ailrst Sep 4, 2024
ceef233
note missing features
ailrst Sep 5, 2024
cff6c97
run through all system tests
ailrst Sep 5, 2024
822c127
add resource limit
ailrst Sep 5, 2024
9b8f715
doc resource limit
ailrst Sep 5, 2024
648a41d
tweak doc
ailrst Sep 5, 2024
dfa7209
fix
ailrst Sep 5, 2024
38f871c
tweak interpretrlimit
ailrst Sep 5, 2024
6559180
basic malloc implementation
ailrst Sep 9, 2024
c6e938d
implement printf
ailrst Sep 10, 2024
285099b
cleanup intrins
ailrst Sep 10, 2024
aac7f5c
cleanup
ailrst Sep 23, 2024
1c2a5d5
Merge remote-tracking branch 'upstream/main' into interpreter
ailrst Sep 23, 2024
46ff66a
cleanup
ailrst Sep 23, 2024
f45015b
initial attempt at IR simplification
ailrst Sep 25, 2024
7769357
fixup analysis
ailrst Sep 25, 2024
533ccce
wl optim
ailrst Sep 25, 2024
febadbd
rename w ssa
ailrst Sep 25, 2024
4465cfb
tweak ssa
ailrst Sep 20, 2024
a6cc33f
change param to localvar
ailrst Sep 30, 2024
750d949
distinguish lvars and rvars in cilvisitor
ailrst Sep 30, 2024
c9c4181
transform ir and spec and loader to have params
ailrst Oct 1, 2024
f83fd74
cleanup spec param handling
ailrst Oct 2, 2024
3fce1c9
update visitor
ailrst Oct 2, 2024
eef39b9
add invariant check
ailrst Oct 2, 2024
9b87104
Merge branch 'procedure-call-abstraction' into xf
ailrst Oct 2, 2024
a21015c
fix test issues in merge
ailrst Oct 2, 2024
409c455
make simplify work with params
ailrst Oct 2, 2024
81fd5e4
improve dsa and params w liveness
ailrst Oct 4, 2024
8e99918
fix dsa, copyprop, cleanup
ailrst Oct 8, 2024
495e4f2
small fix
ailrst Oct 10, 2024
e567f77
rewrites
ailrst Oct 15, 2024
5c42e92
remove slices
ailrst Oct 16, 2024
41aa3d7
disable bad
ailrst Oct 16, 2024
24a12e3
attempt at condition lifting
ailrst Oct 17, 2024
8bf3e4d
cleanup
ailrst Oct 17, 2024
f75086e
add example
ailrst Oct 17, 2024
c26028e
add expr2smt
ailrst Oct 18, 2024
09eb1af
validate and improve expr lifting
ailrst Oct 18, 2024
8b4fd6f
transform order
ailrst Oct 18, 2024
bc48e00
cleanup and perf
ailrst Oct 19, 2024
f2adf72
add early proc trim and fix remove unreachable cfg maintenance
ailrst Oct 22, 2024
a6d302f
flow insensitive copyprop and single pass dsa
ailrst Oct 23, 2024
f313ed3
block coalescing
ailrst Oct 31, 2024
95744f7
booltobv1 and copyprop heuristic
ailrst Nov 1, 2024
70a22c1
WIP bitvector size type inference
ailrst Nov 1, 2024
760bc0a
copyprop completeness improvements
ailrst Nov 5, 2024
2b2a0a5
improvements to cond identification
ailrst Nov 6, 2024
6ea3b1a
improve shift/extend/extract removal
ailrst Nov 7, 2024
3beb84d
improve cond detection
ailrst Nov 7, 2024
7c0c98b
revert to old slice removal
ailrst Nov 7, 2024
a7d0754
cleanup
ailrst Nov 7, 2024
80491cb
validate and improve condition reduction
ailrst Nov 8, 2024
983597c
new prettyprinter
ailrst Nov 11, 2024
08af7a3
docs and cleanup
ailrst Nov 12, 2024
d3b8176
ccmp and rpo sort
ailrst Nov 13, 2024
0f9a756
Merge branch 'main' of github.com:UQ-PAC/bil-to-boogie-translator int…
ailrst Nov 13, 2024
a452165
work on adding param support to interpreter
ailrst Nov 29, 2024
b9c549c
multiple loggers
ailrst Dec 2, 2024
8dd5f0e
fix externalremover
ailrst Dec 3, 2024
21efc16
robustness and perf fixes (monad overflow)
ailrst Dec 3, 2024
797dc2b
Merge branch 'main' into simp-pass-main-merge
b-paul Dec 10, 2024
a824c07
prettyprinter
ailrst Dec 5, 2024
015edd3
Merge branch 'ilparser-serialiser' of github.com:ailrst/basil into si…
ailrst Dec 10, 2024
38f927b
run simplify after analysis
ailrst Dec 10, 2024
8329c11
Merge pull request #285 from UQ-PAC/simp-pass-main-merge
ailrst Dec 10, 2024
a082b35
dont try to <8bit initial memory regions
ailrst Dec 19, 2024
589df48
fix test load/store flag
ailrst Jan 6, 2025
cbc3cac
fix fmt
ailrst Jan 6, 2025
79b8d85
Merge remote-tracking branch 'origin' into simplification-pass
ailrst Jan 6, 2025
3a441cc
remove bvsaddo as not supported by z3 smtlib
ailrst Jan 6, 2025
92a10df
cleanup and autoformat new files
ailrst Jan 6, 2025
e71c1fc
add back initialMemory
ailrst Jan 6, 2025
d5a744b
tweak prettyprinter
ailrst Jan 6, 2025
ef7330a
fix args
ailrst Jan 6, 2025
fa73de2
fix
ailrst Jan 14, 2025
827946c
basic exit call identification
ailrst Jan 14, 2025
d72b987
allow custom initial state in AbstractDomain
sadrabt Jan 15, 2025
f272284
Merge pull request #298 from UQ-PAC/simplification-pass-init
ailrst Jan 15, 2025
589a9ee
load dir update readme
ailrst Jan 15, 2025
f6e1a16
tweak messages and readme
ailrst Jan 16, 2025
c8a208e
disable spec param conversion on procedures with no spec
ailrst Jan 16, 2025
fb808f6
add interproc solver to absint, analysis result printer
ailrst Jan 21, 2025
059807c
fixes
ailrst Jan 22, 2025
8e2c420
Merge pull request #301 from UQ-PAC/simplify-interproc-fixedpoint
ailrst Jan 22, 2025
7544b65
Simplify fixes (#302)
ailrst Jan 23, 2025
95f7b8a
disable debug print
ailrst Jan 23, 2025
8584daa
fix interlivevars return function
ailrst Jan 23, 2025
2e80fcc
wip copyprop throuh memory
ailrst Jan 23, 2025
d51dc93
minor simplifyexpr improvement
ailrst Jan 24, 2025
276af66
disable load prop
ailrst Jan 24, 2025
647e884
Merge pull request #303 from UQ-PAC/memory-copyprop
ailrst Jan 24, 2025
6bd9aea
add R31 to overapprox param set
ailrst Jan 29, 2025
b17ca3d
Merge remote-tracking branch 'origin' into simplification-pass
ailrst Jan 29, 2025
17c0210
add simplify to action
ailrst Jan 29, 2025
f53c05a
disable r30 assertion when simp disabled
ailrst Jan 29, 2025
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
move transforms out of RunUtils.scala
  • Loading branch information
ailrst committed Aug 29, 2024
commit 7e9453693a339a9a928a61b1349a27feecdf741f
4 changes: 2 additions & 2 deletions src/main/scala/analysis/Cfg.scala
Original file line number Diff line number Diff line change
Expand Up @@ -502,7 +502,7 @@ class ProgramCfgFactory:
val targetProc: Procedure = dCall.target
funcEntryNode.callers.add(procToCfg(targetProc)._1)

val callNode = CfgJumpNode(dCall, block, funcEntryNode)
val callNode : CfgJumpNode = s.asInstanceOf[CfgJumpNode]

// Branch to this call
cfg.addEdge(precNode, callNode)
Expand All @@ -523,7 +523,7 @@ class ProgramCfgFactory:
Logger.debug(s"Indirect call found: $iCall in ${proc.name}")
var precNode = prevNode

val jmpNode = CfgJumpNode(iCall, block, funcEntryNode)
val jmpNode = s.asInstanceOf[CfgJumpNode]
// Branch to this call
cfg.addEdge(precNode, jmpNode)

Expand Down
6 changes: 3 additions & 3 deletions src/main/scala/analysis/IDEAnalysis.scala
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
package analysis

import ir.{CFGPosition, Command, DirectCall, GoTo, IndirectCall, Procedure, Program}
import ir.{CFGPosition, Command, DirectCall, GoTo, Return, IndirectCall, Procedure, Program}

final case class Lambda()

Expand Down Expand Up @@ -55,6 +55,6 @@ trait IDEAnalysis[E, EE, C, R, D, T, L <: Lattice[T]] {
}

// IndirectCall in these is because they are returns so that can be further tightened in future
trait ForwardIDEAnalysis[D, T, L <: Lattice[T]] extends IDEAnalysis[Procedure, IndirectCall, DirectCall, Command, D, T, L]
trait ForwardIDEAnalysis[D, T, L <: Lattice[T]] extends IDEAnalysis[Procedure, Return, DirectCall, Command, D, T, L]

trait BackwardIDEAnalysis[D, T, L <: Lattice[T]] extends IDEAnalysis[IndirectCall, Procedure, Command, DirectCall, D, T, L]
trait BackwardIDEAnalysis[D, T, L <: Lattice[T]] extends IDEAnalysis[Return, Procedure, Command, DirectCall, D, T, L]
10 changes: 7 additions & 3 deletions src/main/scala/analysis/InterLiveVarsAnalysis.scala
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
package analysis

import analysis.solvers.BackwardIDESolver
import ir.{Assert, Assume, GoTo, CFGPosition, Command, DirectCall, IndirectCall, Assign, MemoryAssign, Procedure, Program, Variable, toShortString}
import ir.{Assert, Assume, Block, GoTo, CFGPosition, Command, DirectCall, IndirectCall, Assign, MemoryAssign, Halt, Return, Procedure, Program, Variable, toShortString}

/**
* Micro-transfer-functions for LiveVar analysis
Expand All @@ -19,7 +19,7 @@ trait LiveVarsAnalysisFunctions extends BackwardIDEAnalysis[Variable, TwoElement
val edgelattice: EdgeFunctionLattice[TwoElement, TwoElementLattice] = EdgeFunctionLattice(valuelattice)
import edgelattice.{IdEdge, ConstEdge}

def edgesCallToEntry(call: Command, entry: IndirectCall)(d: DL): Map[DL, EdgeFunction[TwoElement]] = {
def edgesCallToEntry(call: Command, entry: Return)(d: DL): Map[DL, EdgeFunction[TwoElement]] = {
Map(d -> IdEdge())
}

Expand Down Expand Up @@ -74,7 +74,11 @@ trait LiveVarsAnalysisFunctions extends BackwardIDEAnalysis[Variable, TwoElement
d match
case Left(value) => if value != variable then Map(d -> IdEdge()) else Map()
case Right(_) => Map(d -> IdEdge(), Left(variable) -> ConstEdge(TwoElementTop))
case _ => Map(d -> IdEdge())
case r: Return => Map(d -> IdEdge())
case h: Halt => Map(d -> IdEdge())
case c: DirectCall => Map(d -> IdEdge())
case c: Block => Map(d -> IdEdge())
case c: GoTo => Map(d -> IdEdge())

}
}
Expand Down
4 changes: 3 additions & 1 deletion src/main/scala/analysis/IntraLiveVarsAnalysis.scala
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
package analysis

import analysis.solvers.SimpleWorklistFixpointSolver
import ir.{Assert, Assume, Block, CFGPosition, Call, DirectCall, GoTo, IndirectCall, Jump, Assign, MemoryAssign, NOP, Procedure, Program, Statement, Variable}
import ir.{Assert, Assume, Block, CFGPosition, Call, DirectCall, GoTo, IndirectCall, Jump, Assign, MemoryAssign, NOP, Procedure, Program, Statement, Variable, Return, Halt}

abstract class LivenessAnalysis(program: Program) extends Analysis[Any]:
val lattice: MapLattice[CFGPosition, Set[Variable], PowersetLattice[Variable]] = MapLattice(PowersetLattice())
Expand All @@ -18,6 +18,8 @@ abstract class LivenessAnalysis(program: Program) extends Analysis[Any]:
case IndirectCall(variable, _) => s + variable
case c: DirectCall => s
case g: GoTo => s
case r: Return => s
case r: Halt => s
case _ => ???
}
}
Expand Down
2 changes: 1 addition & 1 deletion src/main/scala/analysis/VSA.scala
Original file line number Diff line number Diff line change
Expand Up @@ -172,7 +172,7 @@ trait ValueSetAnalysis(program: Program,
if (IRWalk.procedure(n) == n) {
mmm.pushContext(n.asInstanceOf[Procedure].name)
s
} else if (IRWalk.procedure(n).end == n) {
} else if (IRWalk.lastInProc(IRWalk.procedure(n)) == n) {
mmm.popContext()
s
} else n match
Expand Down
40 changes: 24 additions & 16 deletions src/main/scala/analysis/solvers/IDESolver.scala
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
package analysis.solvers

import analysis.{BackwardIDEAnalysis, Dependencies, EdgeFunction, EdgeFunctionLattice, ForwardIDEAnalysis, IDEAnalysis, IRInterproceduralBackwardDependencies, IRInterproceduralForwardDependencies, Lambda, Lattice, MapLattice}
import ir.{CFGPosition, Command, DirectCall, GoTo, IRWalk, IndirectCall, InterProcIRCursor, Procedure, Program, end, isAfterCall, Halt, Statement, Jump}
import ir.{CFGPosition, Command, DirectCall, GoTo, IRWalk, IndirectCall, Return, InterProcIRCursor, Procedure, Program, isAfterCall, Halt, Statement, Jump}
import util.Logger

import scala.collection.immutable.Map
Expand Down Expand Up @@ -208,10 +208,10 @@ abstract class IDESolver[E <: Procedure | Command, EE <: Procedure | Command, C


abstract class ForwardIDESolver[D, T, L <: Lattice[T]](program: Program)
extends IDESolver[Procedure, IndirectCall, DirectCall, Command, D, T, L](program, program.mainProcedure),
extends IDESolver[Procedure, Return, DirectCall, Command, D, T, L](program, program.mainProcedure),
ForwardIDEAnalysis[D, T, L], IRInterproceduralForwardDependencies {

protected def entryToExit(entry: Procedure): IndirectCall = entry.end.asInstanceOf[IndirectCall]
protected def entryToExit(entry: Procedure): Return = IRWalk.lastInProc(entry).asInstanceOf[Return]

protected def exitToEntry(exit: IndirectCall): Procedure = IRWalk.procedure(exit)

Expand All @@ -222,7 +222,10 @@ abstract class ForwardIDESolver[D, T, L <: Lattice[T]](program: Program)
case r: Jump => ret.parent.statements.last.asInstanceOf[DirectCall]
}

protected def getCallee(call: DirectCall): Procedure = call.target
protected def getCallee(call: DirectCall): Procedure = {
require(isCall(call))
call.target
}

protected def isCall(call: CFGPosition): Boolean =
call match
Expand All @@ -232,41 +235,46 @@ abstract class ForwardIDESolver[D, T, L <: Lattice[T]](program: Program)
protected def isExit(exit: CFGPosition): Boolean =
exit match
// only looking at functions with statements
case command: Command => IRWalk.procedure(command).end == command
case command: Command => IRWalk.lastInProc(IRWalk.procedure(command)) == command
case _ => false

protected def getAfterCalls(exit: IndirectCall): Set[Command] =
InterProcIRCursor.succ(exit).filter(_.isInstanceOf[Command]).map(_.asInstanceOf[Command])

}


abstract class BackwardIDESolver[D, T, L <: Lattice[T]](program: Program)
extends IDESolver[IndirectCall, Procedure, Command, DirectCall, D, T, L](program, program.mainProcedure.end),
extends IDESolver[Return, Procedure, Command, DirectCall, D, T, L](program, IRWalk.lastInProc(program.mainProcedure)),
BackwardIDEAnalysis[D, T, L], IRInterproceduralBackwardDependencies {

protected def entryToExit(entry: IndirectCall): Procedure = IRWalk.procedure(entry)
protected def entryToExit(entry: Return): Procedure = IRWalk.procedure(entry)

protected def exitToEntry(exit: Procedure): IndirectCall = exit.end.asInstanceOf[IndirectCall]
protected def exitToEntry(exit: Procedure): Return = exit.returnBlock.get.jump.asInstanceOf[Return]

protected def callToReturn(call: Command): DirectCall = call match {
case ret: Statement => ret.parent.statements.getPrev(ret).asInstanceOf[DirectCall]
case r: Jump => r.parent.statements.last.asInstanceOf[DirectCall]
protected def callToReturn(call: Command): DirectCall = {
IRWalk.prevCommandInBlock(call) match {
case Some(x : DirectCall) => x
case p => throw Exception(s"Not a return/aftercall node $call .... prev = $p")
}
}

protected def returnToCall(ret: DirectCall): Command = ret.successor

protected def getCallee(call: Command): IndirectCall = callToReturn(call: Command).target.end.asInstanceOf[IndirectCall]
protected def getCallee(call: Command): Return = {
require(isCall(call))
val procCalled = callToReturn(call).target
procCalled.returnBlock.getOrElse(throw Exception(s"No return node for procedure ${procCalled}")).jump.asInstanceOf[Return]
}

protected def isCall(call: CFGPosition): Boolean =
call match
case directCall: DirectCall => (!directCall.successor.isInstanceOf[Halt])
case c : Command => isAfterCall(c) && IRWalk.prevCommandInBlock(c).map(_.isInstanceOf[DirectCall]).getOrElse(false)
case _ => false

protected def isExit(exit: CFGPosition): Boolean =
exit match
case procedure: Procedure => procedure.blocks.nonEmpty
case procedure: Procedure => true
case _ => false

protected def getAfterCalls(exit: Procedure): Set[DirectCall] = InterProcIRCursor.pred(exit).filter(_.isInstanceOf[DirectCall]).map(_.asInstanceOf[DirectCall])
protected def getAfterCalls(exit: Procedure): Set[DirectCall] = exit.incomingCalls().toSet
}
Loading