diff --git a/jvm/src/test/scala/org/sireum/logika/LogikaTest.scala b/jvm/src/test/scala/org/sireum/logika/LogikaTest.scala index 717c3bc4..7b15027f 100644 --- a/jvm/src/test/scala/org/sireum/logika/LogikaTest.scala +++ b/jvm/src/test/scala/org/sireum/logika/LogikaTest.scala @@ -99,7 +99,9 @@ object LogikaTest { rwTrace = T, rwMax = 100, rwPar = T, - rwEvalTrace = T + rwEvalTrace = T, + branchParPredNum = 2, + branchParPredComp = 10 ) 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 22decdf4..57a59518 100644 --- a/shared/src/main/scala/org/sireum/logika/Config.scala +++ b/shared/src/main/scala/org/sireum/logika/Config.scala @@ -70,7 +70,9 @@ import org.sireum._ val rwTrace: B, val rwMax: Z, val rwPar: B, - val rwEvalTrace: B) { + val rwEvalTrace: B, + val branchParPredNum: Z, + val branchParPredComp: Z) { @memoize def fingerprint: U64 = { return ops.StringOps(string).sha3U64(T, T) diff --git a/shared/src/main/scala/org/sireum/logika/Logika.scala b/shared/src/main/scala/org/sireum/logika/Logika.scala index a92261ce..ca708d3e 100644 --- a/shared/src/main/scala/org/sireum/logika/Logika.scala +++ b/shared/src/main/scala/org/sireum/logika/Logika.scala @@ -4393,12 +4393,12 @@ import Util._ } @pure def shouldPar: B = { - if (branches.size > 2) { - return T - } if (branches.size == 1) { return F } + if (branches.size >= config.branchParPredNum) { + return T + } var compNum = 0 for (b <- branches) { @@ -4408,7 +4408,7 @@ import Util._ } } - if (compNum < 10) { + if (compNum < config.branchParPredComp) { return F } diff --git a/shared/src/main/scala/org/sireum/logika/cli.scala b/shared/src/main/scala/org/sireum/logika/cli.scala index a73fc730..b666c9f5 100644 --- a/shared/src/main/scala/org/sireum/logika/cli.scala +++ b/shared/src/main/scala/org/sireum/logika/cli.scala @@ -148,6 +148,12 @@ object cli { Opt(name = "branchParReturn", longKey = "par-branch-return", shortKey = None(), tpe = Type.Flag(F), description = "Only use branch parallelization if all branches return"), + Opt(name = "branchPredNum", longKey = "par-branch-pred-num", shortKey = None(), + tpe = Type.Num(sep = None(), default = 2, min = Some(2), max = None()), + description = "Branch parallelization prediction minimum number of branches"), + Opt(name = "branchPredComplexity", longKey = "par-branch-pred-complexity", shortKey = None(), + tpe = Type.Num(sep = None(), default = 10, min = Some(0), max = None()), + description = "Branch parallelization prediction statement complexity"), Opt(name = "rwPar", longKey = "par-rw", shortKey = None(), tpe = Type.Flag(T), description = "Enable rewriting parallelization") 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 623541b1..50719038 100644 --- a/shared/src/main/scala/org/sireum/logika/options/OptionsCli.scala +++ b/shared/src/main/scala/org/sireum/logika/options/OptionsCli.scala @@ -92,6 +92,8 @@ object OptionsCli { val par: Option[Z], val branchPar: B, val branchParReturn: B, + val branchPredNum: Z, + val branchPredComplexity: Z, val rwPar: B, val dontSplitFunQuant: B, val splitAll: B, @@ -256,6 +258,12 @@ import OptionsCli._ | 100; default is 100) | --par-branch Enable branch parallelization | --par-branch-return Only use branch parallelization if all branches return + | --par-branch-pred-num + | Enable branch parallelization (expects an integer; + | min is 2; default is 2) + | --par-branch-pred-complexity + | Enable branch parallelization (expects an integer; + | min is 0; default is 10) | --par-rw Enable rewriting parallelization | |Path Splitting Options: @@ -322,6 +330,8 @@ import OptionsCli._ var par: Option[Z] = None() var branchPar: B = false var branchParReturn: B = false + var branchPredNum: Z = 2 + var branchPredComplexity: Z = 10 var rwPar: B = true var dontSplitFunQuant: B = false var splitAll: B = false @@ -538,6 +548,18 @@ import OptionsCli._ case Some(v) => branchParReturn = v case _ => return None() } + } else if (arg == "--par-branch-pred-num") { + val o: Option[Z] = parseNum(args, j + 1, Some(2), None()) + o match { + case Some(v) => branchPredNum = v + case _ => return None() + } + } else if (arg == "--par-branch-pred-complexity") { + val o: Option[Z] = parseNum(args, j + 1, Some(0), None()) + o match { + case Some(v) => branchPredComplexity = v + case _ => return None() + } } else if (arg == "--par-rw") { val o: Option[B] = { j = j - 1; Some(!rwPar) } o match { @@ -661,7 +683,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, branchPar, branchParReturn, rwPar, dontSplitFunQuant, splitAll, splitContract, splitIf, splitMatch, rwMax, rwTrace, rwEvalTrace, 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, branchPar, branchParReturn, branchPredNum, branchPredComplexity, rwPar, dontSplitFunQuant, splitAll, splitContract, splitIf, splitMatch, rwMax, rwTrace, rwEvalTrace, 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 19f8c045..42b81d12 100644 --- a/shared/src/main/scala/org/sireum/logika/options/OptionsUtil.scala +++ b/shared/src/main/scala/org/sireum/logika/options/OptionsUtil.scala @@ -176,7 +176,9 @@ object OptionsUtil { rwTrace = o.rwTrace, rwMax = o.rwMax, rwPar = o.rwPar, - rwEvalTrace = o.rwEvalTrace + rwEvalTrace = o.rwEvalTrace, + branchParPredNum = o.branchPredNum, + branchParPredComp = o.branchPredComplexity ) return Either.Left(config) } @@ -337,6 +339,12 @@ object OptionsUtil { if (config.rwEvalTrace != defaultConfig.rwEvalTrace) { r = r :+ "--rw-eval-trace" } + if (config.branchParPredNum != defaultConfig.branchParPredNum) { + r = r ++ ISZ[String]("--par-branch-pred-num", config.branchParPredNum.string) + } + if (config.branchParPredComp != defaultConfig.branchParPredComp) { + r = r ++ ISZ[String]("--par-branch-pred-complexity", config.branchParPredComp.string) + } } config.background match { case Config.BackgroundMode.Type => r = r ++ ISZ[String]("--background", "type")