<br><br><div class="gmail_quote">On Fri, Nov 7, 2008 at 4:05 PM, Ted Kremenek <span dir="ltr"><<a href="mailto:kremenek@apple.com">kremenek@apple.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
<div class="Ih2E3d"><br>
On Nov 6, 2008, at 11:54 PM, Zhongxing Xu wrote:<br>
<br>
<blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
Perhaps, but I think all the logic can be divided between the StoreManager and GRExprEngine.  The StoreManager is responsible for reasoning about what is valid memory, and GRExprEngine handles loads/stores.<br>
<br>
This job splitting is OK for me. But does it violates the rule that 'StoreManager does no reasoning'?<br>
<br>
</blockquote>
<br></div>
By "reasoning", I mean "reasoning about extents".<br>
<br>
Perhaps we should talk more about what the requirements would be for an out-of-bounds checker before deciding where its implementation pieces should be.<br>
<br>
>From what I can tell, an out-of-bounds check has three components:<br>
<br>
(1) a location L, which is an offset within a region X<br>
(2) the extent of region X<br>
(3) some logic to determine if the location L is outside the extent of region X<br>
<br>
We need to decide if we currently represent (1) for the interesting cases that we are initially interested in going after.  </blockquote><div><br>I have some difficulty to understand this sentence. I think a we will just get a location MemRegionVal with a out-of-bound ElementRegion, returned by getLValue(). And nobody is aware of its illegality at that time.<br>
 </div><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">Right now locations are modeled using SVals.<br>
<br>
I think the consensus is that (2) is managed by StoreManager.<br>
<br>
For (3), we need to decide where this decision logic would go.  My guess was GRExprEngine, which would issue a series of "Assume" calls to the ConstraintManager to determine if the offset of L exceeded the extent X.  I'm not sure exactly what that would look like.<br>

</blockquote></div><br>I'll try to scratch an implementation to see what indeed we need.<br>