Feedback Thread: DIP 1040--Copying, Moving, and Forwarding--Community Review Round 1

Timon Gehr timon.gehr at gmx.ch
Mon Mar 8 17:42:16 UTC 2021


On 08.03.21 15:01, Imperatorn wrote:
> On Monday, 8 March 2021 at 11:28:53 UTC, Timon Gehr wrote:
>> On 08.03.21 11:21, Walter Bright wrote:
>>>> [...]
>>>
>>> That's exactly how the @live analysis is currently implemented. I 
>>> didn't know it was called a fixed point analysis.
>>
>> The general framework is also called abstract interpretation, where 
>> the merge operation is called a join of abstract elements. There's 
>> also a meet operation that can introduce information from conditionals 
>> into the state. (E.g. if you want to do value range propagation this 
>> can be useful.) In general, abstract interpretation does not converge 
>> to a fixed point in finite time, then you need to introduce some sort 
>> of widening operator. In practice, this is often the main challenge to 
>> make it work.
> 
> Just curious, is there any connection here to symbolic execution?

Most program analysis is abstract interpretation in some way as it is, 
well, abstract.

You can consider symbolic execution as an abstract domain consisting of 
symbolic formulas such that the concretization function γ maps each 
symbolic formula to the set of program states that satisfy it. Possible 
choices for meet and join are symbolic conjunction and disjunction.

Then, a fully precise abstract transformer f^# is a symbolic transformer 
in the sense f[γ(φ)] = γ(f^#(φ)). If your symbolic execution does not 
fully model some aspects of the program semantics you will get the 
ordinary soundness condition f[γ(φ)] ⊆ γ(f^#(φ)).

Widening for this domain is invariant synthesis and if you do it 
(automated or manually), you get something that's getting close to 
what's usually called a program verifier instead of a static analyzer.


More information about the Digitalmars-d mailing list