fix and get rid of more accessors other than the two that are require…

…d for a phase
viperproject · May 9, 2023 · 67c4d65 · 67c4d65
1 parent 6b5c0f1
commit 67c4d65
Show file tree

Hide file tree

Showing 4 changed files with 9 additions and 19 deletions.
diff --git a/Source/ProofGeneration/Passification/PassificationEndToEnd.cs b/Source/ProofGeneration/Passification/PassificationEndToEnd.cs
@@ -43,8 +43,6 @@ public class PassificationEndToEnd
         private StateRelationData oldRelationData;
         private IProgramAccessor passiveProgramAccessor;
 
-        private IProgramAccessor beforePhaseProgramAccessor;
-
         private TermIdent passiveVarContext;
         private IProgramAccessor programAccessor;
         private IVariableTranslation<Variable> varTranslation;
@@ -60,7 +58,6 @@ public IEnumerable<OuterDecl> EndToEndProof(
             string entryCfgLemma,
             string boogieToVcLemma,
             Term vcAssm,
-            IProgramAccessor beforePhaseProgramAccessor,
             IProgramAccessor programAccessor,
             IProgramAccessor passiveProgramAccessor,
             Tuple<string, string> varContextNonPassivePassive,
@@ -72,7 +69,6 @@ public IEnumerable<OuterDecl> EndToEndProof(
             this.entryCfgLemma = entryCfgLemma;
             this.boogieToVcLemma = boogieToVcLemma;
             this.vcAssm = vcAssm;
-            this.beforePhaseProgramAccessor = beforePhaseProgramAccessor;
             this.programAccessor = programAccessor;
             this.passiveProgramAccessor = passiveProgramAccessor;
             boogieContext = new BoogieContextIsa(
@@ -171,7 +167,7 @@ private List<OuterDecl> GenerateLemma()
 
             foreach (var idVar in varIds)
                 relWfProofMethods.Add(
-                    ProofUtil.Apply(ProofUtil.Simp(beforePhaseProgramAccessor.LookupVarTyLemma(idVar.Item2),
+                    ProofUtil.Apply(ProofUtil.Simp(programAccessor.LookupVarTyLemma(idVar.Item2),
                         passiveProgramAccessor.LookupVarTyLemma(idVar.Item2)))
                 );
 
@@ -444,7 +440,7 @@ private ContextElem Context()
             var multiRed = IsaBoogieTerm.RedCFGMulti(
                 BoogieContextIsa.CreateWithNewVarContext(
                     boogieContext,
-                    new TermTuple(beforePhaseProgramAccessor.ConstsAndGlobalsDecl(), beforePhaseProgramAccessor.ParamsAndLocalsDecl())
+                    new TermTuple(programAccessor.ConstsAndGlobalsDecl(), programAccessor.ParamsAndLocalsDecl())
                 ),
                 programAccessor.CfgDecl(),
                 IsaBoogieTerm.CFGConfigNode(new NatConst(cfg.GetUniqueIntLabel(cfg.entry)),

diff --git a/Source/ProofGeneration/Passification/PassificationLemmaManager.cs b/Source/ProofGeneration/Passification/PassificationLemmaManager.cs
@@ -29,7 +29,7 @@ internal class PassificationLemmaManager
 
         private readonly TermIdent normalInitState = IsaCommonTerms.TermIdentFromName("n_s");
 
-        private readonly OldVarFinder oldVarFinder = new OldVarFinder();
+        private readonly OldVarFinder oldVarFinder = new();
         private readonly IDictionary<Block, Block> origToPassiveBlock;
         private readonly IProgramAccessor passiveProgramAccessor;
 
@@ -38,7 +38,6 @@ internal class PassificationLemmaManager
         private readonly IVariableTranslation<Variable> passiveVarTranslation;
 
         private readonly IProgramAccessor programAccessor;
-        private readonly IProgramAccessor beforePhaseProgramAccessor;
 
         private readonly Dictionary<Block, int> smallestRequiredVersionDict = new Dictionary<Block, int>();
         private readonly TermIdent stateRel = IsaCommonTerms.TermIdentFromName("R");
@@ -50,7 +49,6 @@ internal class PassificationLemmaManager
         public PassificationLemmaManager(
             CFGRepr cfg,
             IDictionary<Block, Block> origToPassiveBlock,
-            IProgramAccessor beforePhaseProgramAccessor,
             IProgramAccessor programAccessor,
             IProgramAccessor passiveProgramAccessor,
             Tuple<string, string> varContextNonPassivePassive,
@@ -61,7 +59,6 @@ public PassificationLemmaManager(
         {
             this.cfg = cfg;
             this.origToPassiveBlock = origToPassiveBlock;
-            this.beforePhaseProgramAccessor = beforePhaseProgramAccessor;
             this.programAccessor = programAccessor;
             this.passiveProgramAccessor = passiveProgramAccessor;
             _oldStateRelationData = oldStateRelationData;
@@ -116,7 +113,7 @@ public Tuple<LemmaDecl, LemmaDecl> GenerateBlockLemma(Block block, string localL
                              * in which case the variable is not newly constrained */
                             if (!tuple.Item3) constrainedPassiveVars.Add(passiveVarTerm);
                             lookupTyUpdatesLemmas.Add(
-                                Tuple.Create(beforePhaseProgramAccessor.LookupVarTyLemma(origVar),
+                                Tuple.Create(programAccessor.LookupVarTyLemma(origVar),
                                     passiveProgramAccessor.LookupVarTyLemma(passiveVar))
                             );
                         }

diff --git a/Source/ProofGeneration/Passification/PassificationManager.cs b/Source/ProofGeneration/Passification/PassificationManager.cs
@@ -34,7 +34,6 @@ public static Theory PassificationProof(
             CFGRepr beforePassificationCfg,
             IDictionary<Block, Block> nonPassiveToPassiveBlock,
             PassiveRelationGen relationGen,
-            IProgramAccessor beforePhaseProgramAccess,
             IProgramAccessor beforePassiveProgAccess,
             IProgramAccessor passiveProgAccess,
             BoogieMethodData beforePassiveData,
@@ -63,7 +62,6 @@ public static Theory PassificationProof(
             var beforePassiveLemmaManager = new PassificationLemmaManager(
                 beforePassificationCfg,
                 nonPassiveToPassiveBlock,
-                beforePhaseProgramAccess,
                 beforePassiveProgAccess,
                 passiveProgAccess,
                 varContextNonPassivePassive,
@@ -77,7 +75,7 @@ public static Theory PassificationProof(
 
             var varContextAbbrev = new AbbreviationDecl(
                 varContextName,
-                new Tuple<IList<Term>, Term>(new List<Term>(), beforePhaseProgramAccess.VarContext())
+                new Tuple<IList<Term>, Term>(new List<Term>(), beforePassiveProgAccess.VarContext())
             );
 
             var passiveVarContextAbbrev = new AbbreviationDecl(
@@ -120,7 +118,6 @@ relation used to construct the initial passive state set in the end-to-end proof
                     GetCfgLemmaName(beforePassificationCfg.entry, lemmaNamer),
                     boogieToVcTheoryName + "." + boogieToVcLemma.Name,
                     vcAssm,
-                    beforePhaseProgramAccess,
                     beforePassiveProgAccess,
                     passiveProgAccess,
                     varContextNonPassivePassive,
@@ -133,7 +130,7 @@ relation used to construct the initial passive state set in the end-to-end proof
 
             var imports = new List<string>
             {
-                "Boogie_Lang.Semantics", "Boogie_Lang.Util", beforePhaseProgramAccess.TheoryName(),
+                "Boogie_Lang.Semantics", "Boogie_Lang.Util", beforePassiveProgAccess.TheoryName(),
                 passiveProgAccess.TheoryName(), "Boogie_Lang.PassificationML",
                 boogieToVcTheoryName
             };

diff --git a/Source/ProofGeneration/ProofGenerationLayer.cs b/Source/ProofGeneration/ProofGenerationLayer.cs
@@ -745,9 +745,9 @@ from calls.
                 false, 
                 false, 
                 false, 
-                proofGenInfo.GetOptimizationsFlag(), 
+                parentAccessorForBeforeCfgToDag == null || proofGenInfo.GetOptimizationsFlag(), 
                 parentAccessorForBeforeCfgToDag != null ? SpecsConfig.None : specsConfigDefault, 
-                proofGenInfo.GetOptimizationsFlag());
+                parentAccessorForBeforeCfgToDag == null || proofGenInfo.GetOptimizationsFlag());
 
               beforeCfgToDagProgAccess = new IsaProgramGenerator().GetIsaProgram(
                 beforeCfgToDagTheoryName,
@@ -789,7 +789,7 @@ from calls.
                   false, 
                   parentProgramAccessorForPassification == null,
                   parentProgramAccessorForPassification != null ? SpecsConfig.None : specsConfigDefault, 
-                  false);
+                  parentProgramAccessorForPassification == null);
               beforePassiveProgAccess = new IsaProgramGenerator().GetIsaProgram(beforePassiveProgTheoryName,
                 afterPassificationImpl.Name,
                 afterOptimizationsData, beforePassiveConfig, afterOptimizationsVarTranslationFactory,