Skip to content

Commit 64f3cc1

Browse files
committed
change --pc argument to an enum
1 parent bd7723c commit 64f3cc1

File tree

4 files changed

+14
-7
lines changed

4 files changed

+14
-7
lines changed

src/main/scala/Main.scala

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -153,8 +153,11 @@ object Main {
153153
generateRelyGuarantees: Flag,
154154
@arg(name = "simplify", doc = "Partial evaluate / simplify BASIL IR before output (implies --parameter-form)")
155155
simplify: Flag,
156-
@arg(name = "keep-pc", doc = "Keep PC assignments and assertions in loaded BASIL IR (currently GTIRB-only)")
157-
keepPC: Flag,
156+
@arg(
157+
name = "pc",
158+
doc = "EXPERIMENTAL IN DEVELOPMENT: Program counter mode. (options: none | keep | assert) (default: none)"
159+
)
160+
pcTracking: Option[String],
158161
@arg(
159162
name = "validate-simplify",
160163
doc = "Emit SMT2 check for validation of simplification expression rewrites 'rewrites.smt2'"
@@ -292,7 +295,7 @@ object Main {
292295
procedureTrimDepth = conf.procedureDepth,
293296
parameterForm = conf.parameterForm.value,
294297
trimEarly = conf.trimEarly.value,
295-
keepPC = conf.keepPC.value
298+
pcTracking = PCTrackingOption.valueOf(conf.pcTracking.getOrElse("none").capitalize)
296299
),
297300
runInterpret = conf.interpret.value,
298301
simplify = conf.simplify.value,

src/main/scala/util/BASILConfig.scala

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,10 @@ enum ProcRelyVersion {
44
case Function, IfCommandContradiction
55
}
66

7+
enum PCTrackingOption {
8+
case None, Keep, Assert
9+
}
10+
711
case class BoogieGeneratorConfig(
812
memoryFunctionType: BoogieMemoryAccessMode = BoogieMemoryAccessMode.SuccessiveStoreSelect,
913
coalesceConstantMemory: Boolean = true,
@@ -21,7 +25,7 @@ case class ILLoadingConfig(
2125
procedureTrimDepth: Int = Int.MaxValue,
2226
parameterForm: Boolean = false,
2327
trimEarly: Boolean = false,
24-
keepPC: Boolean = false
28+
pcTracking: PCTrackingOption = PCTrackingOption.None
2529
)
2630

2731
case class StaticAnalysisConfig(

src/main/scala/util/RunUtils.scala

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -136,7 +136,7 @@ object IRLoading {
136136

137137
val specification = IRLoading.loadSpecification(q.specFile, program, globals)
138138

139-
if (!q.keepPC) {
139+
if (q.pcTracking == PCTrackingOption.None) {
140140
visit_prog(transforms.RemovePCStatements(), program)
141141
Logger.info(s"[!] Removed PC-related statements")
142142
}

src/test/scala/RemovePCTest.scala

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@ import org.scalatest.funsuite.AnyFunSuite
22

33
import ir.*
44
import test_util.{BASILTest, CaptureOutput}
5-
import util.{BASILConfig, IRContext, BoogieGeneratorConfig, ILLoadingConfig, StaticAnalysisConfig}
5+
import util.{BASILConfig, IRContext, BoogieGeneratorConfig, ILLoadingConfig, StaticAnalysisConfig, PCTrackingOption}
66

77
import java.nio.file.{Path, Files}
88
import java.io.{BufferedWriter, FileWriter}
@@ -18,7 +18,7 @@ class RemovePCTest extends AnyFunSuite with CaptureOutput {
1818
relfFile = s"${BASILTest.rootDirectory}/src/test/correct/$name/$variation/$name.relf",
1919
specFile = None,
2020
dumpIL = None,
21-
keepPC = keepPC
21+
pcTracking = if keepPC then PCTrackingOption.Assert else PCTrackingOption.None
2222
),
2323
staticAnalysis = Some(StaticAnalysisConfig(None)),
2424
boogieTranslation = BoogieGeneratorConfig(),

0 commit comments

Comments
 (0)