@@ -552,15 +552,17 @@ def copypropTransform(
552552 val t = util.PerformanceTimer (s " simplify ${p.name} ( ${p.blocks.size} blocks) " )
553553 // SimplifyLogger.info(s"${p.name} ExprComplexity ${ExprComplexity()(p)}")
554554 // val result = solver.solveProc(p, true).withDefaultValue(dom.bot)
555+
556+ MinCopyProp .transform(p)
557+
555558 val result = CopyProp .DSACopyProp (p, procFrames, funcEntries, constRead)
556559 val solve = t.checkPoint(" Solve CopyProp" )
557560
558561 if (result.nonEmpty) {
559562 val vis = Simplify (CopyProp .toResult(result))
560563 visit_proc(vis, p)
561-
562564 }
563- visit_proc(CopyProp .BlockyProp (), p)
565+ // visit_proc(CopyProp.BlockyProp(), p)
564566 val gvis = GuardVisitor ()
565567 visit_proc(gvis, p)
566568
@@ -1013,6 +1015,115 @@ object getProcFrame {
10131015
10141016}
10151017
1018+ object MinCopyProp {
1019+
1020+ // None -> Top
1021+ type Value = Option [Variable | Literal ]
1022+
1023+ class CopyProp () {
1024+ val st = mutable.Map [Variable , Value ]()
1025+ var giveUp = false
1026+
1027+ def find (v : Variable ): Literal | Variable = {
1028+ var search : Variable = v
1029+
1030+ boundary {
1031+ while (st.contains(search)) {
1032+ st(search) match {
1033+ case None => break(search)
1034+ case Some (c : Literal ) => break(c)
1035+ case Some (v : Variable ) =>
1036+ search = v
1037+ }
1038+ }
1039+ search
1040+ }
1041+ }
1042+
1043+ def specJoinState (lhs : Variable , rhs : Variable | Literal ): Option [(Variable , Value )] = {
1044+ rhs match {
1045+ case v : Variable if (! st.contains(lhs)) => Some (lhs -> Some (v))
1046+ case v : Literal if (! st.contains(lhs)) => Some (lhs -> Some (v))
1047+ case v : Variable if (find(lhs) != find(v)) => Some (lhs -> None )
1048+ case c : Literal if (find(lhs) != c) => Some (lhs -> None )
1049+ case _ => None
1050+ }
1051+ }
1052+
1053+ def joinState (lhs : Variable , rhs : Variable | Literal ) = {
1054+ specJoinState(lhs, rhs) match {
1055+ case Some ((l, r)) => st(l) = r
1056+ case _ => ()
1057+ }
1058+ }
1059+
1060+ def clob (v : Variable ) = {
1061+ st(v) = None
1062+ }
1063+
1064+ def transfer (s : Statement ) = s match {
1065+ case LocalAssign (l : Variable , r : Variable , _) => joinState(l, r)
1066+ case LocalAssign (l : Variable , r : Literal , _) => joinState(l, r)
1067+ case LocalAssign (l : Variable , _, _) => clob(l)
1068+ // case s: SimulAssign => s.assignments.flatMap {
1069+ // case (l: Variable, r: Variable) => specJoinState(l, r).toSeq
1070+ // case (l: Variable, r) => Seq(l -> None)
1071+ // }.foreach {
1072+ // case (l, r) => st(l) = r
1073+ // }
1074+ case a : Assign => {
1075+ // memoryload and DirectCall
1076+ a.assignees.foreach(clob)
1077+ }
1078+ case _ : MemoryStore => ()
1079+ case _ : NOP => ()
1080+ case _ : Assert => ()
1081+ case _ : Assume => ()
1082+ case i : IndirectCall => giveUp = true
1083+ }
1084+
1085+ def analyse (p : Procedure ): Map [Variable , Variable | Literal ] = {
1086+ reversePostOrder(p)
1087+ val worklist = mutable.PriorityQueue [Block ]()(Ordering .by(_.rpoOrder))
1088+ worklist.addAll(p.blocks)
1089+ while (worklist.nonEmpty && ! giveUp) {
1090+ val b = worklist.dequeue()
1091+ b.statements.foreach(transfer)
1092+ }
1093+
1094+ val res : Map [Variable , Variable | Literal ] =
1095+ if giveUp then Map ()
1096+ else
1097+ st.collect {
1098+ case (v, Some (r : Variable )) => v -> find(r)
1099+ case (v, Some (c : Literal )) => v -> c
1100+ }.toMap
1101+
1102+ res
1103+ }
1104+
1105+ }
1106+
1107+ def transform (p : Procedure ) = {
1108+ val solver = CopyProp ()
1109+ val res = solver.analyse(p)
1110+
1111+ class SubstExprs (subst : Map [Variable , Expr ]) extends CILVisitor {
1112+ override def vexpr (e : Expr ) = {
1113+ Substitute (subst.get)(e) match {
1114+ case Some (n) => ChangeTo (n)
1115+ case _ => SkipChildren ()
1116+ }
1117+ }
1118+ }
1119+ if (res.nonEmpty) {
1120+ visit_proc(SubstExprs (res), p)
1121+ }
1122+
1123+ }
1124+
1125+ }
1126+
10161127object CopyProp {
10171128
10181129 class BlockyProp () extends CILVisitor {
0 commit comments