Skip to content

Commit

Permalink
Fixed cli opt.
Browse files Browse the repository at this point in the history
  • Loading branch information
@robby-phd
robby-phd committed Feb 14, 2024
1 parent 384be13 commit d18eca1
Show file tree
Hide file tree
Showing 3 changed files with 28 additions and 43 deletions.
7 changes: 5 additions & 2 deletions shared/src/main/scala/org/sireum/logika/cli.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -137,8 +137,11 @@ object cli {
OptGroup(name = "Optimizations", opts = ISZ(
parOpt,
Opt(name = "branchPar", longKey = "par-branch", shortKey = None(),
tpe = Type.Choice("branchPar", None(), ISZ("all", "returns", "disabled")),
description = "Branch parallelization mode"),
tpe = Type.Flag(F),
description = "Enable branch parallelization"),
Opt(name = "branchParReturn", longKey = "par-branch-return", shortKey = None(),
tpe = Type.Flag(F),
description = "Only use branch parallelization if all branches return"),
Opt(name = "rwPar", longKey = "par-rw", shortKey = None(),
tpe = Type.Flag(T),
description = "Enable rewriting parallelization")
Expand Down
46 changes: 14 additions & 32 deletions shared/src/main/scala/org/sireum/logika/options/OptionsCli.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -58,12 +58,6 @@ object OptionsCli {
'Uninterpreted
}

@enum object LogikaBranchPar {
'All
'Returns
'Disabled
}

@datatype class LogikaOption(
val help: String,
val args: ISZ[String],
Expand Down Expand Up @@ -96,7 +90,8 @@ object OptionsCli {
val logAtRewrite: B,
val stats: B,
val par: Option[Z],
val branchPar: LogikaBranchPar.Type,
val branchPar: B,
val branchParReturn: B,
val rwPar: B,
val dontSplitFunQuant: B,
val splitAll: B,
Expand Down Expand Up @@ -184,26 +179,6 @@ import OptionsCli._
return r
}

def parseLogikaBranchParH(arg: String): Option[LogikaBranchPar.Type] = {
arg.native match {
case "all" => return Some(LogikaBranchPar.All)
case "returns" => return Some(LogikaBranchPar.Returns)
case "disabled" => return Some(LogikaBranchPar.Disabled)
case s =>
reporter.error(None(), "OptionsCli", s"Expecting one of the following: { all, returns, disabled }, but found '$s'.")
return None()
}
}

def parseLogikaBranchPar(args: ISZ[String], i: Z): Option[LogikaBranchPar.Type] = {
if (i >= args.size) {
reporter.error(None(), "OptionsCli", "Expecting one of the following: { all, returns, disabled }, but none found.")
return None()
}
val r = parseLogikaBranchParH(args(i))
return r
}

def parseLogika(args: ISZ[String], i: Z): Option[LogikaTopOption] = {
val help =
st"""Logika Verifier Options
Expand Down Expand Up @@ -278,8 +253,8 @@ import OptionsCli._
|-p, --par Enable parallelization (with CPU cores percentage to
| use) (accepts an optional integer; min is 1; max is
| 100; default is 100)
| --par-branch Branch parallelization mode (expects one of { all,
| returns, disabled }; default: all)
| --par-branch Enable branch parallelization
| --par-branch-return Only use branch parallelization if all branches return
| --par-rw Enable rewriting parallelization
|
|Path Splitting Options:
Expand Down Expand Up @@ -343,7 +318,8 @@ import OptionsCli._
var logAtRewrite: B = true
var stats: B = false
var par: Option[Z] = None()
var branchPar: LogikaBranchPar.Type = LogikaBranchPar.All
var branchPar: B = false
var branchParReturn: B = false
var rwPar: B = true
var dontSplitFunQuant: B = false
var splitAll: B = false
Expand Down Expand Up @@ -548,11 +524,17 @@ import OptionsCli._
case _ => return None()
}
} else if (arg == "--par-branch") {
val o: Option[LogikaBranchPar.Type] = parseLogikaBranchPar(args, j + 1)
val o: Option[B] = { j = j - 1; Some(!branchPar) }
o match {
case Some(v) => branchPar = v
case _ => return None()
}
} else if (arg == "--par-branch-return") {
val o: Option[B] = { j = j - 1; Some(!branchParReturn) }
o match {
case Some(v) => branchParReturn = v
case _ => return None()
}
} else if (arg == "--par-rw") {
val o: Option[B] = { j = j - 1; Some(!rwPar) }
o match {
Expand Down Expand Up @@ -670,7 +652,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, rwPar, dontSplitFunQuant, splitAll, splitContract, splitIf, splitMatch, rwMax, rwTrace, 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, rwPar, dontSplitFunQuant, splitAll, splitContract, splitIf, splitMatch, rwMax, rwTrace, elideEncoding, rawInscription, rlimit, sequential, simplify, smt2SatConfigs, smt2ValidConfigs, satTimeout, timeout, searchPC))
}

def parseArguments(args: ISZ[String], i: Z): ISZ[String] = {
Expand Down
18 changes: 9 additions & 9 deletions shared/src/main/scala/org/sireum/logika/options/OptionsUtil.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -114,10 +114,11 @@ object OptionsUtil {
case OptionsCli.LogikaFPRoundingMode.TowardZero => "RTZ"
}
val parCores = LibUtil.parCoresOpt(maxCores, o.par)
val branchPar: org.sireum.logika.Config.BranchPar.Type = o.branchPar match {
case OptionsCli.LogikaBranchPar.All => org.sireum.logika.Config.BranchPar.All
case OptionsCli.LogikaBranchPar.Returns => org.sireum.logika.Config.BranchPar.OnlyAllReturns
case OptionsCli.LogikaBranchPar.Disabled => org.sireum.logika.Config.BranchPar.Disabled
val branchPar: org.sireum.logika.Config.BranchPar.Type = (o.branchPar, o.branchParReturn) match {
case (T, F) => org.sireum.logika.Config.BranchPar.All
case (T, T) => org.sireum.logika.Config.BranchPar.OnlyAllReturns
case (F, F) => org.sireum.logika.Config.BranchPar.Disabled
case (F, T) => org.sireum.logika.Config.BranchPar.Disabled
}
val spMode: Config.StrictPureMode.Type = o.strictPureMode match {
case OptionsCli.LogikaStrictPureMode.Default => Config.StrictPureMode.Default
Expand Down Expand Up @@ -224,12 +225,11 @@ object OptionsUtil {
}
}
if (config.branchPar != defaultConfig.branchPar) {
val value: String = config.branchPar match {
case Config.BranchPar.All => "all"
case Config.BranchPar.OnlyAllReturns => "returns"
case Config.BranchPar.Disabled => "disabled"
config.branchPar match {
case Config.BranchPar.All => r = r :+ "--par-branch"
case Config.BranchPar.OnlyAllReturns => r = r ++ ISZ[String]("--par-branch", "--par-branch-return")
case Config.BranchPar.Disabled =>
}
r = r ++ ISZ[String]("--par-branch", value)
}
if (config.sat != defaultConfig.sat) {
r = r :+ "--sat"
Expand Down

0 comments on commit d18eca1

Please sign in to comment.