Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Control flow graphs and code coverage

Hello,

For my short answer to the questions is as follows:

> On Jan 17, 2016, at 9:19 AM, SF Markus Elfring <elfring at users.sourceforge.net> wrote:
> 
> Am 16.01.2016 um 21:20 schrieb Chan Ngo:
>> Hello,
>> 
>>> On Jan 16, 2016, at 8:22 PM, SF Markus Elfring <elfring at users.sourceforge.net> wrote:
>>> 
>>> Hello,
>>> 
>>> I have read the user manual for your evolving software. Now I would like to
>>> find a bit more out from technology areas which are involved here.
>>> 
>>> * Would you like to share any more information about the use of advanced
>>> control flow graphs?
>>> 
>>> * Do extended versions get any special names?
>>> 
>>> * How can the amount of source code which is used between statements
>>> like "goto" (in the C programming language) be modelled by such
>>> a software design approach?
>>> 
>>> Use case:
>>> Do you try to improve capabilities for static source analysis in the way
>>> that issues which are similar to the description of consequences from
>>> a special "goto fail;" in the article "An interesting SSL implementation bug"
>>> can be better detected?
>>> http://blog.frama-c.com/index.php?post/2014/02/23/CVE-2013-5914
>>> 
>>> * Do you know any plug-ins (or add-ons) which collaborate with related
>>> software tools?
>>> 
>> For the use of “go to” statement in C, in critical software development,
>> the convention is that, programers cannot use “go to” statement.
> 
> The are some software design difficulties and challenges to consider also
> for this special statement.
> A few coding style documents recommend its reuse to make software implementations
> even more robust eventually.
> 
> Example "Chapter 7: Centralized exiting of functions":
> https://git.kernel.org/cgit/linux/kernel/git/torvalds/linux.git/tree/Documentation/CodingStyle?id=4b10df7f2c8b3c6de12375b85456c6fd275af6d0#n389
> 
> 
>> In principle, it is detected by building the control flow graph (CFG)
>> of the program and see the dead code fragment.
> 
> Do you know any extensions for such a data structure which are developed
> during software research activities?
> 
> 
>> For example, the “goto fail” bug, the problem with the code of Apple’s
>> sslKeyExchange.c source file is that there are two repeated “goto” statements
>> and under some circumstances the seconde “goto” will be triggered,
>> then the return error code “err” is zero, meaning that the code after
>> the second “goto” is unreachable, dead code.
> 
> This issue got some attention for a while.
> 
> 
> I became interested to clarify details which are also shown here a bit more.
> 
> 1. How do you think about consequences from the selection of popular
>   short identifiers in a programming language like "C"?
> 
>   * Does the identifier length indicate anything?
> 
>   * Will it help to reuse logograms and ideograms there from the evolving
>     support for the Unicode standard?
> 
>   * Does a bit of psychology matter for safer communication and the evolution
>     of thinking processes here?
>     Is it occasionally nicer to specify "go to success" instead of stressing
>     the possibility for failure around such jump labels and status variables?
> 
> 2. Is another search pattern variant interesting here?
> 
>   * Would you like to look at the amount of source code which is used in the
>     control flow between statements like "goto"?
> 
>   * How often will the determination matter for optimisation approaches
>     if a branch or code path is "empty" (or contains only comments together
>     with additional white-space characters)?
> 
> 
>> Any static analyzer provides a function to give the CFG of a program.
> 
> Do you suggest the reuse of any standard data formats for advanced
> software analysis?
> 
> How many progress do you see in the development of plug-ins (or add-ons)?
> 

I prefer to recommend you read some lecture notes or tutorial on static analysis. For example, the following is a quite good one
http://www.itu.dk/people/brabrand/UFPE/Data-Flow-Analysis/static.pdf <http://www.itu.dk/people/brabrand/UFPE/Data-Flow-Analysis/static.pdf>
If you want to look at how its data structures and algorithms to implement it, you can read some chapters about lexing, parsing, abstract syntax tree, and data flow analysis in the “Modern compiler implementation” (in Java, C, or ML) book by Andrew Appel.

> 
>> Roundly speaking, CFG is the essential input for all analysis including
>> value analysis, pointer analysis, … (called data flow analysis)
> 
> Are there any relationships to a technology like computation tree logic?
> 

CTL and/or LTL are temporal logics which are used mostly in a verification technique called “Model Checking”. The principle is that you construct software or system design as a state system (label transition system - LTS) and you express desired temporal property in LTL or CTL (i.e., if request is sent, it implies that eventually in future, the acknowledge message is received). Thus, to automatically generate a state system from C program for example, one  needs the CFG of the C program. For more information, you can refer to some model checking tools like SPIN, SMV,...

In my opinion, static analysis and model checking can be classified as two categories of formal methods as follows:
Static analyses analyze directly and without user intervention the source code at some level of abstraction. Thus, they can make some false positive alarms but never false negative (programs reported as correct indeed correct despite the approximation);

Model checking explores exhaustively and automatically finite models of programs. It may require user intervention beforehand to abstract programs with an infinite or large state space into such models;

Theorem proving employ proof assistants or theorem provers. They rely on the user to provide the inductive invariants needed in the proof. 

Best,

---
Chan Ngo
INRIA,
(+33)02 99 84 72 84
chan.ngo at inria.fr
http://people.rennes.inria.fr/Chan.Ngo

> Regards,
> Markus

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20160117/4007c43a/attachment.html>