diff --git a/jvm/src/test/scala/org/sireum/logika/LogikaTest.scala b/jvm/src/test/scala/org/sireum/logika/LogikaTest.scala index 63011aaf..1140b233 100644 --- a/jvm/src/test/scala/org/sireum/logika/LogikaTest.scala +++ b/jvm/src/test/scala/org/sireum/logika/LogikaTest.scala @@ -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 diff --git a/shared/src/main/scala/org/sireum/logika/Config.scala b/shared/src/main/scala/org/sireum/logika/Config.scala index aedd6652..20dfce40 100644 --- a/shared/src/main/scala/org/sireum/logika/Config.scala +++ b/shared/src/main/scala/org/sireum/logika/Config.scala @@ -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) diff --git a/shared/src/main/scala/org/sireum/logika/RewritingSystem.scala b/shared/src/main/scala/org/sireum/logika/RewritingSystem.scala index fbac7fc0..b6aab830 100644 --- a/shared/src/main/scala/org/sireum/logika/RewritingSystem.scala +++ b/shared/src/main/scala/org/sireum/logika/RewritingSystem.scala @@ -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 { @@ -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) } } diff --git a/shared/src/main/scala/org/sireum/logika/cli.scala b/shared/src/main/scala/org/sireum/logika/cli.scala index eb3d89b1..5a19b3af 100644 --- a/shared/src/main/scala/org/sireum/logika/cli.scala +++ b/shared/src/main/scala/org/sireum/logika/cli.scala @@ -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), diff --git a/shared/src/main/scala/org/sireum/logika/options/OptionsCli.scala b/shared/src/main/scala/org/sireum/logika/options/OptionsCli.scala index dfeffb22..28e69b9e 100644 --- a/shared/src/main/scala/org/sireum/logika/options/OptionsCli.scala +++ b/shared/src/main/scala/org/sireum/logika/options/OptionsCli.scala @@ -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, @@ -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 @@ -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 @@ -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 { @@ -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] = { diff --git a/shared/src/main/scala/org/sireum/logika/options/OptionsUtil.scala b/shared/src/main/scala/org/sireum/logika/options/OptionsUtil.scala index 9a38bb2b..18bd3bac 100644 --- a/shared/src/main/scala/org/sireum/logika/options/OptionsUtil.scala +++ b/shared/src/main/scala/org/sireum/logika/options/OptionsUtil.scala @@ -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) } @@ -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") diff --git a/shared/src/main/scala/org/sireum/logika/plugin/RewritePlugin.scala b/shared/src/main/scala/org/sireum/logika/plugin/RewritePlugin.scala index 99d06150..134c9aa6 100644 --- a/shared/src/main/scala/org/sireum/logika/plugin/RewritePlugin.scala +++ b/shared/src/main/scala/org/sireum/logika/plugin/RewritePlugin.scala @@ -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 => @@ -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) { @@ -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: @@ -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) @@ -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 } }