Analyse sémantique et compilation pour la sécurité des environnements d'exécution (EPICURE), Centre Inria de l'Université de Rennes, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-LANGAGE ET GÉNIE LOGICIEL (IRISA-D4), Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), Institut Mines-Télécom Paris (IMT)-Institut Mines-Télécom Paris (IMT)-Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut Mines-Télécom Paris (IMT)-Institut Mines-Télécom Paris (IMT)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), Institut Mines-Télécom Paris (IMT)-Institut Mines-Télécom Paris (IMT)
Source:
Programming Languages and Systems ; ESOP 2025 - 34th European Symposium on Programming ; https://hal.science/hal-04851724 ; ESOP 2025 - 34th European Symposium on Programming, May 2025, Hamilton, Canada. pp.1-27
International audience ; In this paper, we consider specific dataflow solvers, inspired by thework of Bourdoncle, in which an iteration order ispre-computed, based on the structure of the control-flow graph ofprograms. Our work aims at a clearer formulation and a betterunderstanding of the folklore algorithms proposed three decades ago.We present a formalization of the dataflow solvers. Central to theproof of correctness is the general notion of a Weak TopologicalOrdering (WTO). Our correctness proofs are valid for any suchordering. The first solver implements an iterative strategy over theordering, the second solver implements a recursive strategy.Our formalization is done within the Coq proof assistant and oursolvers are extractable to OCaml code. Our formalization is fullycompatible with the interface of dataflow solvers of the verified,optimizing C CompCert compiler. We conduct practical experiments onthe wide range of forward and backward analyses of CompCert,demonstrating the practicality of our solvers in terms of efficiencyand precision.
