Cfg optimizations (unreachable blocks and block coalescing)#8

Merged

gauravpartha merged 87 commits intomasterfrom

cfg_optimizations

Dec 19, 2024

Commits on Mar 10, 2022

first draft of ast formalization
ahubanov-eth2
committed

Commits on Mar 13, 2022

changed to small-step semantics, added a find_label function and added goto reduction (which needs to be checked again)
ahubanov-eth2
committed

Commits on Mar 14, 2022

Commits on Mar 17, 2022

added invariants, fixed while_loop rule
ahubanov-eth2
committed

Commits on Mar 23, 2022

minor syntactic tweaks + comments
ahubanov-eth2
committed

Commits on Mar 24, 2022

added Failure and Magic rule + invariants
ahubanov-eth2
committed

Commits on Mar 30, 2022

added definitions for correctness of AST
ahubanov-eth2
committed

Commits on Apr 2, 2022

added an ast-to-cfg relation function (doesn't work for breaks and gotos)
ahubanov-eth2
committed

Commits on Apr 5, 2022

refactored the code
ahubanov-eth2
committed

Commits on Apr 22, 2022

latest version of ast.thy
ahubanov-eth2
committed

Commits on Apr 28, 2022

saving before making some changes
ahubanov-eth2
committed

Commits on May 15, 2022

first draft of lemmas and proofs for the ast_cfg_phase
ahubanov-eth2
committed

Commits on May 22, 2022

cleaned proofs + nested loop example done
ahubanov-eth2
committed

Commits on Jun 1, 2022

annotated Ast_Cfg_Transformation.thy
ahubanov-eth2
committed

Commits on Jun 2, 2022

fixed most of the concrete proofs + minor changes
ahubanov-eth2
committed

Commits on Jun 3, 2022

changed nested loop2
ahubanov-eth2
committed

Commits on Jun 26, 2022

changed the definition of a procedure and of proc_is_correct
ahubanov-eth2
committed

Commits on Jul 20, 2022

latest version
ahubanov-eth2
committed

Commits on Aug 29, 2022

Commits on Oct 6, 2022

resolving some pull request comments + a few smts removed
ahubanov-eth2
committed

Commits on Oct 10, 2022

Commits on Oct 11, 2022

decoupled the procedure type parameter from the proc_context type parameter
ahubanov-eth2
committed

Commits on Nov 10, 2022

minor
gauravpartha
committed

Commits on Nov 19, 2022

removed rev for AST and AST_CFG_Transformation
ahubanov-eth2
committed

Commits on Jan 10, 2023

fix bug in goto semantics
gauravpartha
committed

Commits on Jan 11, 2023

Merge branch 'master' into ast
gauravpartha
committed

Commits on Jan 15, 2023

Merge branch 'master' into ast
gauravpartha
committed

Commits on Apr 20, 2023

Create CfgOptimizations.thy
lukashimmelreich
committed

Commits on May 10, 2023

Update CfgOptimizations.thy
lukashimmelreich
committed

Commits on May 31, 2023

Create CfgOptimizationsLoop.thy
lukashimmelreich
committed
Update CfgOptimizations.thy
lukashimmelreich
committed

Commits on Jun 14, 2023

Change File Name CFGOptimizations
lukashimmelreich
committed

Commits on Jun 15, 2023

Fix Main Lemma 4 (Wrong assumption)
lukashimmelreich
committed

Commits on Jun 21, 2023

New Document for Dead Variables Elimination
lukashimmelreich
committed

Commits on Jun 26, 2023

Changed Definition of Global Block and Hybrid Block Lemma
lukashimmelreich
committed

Commits on Jun 29, 2023

Edited assumptions of Lemmas and changed the proof accordingly
lukashimmelreich
committed

Commits on Jul 2, 2023

Changed Hybrid Block Lemma to get rid of the last sorry statements
lukashimmelreich
committed

Commits on Jul 5, 2023

Changed sorry statements dead variables elimination
lukashimmelreich
committed

Commits on Jul 9, 2023

Commits on Jul 10, 2023

Sorry statements conditional expressions
lukashimmelreich
committed

Commits on Jul 11, 2023

Removed sorry statement
lukashimmelreich
committed
add CFGOptimizationsLoop
gauravpartha
committed

Commits on Jul 12, 2023

Changed Pruning of Unreachable Blocks Lemma
lukashimmelreich
committed
Merge branch 'cfg_optimizations' of https://github.com/gauravpartha/foundational_boogie into cfg_optimizations
lukashimmelreich
committed

Commits on Jul 18, 2023

minor
gauravpartha
committed

Commits on Oct 21, 2023

Commits on Oct 30, 2023

Commits on Oct 31, 2023

Commits on Nov 16, 2023

Commits on Dec 5, 2023

Commits on Feb 10, 2024

Merge remote-tracking branch 'origin/adjust_interface' into cfg_optimizations
gauravpartha
committed

Commits on Apr 25, 2024

allow WhileWrapper around any control-flow construct in AST semantics
gauravpartha
committed

Commits on Aug 21, 2024

add helper lemma for proof generation of CFG optimizations
gauravpartha
committed

Commits on Nov 21, 2024

Updated files to work with Isabelle 2023

tdardinier
authored and
gauravpartha
committed

Commits on Dec 8, 2024

Update README.md
gauravpartha
authored