From 2675090c8f92fce162ac7ef7abe7d68e6e6ce49b Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Tue, 21 Aug 2018 14:09:37 +0100 Subject: [PATCH] Add documentation for object numbering --- src/pointer-analysis/README.md | 17 +++++++++++++++-- src/pointer-analysis/object_numbering.h | 14 ++++++++++++-- 2 files changed, 27 insertions(+), 4 deletions(-) diff --git a/src/pointer-analysis/README.md b/src/pointer-analysis/README.md index 5fd38dcc4af..9482b9e1810 100644 --- a/src/pointer-analysis/README.md +++ b/src/pointer-analysis/README.md @@ -3,7 +3,7 @@ # Folder pointer-analysis -\author Martin Brain +\author Martin Brain, Chris Smowton To perform symbolic execution on programs with dereferencing of arbitrary pointers, some alias analysis is needed. `pointer-analysis` @@ -15,7 +15,20 @@ subtle and sophisticated and thus there may be bugs. \subsection pointer-analysis-object-numbering Object / expression numbering (object_numberingt) -To be documented. +Object numbering assigns numbers to expressions, allowing other pointer-analysis +classes to use small, cheap to compare, cheap to sort numbers in place of +\ref exprt instances. Numbering also saves memory, as two identical exprt +objects will be assigned the same number, eliminating redundant storage of the +same data. + +Alternative approaches to the same problem include \ref irept sharing (but this +only shares when a copy is taken; two identical irepts arrived at by different +routes will not be shared) and \ref merge_irept (which does merge identical +ireps, but is still more expensive to compare than numbers). + +Object numbering is used by \ref value_sett and cousins (such as +\ref value_set_fit) in an effort to reduce the memory dedicated to value-set +storage. \subsection pointer-analysis-pointer-offset-sum Pointer-offset sum (pointer_offset_sum) diff --git a/src/pointer-analysis/object_numbering.h b/src/pointer-analysis/object_numbering.h index 6e731bd072c..4e51a68f8fc 100644 --- a/src/pointer-analysis/object_numbering.h +++ b/src/pointer-analysis/object_numbering.h @@ -1,13 +1,23 @@ /*******************************************************************\ -Module: Value Set +Module: Object Numbering Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ /// \file -/// Value Set +/// Object Numbering +/// +/// This is used to abbreviate identical expressions by number: for example, +/// an object_numberingt instance might maintain the map: +/// ``` +/// 1 -> constant_exprt("Hello", string_typet()) +/// 2 -> constant_exprt("World", string_typet()) +/// ``` +/// Then any users that agree to use the same object_numberingt instance as a +/// common reference source can use '1' and '2' as shorthands for "Hello" and +/// "World" respectively. #ifndef CPROVER_POINTER_ANALYSIS_OBJECT_NUMBERING_H #define CPROVER_POINTER_ANALYSIS_OBJECT_NUMBERING_H