From 67c4d65e74918b7903d931ae7438cf1895e24d9c Mon Sep 17 00:00:00 2001 From: gauravpartha Date: Tue, 9 May 2023 19:42:56 +0200 Subject: [PATCH] fix and get rid of more accessors other than the two that are required for a phase --- .../Passification/PassificationEndToEnd.cs | 8 ++------ .../Passification/PassificationLemmaManager.cs | 7 ++----- .../ProofGeneration/Passification/PassificationManager.cs | 7 ++----- Source/ProofGeneration/ProofGenerationLayer.cs | 6 +++--- 4 files changed, 9 insertions(+), 19 deletions(-) diff --git a/Source/ProofGeneration/Passification/PassificationEndToEnd.cs b/Source/ProofGeneration/Passification/PassificationEndToEnd.cs index 295c9360..630d9556 100644 --- 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 varTranslation; @@ -60,7 +58,6 @@ public IEnumerable EndToEndProof( string entryCfgLemma, string boogieToVcLemma, Term vcAssm, - IProgramAccessor beforePhaseProgramAccessor, IProgramAccessor programAccessor, IProgramAccessor passiveProgramAccessor, Tuple varContextNonPassivePassive, @@ -72,7 +69,6 @@ public IEnumerable 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 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 index c5d7021c..defcf34d 100644 --- 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 origToPassiveBlock; private readonly IProgramAccessor passiveProgramAccessor; @@ -38,7 +38,6 @@ internal class PassificationLemmaManager private readonly IVariableTranslation passiveVarTranslation; private readonly IProgramAccessor programAccessor; - private readonly IProgramAccessor beforePhaseProgramAccessor; private readonly Dictionary smallestRequiredVersionDict = new Dictionary(); private readonly TermIdent stateRel = IsaCommonTerms.TermIdentFromName("R"); @@ -50,7 +49,6 @@ internal class PassificationLemmaManager public PassificationLemmaManager( CFGRepr cfg, IDictionary origToPassiveBlock, - IProgramAccessor beforePhaseProgramAccessor, IProgramAccessor programAccessor, IProgramAccessor passiveProgramAccessor, Tuple 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 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 index a31c640f..006d36da 100644 --- a/Source/ProofGeneration/Passification/PassificationManager.cs +++ b/Source/ProofGeneration/Passification/PassificationManager.cs @@ -34,7 +34,6 @@ public static Theory PassificationProof( CFGRepr beforePassificationCfg, IDictionary 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, Term>(new List(), beforePhaseProgramAccess.VarContext()) + new Tuple, Term>(new List(), 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 { - "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 index 546d5be1..f6fb694e 100644 --- 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,