From f8d0fb8931ae57a306ef434d26bc48d2bab7f149 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Tue, 21 Aug 2018 15:05:22 +0100 Subject: [PATCH] Add overview of constant propagator --- src/analyses/README.md | 7 +++++-- src/analyses/constant_propagator.h | 10 ++++++++++ 2 files changed, 15 insertions(+), 2 deletions(-) diff --git a/src/analyses/README.md b/src/analyses/README.md index f3ecd34a976..132751b985a 100644 --- a/src/analyses/README.md +++ b/src/analyses/README.md @@ -30,9 +30,12 @@ To be documented. To be documented. -\subsection analyses-constant-propagation Constant propagation (constant_propagator_ait) +\subsection analyses-constant-propagation Constant propagation (\ref constant_propagator_ait) -To be documented. +A simple, unsound constant propagator. Replaces RHS symbol expressions (variable +reads) with their values when they appear to have a unique value at a particular +program point. Unsound with respect to pointer operations on the left-hand side +of assignments. \subsection analyses-taint Taint analysis (custom_bitvector_analysist) diff --git a/src/analyses/constant_propagator.h b/src/analyses/constant_propagator.h index 80a3579fcf8..63e285785c1 100644 --- a/src/analyses/constant_propagator.h +++ b/src/analyses/constant_propagator.h @@ -8,6 +8,16 @@ Author: Peter Schrammel /// \file /// Constant propagation +/// +/// A simple, unsound constant propagator. Assignments to symbols (local and +/// global variables) are tracked, and propagated if a unique value is found +/// at a given use site. Function calls are accounted for (they are assumed to +/// overwrite all address-taken variables; see \ref dirtyt), but assignments +/// through pointers are not (they are assumed to have no effect). +/// +/// Can be restricted to operate over only particular symbols by passing a +/// predicate to a \ref constant_propagator_ait constructor, in which case this +/// can be rendered sound by restricting it to non-address-taken variables. #ifndef CPROVER_ANALYSES_CONSTANT_PROPAGATOR_H #define CPROVER_ANALYSES_CONSTANT_PROPAGATOR_H