Chalice: Clean up /percentageSupport command line option to adapt to the usage of reals for permissions.

3 files changed, 15 insertions, 39 deletions

diff --git a/Chalice/src/main/scala/Chalice.scala b/Chalice/src/main/scala/Chalice.scala
index 2514d6b1..ca39e95e 100644
--- a/Chalice/src/main/scala/Chalice.scala
+++ b/Chalice/src/main/scala/Chalice.scala
@@ -34,11 +34,9 @@ object Chalice {
   private[chalice] var skipDeadlockChecks = false: Boolean;

   private[chalice] var skipTermination = false: Boolean;

   private[chalice] var noFreeAssume = false: Boolean;

-  // percentageSupport 0: use multiplication directly

-  // percentageSupport 1: fix Permission$denominator as constant (possibly unsound for small values of the constant?)

-  // percentageSupport 2: use function and provide some (redundant) axioms

-  // percentageSupport 3: use an uninterpreted function and axiomatize the properties of multiplication

-  private[chalice] var percentageSupport = 2;

+  // percentageSupport 0: use multiplication directly (default)

+  // percentageSupport 1: use function and provide some (redundant) axioms

+  private[chalice] var percentageSupport = 0;

   private[chalice] var smoke = false;

   private[chalice] var smokeAll = false;

   private[chalice] var timingVerbosity = 1;

@@ -147,10 +145,8 @@ object Chalice {
           "level 2: unfold predicates and functions with receiver this in pre and postconditions\n"+

           "level 3 or above: level 2 + autoMagic"),

       "percentageSupport:<n>" -> ("determin how percentage permissions are translated to Boogie\n"+

-          "0: use multiplication directly (can cause performance problems)\n"+

-          "1: fix Permission$denominator as constant (possibly unsound)\n"+

-          "2: use a function and provide some (redundant) axioms\n"+

-          "3: use an uninterpreted function and axiomatize the properties of multiplication"),

+          "0: use multiplication directly (default)\n"+

+          "1: use a function and provide some (redundant) axioms")+

       "boogieOpt:<arg>, /bo:<arg>" -> "specify additional Boogie options"

     )

     lazy val help = {

@@ -178,7 +174,7 @@ object Chalice {
      else if (a.startsWith("/percentageSupport:") || a.startsWith("-percentageSupport:")) {

        try {

          val in = Integer.parseInt(a.substring(19));

-         if (in < 0 || in > 3) CommandLineError("/percentageSupport takes only values 0, 1, 2 or 3", help)

+         if (in < 0 || in > 1) CommandLineError("/percentageSupport takes only values 0 or 1", help)

          else percentageSupport = in

        } catch { case _ => CommandLineError("/percentageSupport takes integer argument", help); }

      }

@@ -214,9 +210,7 @@ object Chalice {
     

     percentageSupport match {

       case 0 => TranslatorPrelude.addComponent(PercentageStandardPL)

-      case 1 => TranslatorPrelude.addComponent(PercentageStandardPL, PercentageFixedDenominatorPL)

-      case 2 => TranslatorPrelude.addComponent(PercentageFunctionPL)

-      case 3 => TranslatorPrelude.addComponent(PercentageUninterpretedFunctionPL)

+      case 1 => TranslatorPrelude.addComponent(PercentageFunctionPL)

     }

 

     // check that input files exist

diff --git a/Chalice/src/main/scala/Prelude.scala b/Chalice/src/main/scala/Prelude.scala
index a7ff156d..4a333f8e 100644
--- a/Chalice/src/main/scala/Prelude.scala
+++ b/Chalice/src/main/scala/Prelude.scala
@@ -53,7 +53,7 @@ object TranslatorPrelude {
 sealed abstract class PreludeComponent {

   // determines the order in which the components are output

   def compare(that: PreludeComponent): Boolean = {

-    val order: List[PreludeComponent] = List(CopyrightPL, TypesPL, PermissionTypesAndConstantsPL, PercentageFixedDenominatorPL, PercentageFunctionPL, PercentageUninterpretedFunctionPL, CreditsAndMuPL, PermissionFunctionsAndAxiomsPL, IfThenElsePL, StringPL, AxiomatizationOfSequencesPL)

+    val order: List[PreludeComponent] = List(CopyrightPL, TypesPL, PermissionTypesAndConstantsPL, PercentageFunctionPL, CreditsAndMuPL, PermissionFunctionsAndAxiomsPL, IfThenElsePL, StringPL, AxiomatizationOfSequencesPL)

     if (!order.contains(this)) false

     else order.indexOf(this) < order.indexOf(that)

   }

@@ -105,19 +105,15 @@ const predicateK: real;"""
 }

 object PercentageStandardPL extends PreludeComponent {

   val text = """

-axiom (0 < channelK && 1000*channelK < Permission$denominator);

-axiom (0 < monitorK && 1000*monitorK < Permission$denominator);

-axiom (0 < predicateK && 1000*predicateK < Permission$denominator);

-axiom Permission$FullFraction  == 100*Permission$denominator;

+axiom Permission$FullFraction  == 1.0;

+axiom 0.0 < channelK && 1000.0*channelK < 0.01;

+axiom 0.0 < monitorK && 1000.0*monitorK < 0.01;

+axiom 0.0 < predicateK && 1000.0*predicateK < 0.01;

 axiom predicateK == channelK && channelK == monitorK;"""

 }

-object PercentageFixedDenominatorPL extends PreludeComponent {

-  val text = """

-axiom Permission$denominator == 100000000000;"""

-}

 object PercentageFunctionPL extends PreludeComponent {

   val text = """

-function {:inline} Fractions(n: int) returns (real)

+function Fractions(n: int) returns (real)

 {

   n / 100.0

 }

@@ -129,20 +125,6 @@ axiom 0.0 < monitorK && 1000.0*monitorK < Fractions(1);
 axiom 0.0 < predicateK && 1000.0*predicateK < Fractions(1);

 axiom predicateK == channelK && channelK == monitorK;"""

 }

-object PercentageUninterpretedFunctionPL extends PreludeComponent {

-  val text = """

-function Fractions(n: int) returns (int);

-function Fractions'(n: int) returns (int);

-axiom (forall x: int :: { Fractions(x) } Fractions(x) == Fractions'(x));

-axiom (forall x,y: int :: 0 <= x && x <= y ==> Fractions'(x) <= Fractions'(y));

-axiom (forall x,y: int :: { Fractions(x), Fractions(y) } Fractions(x) + Fractions(y) == Fractions'(x+y));

-

-axiom Permission$FullFraction  == Fractions(100);

-axiom 0 < channelK && 1000*channelK < Fractions(1);

-axiom 0 < monitorK && 1000*monitorK < Fractions(1);

-axiom 0 < predicateK && 1000*predicateK < Fractions(1);

-axiom predicateK == channelK && channelK == monitorK;"""

-}

 object CreditsAndMuPL extends PreludeComponent {

   def text = {

     val base = """

diff --git a/Chalice/src/main/scala/Translator.scala b/Chalice/src/main/scala/Translator.scala
index 93df061e..e57c861e 100644
--- a/Chalice/src/main/scala/Translator.scala
+++ b/Chalice/src/main/scala/Translator.scala
@@ -3099,8 +3099,8 @@ object TranslationHelper {
   def permissionOnePercent = percentPermission(1);

   def percentPermission(e: Expr) = {

     Chalice.percentageSupport match {

-      case 0 | 1 => e*VarExpr("Permission$denominator")

-      case 2 | 3 => FunctionApp("Fractions", List(e))

+      case 0 => int2real(e)*0.01

+      case 1 => FunctionApp("Fractions", List(e))

     }

   }

   def int2real(e: Expr): Expr = FunctionApp("real", List(e))