Evènement pour le groupe Modélisation et Verification

Date 2013-05-16  11:30-12:30
TitrePath Analysis in OTAWA Framework 
RésuméOTAWA (Open Tool for Adaptive WCET Analysis) is an open framework dedicated to the computation of WCET (Worst Case Execution Time). To be sound, effective and precise, this type of analysis must be performed at the machine code level that requires to decode and build back the execution paths of the program. A challenging and interesting issue of path analysis is that the embedded real-time systems, targeted by the OTAWA, exhibit a lot of different ISA (Instruction Set Architecture) like PowerPC, Sparc, ARM, TriCore, etc. As it would be a possible but a tedious and error-prone solution to implement these back-ends by hand, OTAWA re-use a well-known technology based on ADL (Architecture Description Language). Basically, ADL were developed to allow automatic and safe generation of ISS (Instruction Set Simulator) including the ability of decoding instructions from the binary code. In OTAWA, we have adapted an existing ADL generator, called GLISS, not only to get an instruction decoder but also to provide other useful information items like target of branches, used registers, type of instructions, etc. Decoding instructions is necessary to build back execution paths but we need also to get a simple and concise representation of the execution paths. CFG (Control Flow Graph) is good and common candidate: starting from the function entry points, they are build by following the instruction control flow to get edges and by grouping instruction in basic blocks to improve compactness of the representation. Yet, it remains some constructions that are hard to handle, i.e. indirect or computed branches, whose target can not be obtained by just looking to the instructions. This constructions are induced by the use of function pointers or by optimization of switch-like statements in high-level languages. The determination of the possible target of such branches requires to perform data flow analysis based on machine code and once again, the ADL have been used in OTAWA to easily produce semantics of machine code instruction making the data flow analysis independent of the actual ISA. The presentation will be followed by a demonstration of the OTAWA plugin in the Eclipse environment. 
OrateurHugues Cassé 

Aucun document lié à cet événement.

Retour à l'index