Polynomial Constants are Decidable

Constant propagation aims at identifying expressions that always yield a unique constant value at run-time. It is well-known that constant propagation is undecidable for programs working on integers even if guards are ignored as in non-deterministic flow graphs. We show that polynomial constants are decidable in non-deterministic flow graphs. In polynomial constant propagation, assignment statements that use the operators +, -, are interpreted exactly but all assignments that use other operators are conservatively interpreted as non-deterministic assignments. We present a generic algorithm for constant propagation via a symbolic weakest precondition computation and show how this generic algorithm can be instantiated for polynomial constant propagation by exploiting techniques from computable ring theory.

• Type: Journal
• Year: 2002
• Where: TRIER
• Authors: Markus Müller-Olm, Helmut Seidl
• Keywords: Constant Propagation, Modeling And Simulation, Non-deterministic Flow Graphs, Polynomial Constant, TRIER 2002