Implemented the command line switch /useArrayTheory. This switch should be used only in conjunction with /monomorphize. When enabled, this switch uses the native Z3 array theory rather than the Select-Update axioms.

6 files changed, 90 insertions, 29 deletions

diff --git a/Source/Core/Absy.ssc b/Source/Core/Absy.ssc
index fc706e2c..00142344 100644
--- a/Source/Core/Absy.ssc
+++ b/Source/Core/Absy.ssc
@@ -429,6 +429,20 @@ namespace Microsoft.Boogie
       return true;

     }

 

+    public void AddAttribute(string! name, object! val)

+    {

+      QKeyValue kv;

+      for (kv = this.Attributes; kv != null; kv = kv.Next) {

+        if (kv.Key == name) {

+          kv.Params.Add(val);

+          break;

+        }

+      }

+      if (kv == null) {

+        Attributes = new QKeyValue(tok, name, new List<object!>(new object![] { val }), Attributes);

+      }

+    }                                   

+    

     public abstract void Emit(TokenTextWriter! stream, int level);

     public abstract void Register(ResolutionContext! rc);

 

diff --git a/Source/Core/CommandLineOptions.ssc b/Source/Core/CommandLineOptions.ssc
index d3eb2eba..5912220d 100644
--- a/Source/Core/CommandLineOptions.ssc
+++ b/Source/Core/CommandLineOptions.ssc
@@ -151,6 +151,8 @@ namespace Microsoft.Boogie
     public enum BvHandling { None, Z3Native, ToInt }

     public BvHandling Bitvectors = BvHandling.Z3Native;

     

+    public bool UseArrayTheory = false;

+    

     public bool UseAbstractInterpretation = true;          // true iff the user want to use abstract interpretation

     public int  /*0..9*/StepsBeforeWidening = 0;           // The number of steps that must be done before applying a widen operator

     invariant 0 <= StepsBeforeWidening && StepsBeforeWidening <= 9;

@@ -788,7 +790,7 @@ namespace Microsoft.Boogie
               }

             }

             break;

-

+              

           case "-contractInfer":

           case "/contractInfer":

             ContractInfer = true;

@@ -1132,7 +1134,8 @@ namespace Microsoft.Boogie
               ps.CheckBooleanFlag("reflectAdd", ref ReflectAdd) ||

               ps.CheckBooleanFlag("z3types", ref Z3types) ||

               ps.CheckBooleanFlag("z3multipleErrors", ref z3AtFlag, false) ||

-              ps.CheckBooleanFlag("monomorphize", ref Monomorphize)

+              ps.CheckBooleanFlag("monomorphize", ref Monomorphize) ||

+              ps.CheckBooleanFlag("useArrayTheory", ref UseArrayTheory)

               )

             {

               // one of the boolean flags matched

diff --git a/Source/Provers/Z3/TypeDeclCollector.ssc b/Source/Provers/Z3/TypeDeclCollector.ssc
index 26af2f2c..80d4c4a5 100644
--- a/Source/Provers/Z3/TypeDeclCollector.ssc
+++ b/Source/Provers/Z3/TypeDeclCollector.ssc
@@ -95,9 +95,25 @@ namespace Microsoft.Boogie.Z3
 

     private void RegisterType(Type! type)

     {

-      if (!type.IsBv || !NativeBv) return;

-

-      if (!KnownTypes.ContainsKey(type)) {

+      if (KnownTypes.ContainsKey(type)) return;

+      

+      if (type.IsMap && CommandLineOptions.Clo.UseArrayTheory) {

+        string declString = "";

+        MapType! mapType = type.AsMap;

+        

+        declString += "(DEFTYPE " +  TypeToString(type) + " :BUILTIN Array ";

+		foreach (Type! t in mapType.Arguments) {

+		  declString += TypeToString(t);

+		  declString += " ";

+		}

+		declString += TypeToString(mapType.Result);

+		declString += ")";

+		AddDeclaration(declString);

+		KnownTypes.Add(type, true);

+		return;

+      }

+      

+      if (type.IsBv && NativeBv) {

         int bits = type.BvBits;

         string name = TypeToString(type);

 

@@ -114,7 +130,7 @@ namespace Microsoft.Boogie.Z3
     }

 

     public override bool Visit(VCExprNAry! node, bool arg) {

-      // there are a couple of cases where operators have to be

+      // there are a couple cases where operators have to be

       // registered by generating appropriate Z3 statements

 

       if (node.Op is VCExprBvConcatOp) {

@@ -187,11 +203,14 @@ namespace Microsoft.Boogie.Z3
     }

 

     private string? ExtractBuiltin(Function! f) {

+      string? retVal = null; 

       if (NativeBv) {

-        return f.FindStringAttribute("bvbuiltin");

-      } else {

-        return null;

+        retVal = f.FindStringAttribute("bvbuiltin");

+      } 

+      if (retVal == null) {

+        retVal = f.FindStringAttribute("builtin");

       }

+      return retVal;

     }

 

     public override bool Visit(VCExprVar! node, bool arg) {

diff --git a/Source/VCExpr/TypeErasure.ssc b/Source/VCExpr/TypeErasure.ssc
index f282b342..604be456 100644
--- a/Source/VCExpr/TypeErasure.ssc
+++ b/Source/VCExpr/TypeErasure.ssc
@@ -23,7 +23,7 @@ namespace Microsoft.Boogie.TypeErasure
   // really be provided by the Spec# container classes; maybe one

   // could integrate the functions in a nicer way?)

   public class HelperFuns {

-

+    

     public static Function! BoogieFunction(string! name, List<TypeVariable!>! typeParams,

                                            params Type[]! types)

       requires types.Length > 0;

@@ -542,7 +542,7 @@ namespace Microsoft.Boogie.TypeErasure
 

     [Pure]

     public override bool UnchangedType(Type! type) {

-      return type.IsInt || type.IsBool || type.IsBv;

+      return type.IsInt || type.IsBool || type.IsBv || (type.IsMap && CommandLineOptions.Clo.UseArrayTheory);

     }    

 

     public VCExpr! Cast(VCExpr! expr, Type! toType)

diff --git a/Source/VCExpr/TypeErasureArguments.ssc b/Source/VCExpr/TypeErasureArguments.ssc
index 98baf874..4fe37a4e 100644
--- a/Source/VCExpr/TypeErasureArguments.ssc
+++ b/Source/VCExpr/TypeErasureArguments.ssc
@@ -148,6 +148,7 @@ namespace Microsoft.Boogie.TypeErasure
       string! baseName = synonym.Name;

       int typeParamNum = abstractedType.FreeVariables.Length +

                          abstractedType.TypeParameters.Length;

+      

       int arity = typeParamNum + abstractedType.Arguments.Length;

 

       Type![]! selectTypes = new Type! [arity + 2];

@@ -160,8 +161,13 @@ namespace Microsoft.Boogie.TypeErasure
         storeTypes[i] = AxBuilder.T;

       }

       // Fill in the map type

-      selectTypes[i] = AxBuilder.U;

-      storeTypes[i] = AxBuilder.U;

+      if (CommandLineOptions.Clo.UseArrayTheory) {

+        selectTypes[i] = abstractedType;

+        storeTypes[i] = abstractedType;

+      } else {

+        selectTypes[i] = AxBuilder.U;

+        storeTypes[i] = AxBuilder.U;

+      }

       i++;

       // Fill in the index types

       foreach (Type! type in abstractedType.Arguments)

@@ -186,17 +192,25 @@ namespace Microsoft.Boogie.TypeErasure
       }

       i++;

       // Fill in the map type which is the output of the store function

-      storeTypes[i] = AxBuilder.U;

+      if (CommandLineOptions.Clo.UseArrayTheory) 

+        storeTypes[i] = abstractedType;

+      else

+        storeTypes[i] = AxBuilder.U;

       NonNullType.AssertInitialized(selectTypes);

       NonNullType.AssertInitialized(storeTypes);

       

-      select = HelperFuns.BoogieFunction(baseName + "Select", selectTypes);

+      select = HelperFuns.BoogieFunction(baseName + "Select", selectTypes);      

       store = HelperFuns.BoogieFunction(baseName + "Store", storeTypes);

-

-      AxBuilder.AddTypeAxiom(GenMapAxiom0(select, store, 

+      

+      if (CommandLineOptions.Clo.UseArrayTheory) {

+        select.AddAttribute("builtin", "select");

+        store.AddAttribute("builtin", "store");

+      } else {

+        AxBuilder.AddTypeAxiom(GenMapAxiom0(select, store, 

                  abstractedType.TypeParameters.Length, abstractedType.FreeVariables.Length));

-      AxBuilder.AddTypeAxiom(GenMapAxiom1(select, store, 

+        AxBuilder.AddTypeAxiom(GenMapAxiom1(select, store, 

                  abstractedType.TypeParameters.Length, abstractedType.FreeVariables.Length));

+      }

     }

 

     ///////////////////////////////////////////////////////////////////////////

diff --git a/Source/VCExpr/TypeErasurePremisses.ssc b/Source/VCExpr/TypeErasurePremisses.ssc
index 40c062e0..734bc16b 100644
--- a/Source/VCExpr/TypeErasurePremisses.ssc
+++ b/Source/VCExpr/TypeErasurePremisses.ssc
@@ -473,7 +473,7 @@ namespace Microsoft.Boogie.TypeErasure
       select = CreateAccessFun(typeParams, originalInTypes,

                                abstractedType.Result, synonym.Name + "Select",

                                out implicitSelectParams, out explicitSelectParams);

-

+      

       // store, which gets one further argument: the assigned rhs

       originalInTypes.Add(abstractedType.Result);

 

@@ -482,16 +482,21 @@ namespace Microsoft.Boogie.TypeErasure
                               mapTypeSynonym, synonym.Name + "Store",

                               out implicitStoreParams, out explicitStoreParams);

 

-      // the store function does not have any explicit type parameters

+	  // the store function does not have any explicit type parameters

       assert explicitStoreParams.Count == 0;

-

-      AxBuilder.AddTypeAxiom(GenMapAxiom0(select, store,

-                                          abstractedType.Result,

-                                          implicitSelectParams, explicitSelectParams,

-                                          originalInTypes));

-      AxBuilder.AddTypeAxiom(GenMapAxiom1(select, store, 

-                                          abstractedType.Result,

-                                          explicitSelectParams));

+      

+      if (CommandLineOptions.Clo.UseArrayTheory) {

+        select.AddAttribute("builtin", "select");

+        store.AddAttribute("builtin", "store");

+      } else {                       

+        AxBuilder.AddTypeAxiom(GenMapAxiom0(select, store,

+                                            abstractedType.Result,

+                                            implicitSelectParams, explicitSelectParams,

+                                            originalInTypes));

+        AxBuilder.AddTypeAxiom(GenMapAxiom1(select, store, 

+                                            abstractedType.Result,

+                                            explicitSelectParams));

+      }

     }

 

     protected void GenTypeAxiomParams(MapType! abstractedType, TypeCtorDecl! synonymDecl,

@@ -506,7 +511,12 @@ namespace Microsoft.Boogie.TypeErasure
       TypeSeq! mapTypeParams = new TypeSeq ();

       foreach (TypeVariable! var in abstractedType.FreeVariables)

         mapTypeParams.Add(var);

-      mapTypeSynonym = new CtorType (Token.NoToken, synonymDecl, mapTypeParams);

+      

+      if (CommandLineOptions.Clo.UseArrayTheory)

+        mapTypeSynonym = abstractedType;

+      else 

+        mapTypeSynonym = new CtorType (Token.NoToken, synonymDecl, mapTypeParams);

+        

       originalIndexTypes.Add(mapTypeSynonym);

       originalIndexTypes.AddRange(abstractedType.Arguments.ToList());

     }

@@ -524,6 +534,7 @@ namespace Microsoft.Boogie.TypeErasure
                                                    HelperFuns.ToSeq(originalTypeParams),

                                                    out implicitTypeParams,

                                                    out explicitTypeParams);

+      

       Type[]! ioTypes = new Type [explicitTypeParams.Count + originalInTypes.Count + 1];

       int i = 0;

       for (; i < explicitTypeParams.Count; ++i)