@@ -10,20 +10,102 @@ use constant_value::ConstantValue;
1010/// A collection of abstract domains associated with a particular abstract value.
1111/// The expression domain captures the precise expression that resulted in the abstract
1212/// value. It can be used to derive any other kind of abstract domain on demand.
13- #[ derive( Serialize , Deserialize , Debug , Eq , PartialEq , Hash ) ]
13+ #[ derive( Serialize , Deserialize , Clone , Debug , Eq , PartialEq , Hash ) ]
1414pub struct AbstractDomains {
1515 pub expression_domain : ExpressionDomain ,
1616 //todo: use cached getters to get other domains on demand
1717}
1818
19- /// The things all abstract domain instances have to be able to do
19+ /// A collection of abstract domains that all represent the impossible abstract value.
20+ /// I.e. the corresponding set of possible concrete values is empty.
21+ pub const BOTTOM : AbstractDomains = AbstractDomains {
22+ expression_domain : ExpressionDomain :: Bottom ,
23+ } ;
24+
25+ /// A collection of abstract domains that all represent the universal abstract value.
26+ /// I.e. the corresponding set of possible concrete values includes every possible concrete value.
27+ pub const TOP : AbstractDomains = AbstractDomains {
28+ expression_domain : ExpressionDomain :: Top ,
29+ } ;
30+
31+ impl AbstractDomains {
32+ /// True if all of the abstract domains in this collection correspond to an empty set of concrete values.
33+ pub fn is_bottom ( & self ) -> bool {
34+ self . expression_domain . is_bottom ( )
35+ }
36+
37+ /// True if all of the abstract domains in this collection correspond to the set of all possible concrete values.
38+ pub fn is_top ( & self ) -> bool {
39+ self . expression_domain . is_top ( )
40+ }
41+
42+ /// Joins all of the abstract domains in the two collections to form a single collection.
43+ /// In a context where the join condition is known to be true, the result can be refined to be
44+ /// just self, correspondingly if it is known to be false, the result can be refined to be just other.
45+ pub fn join (
46+ & self ,
47+ other : & AbstractDomains ,
48+ join_condition : & AbstractDomains ,
49+ ) -> AbstractDomains {
50+ AbstractDomains {
51+ expression_domain : self
52+ . expression_domain
53+ . join ( & other. expression_domain , & join_condition) ,
54+ }
55+ }
56+
57+ /// Widen all of the abstract domains in the two collections to form a single collection.
58+ /// The join condition is supplied to inform the widen operation, but the result is not
59+ /// required to be in a form that can be refined using the join condition.
60+ pub fn widen (
61+ & self ,
62+ other : & AbstractDomains ,
63+ join_condition : & AbstractDomains ,
64+ ) -> AbstractDomains {
65+ AbstractDomains {
66+ expression_domain : self
67+ . expression_domain
68+ . widen ( & other. expression_domain , & join_condition) ,
69+ }
70+ }
71+
72+ /// True if for each abstract domains in the self collection, all of its concrete values are
73+ /// elements of the corresponding set of the same domain in other.
74+ pub fn subset ( & self , other : & AbstractDomains ) -> bool {
75+ self . expression_domain . subset ( & other. expression_domain )
76+ }
77+ }
78+
79+ /// An abstract domain defines a set of concrete values in some way.
2080pub trait AbstractDomain {
21- //todo: join, is_top, is_bottom, etc.
81+ /// True if the set of concrete values that correspond to this domain is empty.
82+ fn is_bottom ( & self ) -> bool ;
83+
84+ /// True if all possible concrete values are elements of the set corresponding to this domain.
85+ fn is_top ( & self ) -> bool ;
86+
87+ /// Returns a domain whose corresponding set of concrete values include all of the values
88+ /// corresponding to self and other.
89+ /// In a context where the join condition is known to be true, the result can be refined to be
90+ /// just self, correspondingly if it is known to be false, the result can be refined to be just other.
91+ fn join ( & self , other : & Self , join_condition : & AbstractDomains ) -> Self ;
92+
93+ /// True if all of the concrete values that correspond to self also correspond to other.
94+ fn subset ( & self , other : & Self ) -> bool ;
95+
96+ /// Returns a domain whose corresponding set of concrete values include all of the values
97+ /// corresponding to self and other.The set of values may be less precise (more inclusive) than
98+ /// the set returned by join. The chief requirement is that a small number of widen calls
99+ /// deterministically lead to Top.
100+ fn widen ( & self , other : & Self , join_condition : & AbstractDomains ) -> Self ;
22101}
23102
24- /// An abstract domain uses a functional (side effect free) expression that precisely tracks
103+ /// An abstract domain that uses a functional (side effect free) expression that precisely tracks
25104/// a single value.
26- #[ derive( Serialize , Deserialize , Debug , Eq , PartialEq , Hash ) ]
105+ /// Note: that value might not be known at compile time, so some operations on the domain
106+ /// may conservatively expand the set of of values that correspond to the domain to more than
107+ /// just one element.
108+ #[ derive( Serialize , Deserialize , Clone , Debug , Eq , PartialEq , Hash ) ]
27109pub enum ExpressionDomain {
28110 /// An expression that represents any possible value
29111Top ,
@@ -32,9 +114,97 @@ pub enum ExpressionDomain {
32114/// that always panics.
33115Bottom ,
34116
35- /// An expression that is a compile time constant value, such as a numeric literal or a
36- /// function.
117+ /// An expression that is a compile time constant value, such as a numeric literal or a function.
37118CompileTimeConstant ( ConstantValue ) ,
119+
120+ /// An expression that is either if_true or if_false, depending on the value of condition.
121+ ConditionalExpression {
122+ // A condition that results in a Boolean value
123+ condition : Box < AbstractDomains > ,
124+ // The value of this expression if join_condition is true.
125+ consequent : Box < ExpressionDomain > ,
126+ // The value of this expression if join_condition is false.
127+ alternate : Box < ExpressionDomain > ,
128+ } ,
38129}
39130
40- // todo: implement the AbstractDomain trait for ExpressionDomain
131+ impl AbstractDomain for ExpressionDomain {
132+ /// True if the set of concrete values that correspond to this domain is empty.
133+ fn is_bottom ( & self ) -> bool {
134+ match self {
135+ ExpressionDomain :: Bottom => true ,
136+ _ => false ,
137+ }
138+ }
139+
140+ /// True if all possible concrete values are elements of the set corresponding to this domain.
141+ fn is_top ( & self ) -> bool {
142+ match self {
143+ ExpressionDomain :: Top => true ,
144+ _ => false ,
145+ }
146+ }
147+
148+ /// Returns a domain whose corresponding set of concrete values include all of the values
149+ /// corresponding to self and other.
150+ /// In a context where the join condition is known to be true, the result can be refined to be
151+ /// just self, correspondingly if it is known to be false, the result can be refined to be just other.
152+ fn join ( & self , other : & ExpressionDomain , join_condition : & AbstractDomains ) -> ExpressionDomain {
153+ ExpressionDomain :: ConditionalExpression {
154+ condition : box join_condition. clone ( ) ,
155+ consequent : box self . clone ( ) ,
156+ alternate : box other. clone ( ) ,
157+ }
158+ }
159+
160+ /// True if all of the concrete values that correspond to self also correspond to other.
161+ /// Note: !x.subset(y) does not imply y.subset(x).
162+ fn subset ( & self , other : & ExpressionDomain ) -> bool {
163+ match ( self , other) {
164+ // The empty set is a subset of every other set.
165+ ( ExpressionDomain :: Bottom , _) => true ,
166+ // A non empty set is not a subset of the empty set.
167+ ( _, ExpressionDomain :: Bottom ) => false ,
168+ // Every set is a subset of the universal set.
169+ ( _, ExpressionDomain :: Top ) => true ,
170+ // The universal set is not a subset of any set other than the universal set.
171+ ( ExpressionDomain :: Top , _) => false ,
172+ (
173+ ExpressionDomain :: ConditionalExpression {
174+ consequent,
175+ alternate,
176+ ..
177+ } ,
178+ _,
179+ ) => {
180+ // This is a conservative answer. False does not imply other.subset(self).
181+ consequent. subset ( other) && alternate. subset ( other)
182+ }
183+ (
184+ _,
185+ ExpressionDomain :: ConditionalExpression {
186+ consequent,
187+ alternate,
188+ ..
189+ } ,
190+ ) => {
191+ // This is a conservative answer. False does not imply other.subset(self).
192+ self . subset ( consequent) || self . subset ( alternate)
193+ }
194+ // {x} subset {y} iff x = y
195+ (
196+ ExpressionDomain :: CompileTimeConstant ( cv1) ,
197+ ExpressionDomain :: CompileTimeConstant ( cv2) ,
198+ ) => cv1 == cv2,
199+ }
200+ }
201+
202+ /// Returns a domain whose corresponding set of concrete values include all of the values
203+ /// corresponding to self and other.The set of values may be less precise (more inclusive) than
204+ /// the set returned by join. The chief requirement is that a small number of widen calls
205+ /// deterministically lead to Top.
206+ fn widen ( & self , _other : & Self , _join_condition : & AbstractDomains ) -> ExpressionDomain {
207+ //todo: don't get to top quite this quickly.
208+ ExpressionDomain :: Top
209+ }
210+ }
0 commit comments