Boogie Verifier instrumentation for generating AST-to-CFG validation certificates #4

ahubanov-eth2 · 2022-08-29T09:14:58Z

ObjectExtensions.cs file in the Core module is redundant, added reference to ProofGenUtil from Core.

copying of unoptimized blocks to be done

…enerated

gauravpartha · 2022-09-16T10:09:25Z

There seems to be often lots of redundant white space in the generated proofs. For example

gauravpartha · 2022-09-18T14:29:51Z

It would be good to add comments to the newly added code such that it is easier to understand the code. Moreover, the parts where big blocks are added for the purpose of proof generation should be documented clearly.

gauravpartha · 2022-09-18T13:39:37Z

Source/Core/ObjectExtensions.cs

+
+namespace Core
+{
+    public static class ObjectExtensions


This file is duplicated (also in ProofGenUtil). It should be possible to keep this file only once, since there are no dependencies from this file to the Boogie code.

gauravpartha · 2022-09-18T13:41:33Z

Source/Core/ProofGenInfoManager.cs

+      /*
+      if (mapFromImplementationToProofGenInfo == null)
+      {
+        mapFromImplementationToProofGenInfo = new Dictionary<Implementation, ProofGenInfo>();
+      }
+
+      return mapFromImplementationToProofGenInfo;
+      */


should this be removed?

gauravpartha · 2022-09-18T13:44:16Z

Source/Core/Parser.cs

-			impl = new Implementation(x, x.val, typeParams.ConvertAll(tp => new TypeVariable(tp.tok, tp.Name)),
+      impl = new Implementation(x, x.val, typeParams.ConvertAll(tp => new TypeVariable(tp.tok, tp.Name)),


It seems like there is no change here. It would be good to keep the old formatting so that no change is displayed.

gauravpartha · 2022-09-18T13:44:27Z

Source/Core/Parser.cs

@@ -581,7 +582,7 @@ public override int ComputeHashCode()
 		Expect(35);
 		ProcSignature(false, out x, out typeParams, out ins, out outs, out kv);
 		ImplBody(out locals, out stmtList);
-		impl = new Implementation(x, x.val, typeParams, ins, outs, locals, stmtList, kv, this.errors); 
+    impl = new Implementation(x, x.val, typeParams, ins, outs, locals, stmtList, kv, this.errors); 


It seems like there is no change here. It would be good to keep the old formatting so that no change is displayed.

gauravpartha · 2022-09-18T13:45:01Z

Source/ExecutionEngine/ExecutionEngine.cs

-      CoalesceBlocks(program);
+      //CoalesceBlocks(program);


Block coalescing should be left switched on.

What impact does this have on the evaluation?

gauravpartha · 2022-09-18T14:36:07Z

Source/ProofGeneration/BoogieIsaInterface/IsaBoogieTerm.cs

@@ -484,6 +602,31 @@ public static Term RedCmdList(BoogieContextIsa boogieContext, Term cmdList, Term
                        finalCFGConfig
                    });
        }
+
+        public static Term LoopIH(BoogieContextIsa astBoogieContext, BoogieContextIsa cfgBoogieContext, Term ast, Term bigblock, Term cont, Term cfgBody, Term blockIndex, Term posts)


A more specific name than LoopIH would be useful.

gauravpartha · 2022-09-18T14:39:21Z

Source/ProofGeneration/BoogieIsaInterface/MembershipLemmaManager.cs

+        public MembershipLemmaManager(
+            IsaProgramGeneratorConfig config,
+            IsaProgramRepr isaProgramRepr,
+            IsaBigBlockInfo isaBigBlockInfo,
+            Tuple<int, int> GlobalsMaxLocalsMin,
+            IVariableTranslationFactory factory,
+            string theoryName
+        )


this constructor seems to share a lot of code with the previous one. It would be good to share that code.

gauravpartha · 2022-09-18T14:43:04Z

Source/ProofGeneration/BoogieIsaInterface/VariableTranslation/DeBruijnFixedVarTranslation.cs

+            foreach (var id in paramsAndLocalMapping.Keys)
+            {
+              if (variable.ToString() == id.ToString())
+              {
+                variable = id;
+              }
+            }


I don't understand the point of this code, it does not seem to have an effect.

gauravpartha · 2022-09-18T14:44:50Z

Source/ProofGeneration/CfgToDag/CfgToDagEndToEnd.cs

            IProgramAccessor programAccessor,
+            IProgramAccessor beforeCfgProgramAccessor,
            CFGRepr cfg)


What was the reason again for requiring two program accessors here? It would be good if you could describe the reasons why this is required.

gauravpartha · 2022-09-18T14:45:29Z

Source/ProofGeneration/CfgToDag/CfgToDagEndToEnd.cs

                //TODO: here assuming that we use "'a" for the abstract value type carrier t --> make t a parameter somewhere 
                new TermWithExplicitType(new TermIdent(typeInterpId), IsaBoogieType.AbstractValueTyFunType(new VarType("a"))),
                funDecls,
                constantDecls,
                globalDecls,
                axioms,
-                procedure));
+                procedure,
+                //TODO: define this elsewhere.


…anup, still need to run and check all examples

the previous versoin used explicit symbols, which cannot be parsed by Isabelle's command line tool

# Conflicts: # Source/ProofGeneration/BoogieIsaInterface/IsaBoogieTerm.cs

…gardless of labels

…neration of the before-phase programs

(i.e., revert Parser.cs to commit ce40e35, which was the last non-proof-generation commit for Parser.cs from the main Boogie repository)

…ram is not

…variable declarations before and after optimizations The change also adjusts the selective phase generation. In particular, one does not need to give the AstToCfg program accessor to phases that are not connected to it. This is achieved by making the AstToCfg program accessor a parent of those program accessors right below it.

…d for a phase

We should revisit the RemoveApostrophe with a different solution where terms are constructed via the AST instead of via strings.

ahubanov-eth2 added 2 commits August 10, 2022 17:28

ast_to_cfg certification in progress

e59ce53

copying of unoptimized blocks to be done

for procedures with breaks or gotos, certificate for AST-to-CFG not g…

fa64238

…enerated

ahubanov-eth2 requested a review from gauravpartha August 29, 2022 09:15

gauravpartha requested changes Sep 18, 2022

View reviewed changes

ahubanov-eth2 and others added 24 commits October 5, 2022 08:07

some pull request comments resolved

f9db316

added some comments for documentation

0b9cf72

separation of AstCfg Proofs from the rest done, needs to be checked

de72fcc

ASTtoCFG proofs separated + added booleans per phase + small code cle…

dbe99fb

…anup, still need to run and check all examples

added conditional generation of AST-to-CFG end-to-end lemma

9e50541

refactored the booleans

3bc02f2

added comment about loop head big block map

ff89f0e

use type synonym instead of explicit type for "proc_body_satisfies_spec"

030a993

the previous versoin used explicit symbols, which cannot be parsed by Isabelle's command line tool

Merge branch 'master' into ast_to_cfg

254bbab

# Conflicts: # Source/ProofGeneration/BoogieIsaInterface/IsaBoogieTerm.cs

resolved naming issues for subdirectories, omitted numbers in titles

d6bb14b

changes on proofs and naming

1bf7398

update flags to avoid generating redundant definitions

cd737c0

bigblock definitions redone and 'blast+' removed from most proofs

eb05cff

finalizing branch, proof generation for all phases enabled

88ee90f

forcing squeezing of assume commands in the beginning of if-blocks re…

153df56

…gardless of labels

small bug fix regarding naming

2d3da1f

reverted forceful squeezing of assume-commands and added condition ge…

6134eaa

…neration of the before-phase programs

selective generation of phases done

06180da

selective phase gen now done

a8c60ae

merge master into ast_to_cfg

e951e02

generate all proofs (ProofGenConfig initialization adjustments)

489c5c5

set foundational boogie commit to ast version

93df447

fix bug: initialize phaseTheories directly with unique namer

a2c98ee

remove redundant changes to Parser.cs

9a07ce2

(i.e., revert Parser.cs to commit ce40e35, which was the last non-proof-generation commit for Parser.cs from the main Boogie repository)

gauravpartha added 4 commits February 6, 2023 18:01

fix bug

2ee733a

handle case when unoptimized program is generated but AST-to-CFG prog…

6b90aef

…ram is not

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

2bb37ad

…d for a phase

gauravpartha force-pushed the ast_to_cfg branch from 67c4d65 to 2bb37ad Compare May 9, 2023 17:48

gauravpartha added 6 commits May 10, 2023 21:11

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

fdcda03

…d for a phase

added FIXME for optimization flag

741cbb4

comment out number replacement for preferred names

b5d9181

fix bug

8a27db8

add TODOs

3069bbf

get rid of RemoveApostrophe usage for axioms

9fb01eb

We should revisit the RemoveApostrophe with a different solution where terms are constructed via the AST instead of via strings.

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Boogie Verifier instrumentation for generating AST-to-CFG validation certificates #4

Boogie Verifier instrumentation for generating AST-to-CFG validation certificates #4

ahubanov-eth2 commented Aug 29, 2022 •

edited

Loading

gauravpartha commented Sep 16, 2022

gauravpartha commented Sep 18, 2022

gauravpartha Sep 18, 2022

gauravpartha Sep 18, 2022

gauravpartha Sep 18, 2022

gauravpartha Sep 18, 2022

gauravpartha Sep 18, 2022

gauravpartha Sep 18, 2022

gauravpartha Sep 18, 2022

gauravpartha Sep 18, 2022

gauravpartha Sep 18, 2022

gauravpartha Sep 18, 2022 •

edited

Loading

gauravpartha Sep 18, 2022

		impl = new Implementation(x, x.val, typeParams.ConvertAll(tp => new TypeVariable(tp.tok, tp.Name)),
		impl = new Implementation(x, x.val, typeParams.ConvertAll(tp => new TypeVariable(tp.tok, tp.Name)),

Boogie Verifier instrumentation for generating AST-to-CFG validation certificates #4

Are you sure you want to change the base?

Boogie Verifier instrumentation for generating AST-to-CFG validation certificates #4

Conversation

ahubanov-eth2 commented Aug 29, 2022 • edited Loading

gauravpartha commented Sep 16, 2022

gauravpartha commented Sep 18, 2022

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

gauravpartha Sep 18, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

ahubanov-eth2 commented Aug 29, 2022 •

edited

Loading

gauravpartha Sep 18, 2022 •

edited

Loading