Skip to content

Commit

Permalink
Rewriting system.
Browse files Browse the repository at this point in the history
  • Loading branch information
@robby-phd
robby-phd committed Feb 12, 2024
1 parent 885ec1c commit b507d03
Show file tree
Hide file tree
Showing 7 changed files with 61 additions and 17 deletions.
4 changes: 3 additions & 1 deletion jvm/src/test/scala/org/sireum/logika/LogikaTest.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -96,7 +96,9 @@ object LogikaTest {
isAuto = T,
background = Config.BackgroundMode.Type,
atRewrite = T,
searchPc = T
searchPc = T,
rwTrace = T,
rwMax = 100
)

lazy val isInGithubAction: B = Os.env("GITHUB_ACTION").nonEmpty
Expand Down
4 changes: 3 additions & 1 deletion shared/src/main/scala/org/sireum/logika/Config.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -67,7 +67,9 @@ import org.sireum._
val isAuto: B,
val background: Config.BackgroundMode.Type,
val atRewrite: B,
val searchPc: B) {
val searchPc: B,
val rwTrace: B,
val rwMax: Z) {

@memoize def fingerprint: U64 = {
return ops.StringOps(string).sha3U64(T, T)
Expand Down
5 changes: 4 additions & 1 deletion shared/src/main/scala/org/sireum/logika/RewritingSystem.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -134,6 +134,7 @@ object RewritingSystem {
@record class Rewriter(val th: TypeHierarchy,
val provenClaims: HashSSet[AST.CoreExp.Base],
val rwPatterns: ISZ[Rewriter.Pattern],
val shouldTrace: B,
var trace: ISZ[TraceElement]) extends AST.MCoreExpTransformer {
override def preCoreExpIf(o: AST.CoreExp.If): AST.MCoreExpTransformer.PreResult[AST.CoreExp.Base] = {
o.cond match {
Expand Down Expand Up @@ -172,7 +173,9 @@ object RewritingSystem {
} else if (pattern.isPermutative && o < o3) {
// skip
} else {
trace = trace :+ TraceElement(pattern.name, pattern.rightToLeft, pattern.exp, o, o2, o3Opt, o3)
if (shouldTrace) {
trace = trace :+ TraceElement(pattern.name, pattern.rightToLeft, pattern.exp, o, o2, o3Opt, o3)
}
rOpt = MSome(o3)
}
}
Expand Down
8 changes: 8 additions & 0 deletions shared/src/main/scala/org/sireum/logika/cli.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -160,6 +160,14 @@ object cli {
tpe = Type.Flag(F),
description = "Split on match expressions and statements")
)),
OptGroup(name = "Rewriting", opts = ISZ(
Opt(name = "rwTrace", longKey = "rw-trace", shortKey = None(),
tpe = Type.Flag(T),
description = "Disable rewriting trace"),
Opt(name = "rwMax", longKey = "rw-max", shortKey = None(),
tpe = Type.Num(None(), 100, Some(1), None()),
description = "Maximum number of rewriting")
)),
OptGroup(name = "SMT2", opts = ISZ(
Opt(name = "elideEncoding", longKey = "elide-encoding", shortKey = None(),
tpe = Type.Flag(F),
Expand Down
23 changes: 22 additions & 1 deletion shared/src/main/scala/org/sireum/logika/options/OptionsCli.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -103,6 +103,8 @@ object OptionsCli {
val splitContract: B,
val splitIf: B,
val splitMatch: B,
val rwTrace: B,
val rwMax: Z,
val elideEncoding: B,
val rawInscription: B,
val rlimit: Z,
Expand Down Expand Up @@ -290,6 +292,11 @@ import OptionsCli._
| --split-if Split on if-conditional expressions and statements
| --split-match Split on match expressions and statements
|
|Rewriting Options:
| --rw-trace Disable rewriting trace
| --rw-max Maximum number of rewriting (expects an integer; min
| is 1; default is 100)
|
|SMT2 Options:
| --elide-encoding Strip out SMT2 encoding in feedback
| --raw-inscription Use raw sequent/sat preamble inscription
Expand Down Expand Up @@ -345,6 +352,8 @@ import OptionsCli._
var splitContract: B = false
var splitIf: B = false
var splitMatch: B = false
var rwTrace: B = true
var rwMax: Z = 100
var elideEncoding: B = false
var rawInscription: B = false
var rlimit: Z = 2000000
Expand Down Expand Up @@ -585,6 +594,18 @@ import OptionsCli._
case Some(v) => splitMatch = v
case _ => return None()
}
} else if (arg == "--rw-trace") {
val o: Option[B] = { j = j - 1; Some(!rwTrace) }
o match {
case Some(v) => rwTrace = v
case _ => return None()
}
} else if (arg == "--rw-max") {
val o: Option[Z] = parseNum(args, j + 1, Some(1), None())
o match {
case Some(v) => rwMax = v
case _ => return None()
}
} else if (arg == "--elide-encoding") {
val o: Option[B] = { j = j - 1; Some(!elideEncoding) }
o match {
Expand Down Expand Up @@ -654,7 +675,7 @@ import OptionsCli._
isOption = F
}
}
return Some(LogikaOption(help, parseArguments(args, j), background, manual, smt2Caching, transitionCaching, infoFlow, charBitWidth, fpRounding, useReal, intBitWidth, interprocedural, interproceduralContracts, strictPureMode, line, loopBound, callBound, patternExhaustive, pureFun, sat, skipMethods, skipTypes, logPc, logPcLines, logRawPc, logVc, logVcDir, logDetailedInfo, logAtRewrite, stats, par, branchParMode, branchPar, dontSplitFunQuant, splitAll, splitContract, splitIf, splitMatch, elideEncoding, rawInscription, rlimit, sequential, simplify, smt2SatConfigs, smt2ValidConfigs, satTimeout, timeout, searchPC))
return Some(LogikaOption(help, parseArguments(args, j), background, manual, smt2Caching, transitionCaching, infoFlow, charBitWidth, fpRounding, useReal, intBitWidth, interprocedural, interproceduralContracts, strictPureMode, line, loopBound, callBound, patternExhaustive, pureFun, sat, skipMethods, skipTypes, logPc, logPcLines, logRawPc, logVc, logVcDir, logDetailedInfo, logAtRewrite, stats, par, branchParMode, branchPar, dontSplitFunQuant, splitAll, splitContract, splitIf, splitMatch, rwTrace, rwMax, elideEncoding, rawInscription, rlimit, sequential, simplify, smt2SatConfigs, smt2ValidConfigs, satTimeout, timeout, searchPC))
}

def parseArguments(args: ISZ[String], i: Z): ISZ[String] = {
Expand Down
10 changes: 9 additions & 1 deletion shared/src/main/scala/org/sireum/logika/options/OptionsUtil.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -173,7 +173,9 @@ object OptionsUtil {
isAuto = !o.manual,
background = background,
atRewrite = o.logAtRewrite,
searchPc = o.searchPC
searchPc = o.searchPC,
rwTrace = o.rwTrace,
rwMax = o.rwMax
)
return Either.Left(config)
}
Expand Down Expand Up @@ -331,6 +333,12 @@ object OptionsUtil {
if (config.searchPc != defaultConfig.searchPc) {
r = r :+ "--search-pc"
}
if (config.rwTrace != defaultConfig.rwTrace) {
r = r :+ "--rw-trace"
}
if (config.rwMax != defaultConfig.rwMax) {
r = r ++ ISZ[String]("--rw-max", config.rwMax.string)
}
}
config.background match {
case Config.BackgroundMode.Type => r = r ++ ISZ[String]("--background", "type")
Expand Down
24 changes: 12 additions & 12 deletions shared/src/main/scala/org/sireum/logika/plugin/RewritePlugin.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -38,8 +38,6 @@ import org.sireum.logika.{Logika, RewritingSystem, Smt2, State, StepProofContext

val justificationName: ISZ[String] = ISZ("org", "sireum", "justification")

val maxIt: Z = 100

override def canHandle(logika: Logika, just: AST.ProofAst.Step.Justification): B = {
just match {
case just: AST.ProofAst.Step.Justification.Apply =>
Expand Down Expand Up @@ -96,12 +94,12 @@ import org.sireum.logika.{Logika, RewritingSystem, Smt2, State, StepProofContext
}
}
}
val rwPc = Rewriter(logika.th, provenClaims, patterns, ISZ())
val rwPc = Rewriter(logika.th, provenClaims, patterns, logika.config.rwTrace, ISZ())
val fromCoreClaim = RewritingSystem.translate(logika.th, F, fromClaim)
var done = F
var rwClaim = fromCoreClaim
var i = 0
while (!done && i < maxIt) {
while (!done && i < logika.config.rwMax) {
rwClaim = rwPc.transformCoreExpBase(rwClaim) match {
case MSome(c) =>
if (rwPc.trace.nonEmpty) {
Expand All @@ -116,6 +114,14 @@ import org.sireum.logika.{Logika, RewritingSystem, Smt2, State, StepProofContext
i = i + 1
}
val stepClaim = RewritingSystem.translate(logika.th, F, step.claim)
val traceOpt: Option[ST] = if (logika.config.rwTrace) {
Some(
st"""Rewriting trace:
|
|${(for (te <- rwPc.trace) yield te.toST, "\n\n")}""")
} else {
None()
}
if (rwClaim == stepClaim) {
reporter.inform(just.id.attr.posOpt.get, Reporter.Info.Kind.Verified,
st"""Matched:
Expand All @@ -124,10 +130,7 @@ import org.sireum.logika.{Logika, RewritingSystem, Smt2, State, StepProofContext
|After rewriting $from:
| ${fromCoreClaim.prettyST}
|
|Rewriting trace:
|
|${(for (te <- rwPc.trace) yield te.toST, "\n\n")}
|""".render)
|$traceOpt""".render)
val q = logika.evalRegularStepClaimRtCheck(smt2, cache, F, state, step.claim, step.id.posOpt, reporter)
val (stat, nextFresh, claims) = (q._1, q._2, q._3 :+ q._4)
return Plugin.Result(stat, nextFresh, claims)
Expand All @@ -139,10 +142,7 @@ import org.sireum.logika.{Logika, RewritingSystem, Smt2, State, StepProofContext
|After rewriting $from to:
| ${rwClaim.prettyST}
|
|Rewriting trace:
|
|${(for (te <- rwPc.trace) yield te.toST, "\n\n")}
|""".render)
|$traceOpt""".render)
return emptyResult
}
}
Expand Down

0 comments on commit b507d03

Please sign in to comment.