package jasmin

  1. Overview
  2. Docs
package jasmin
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module ForwardAnalyser.Make

Functor used to create a module implementing forward analysis.

It takes a module implementing the Logic interface and returns a module implementing the S signature.

Each instruction is annotated with its IN domain and the OUT domain is passed to the next instruction. Domain are updated using the functions provided by the Logic module. Control flow is handled as follow :

  • if bloc : * we assume the condition of the if bloc to produce two domains d1 and d2 * we analyse the first branch (then branch) with the domain d1 * we analyse the second branch (else branch) with the domain d2 * we merge the two domains to produce the final domain for the if bloc
  • while bloc (b1, condition, b2) : * we analyse the first bloc b1 with the input domain d * we loop and analyse the body of the while bloc (b2,b1,condition) until we reach a fixpoint * we return the corresponding domain
  • for bloc : * we convert the for loop to a while loop using a proxy variable for the loop variable : inline int i; for i = 0 to 10 { ... }

becomes :

inline int i; inline int i_proxy = 0; while (i_proxy < 10) { i = i_proxy; ... i_proxy++; } * we analyse the while loop with the while loop logic * we forget the proxy variable introduced by the for loop

Parameters

module Logic : Logic

Signature

type domain = Logic.domain
val analyse_function : ('info, 'asm) Jasmin.Prog.func -> (domain Annotation.annotation, 'asm) Jasmin.Prog.func

Entrypoint for analysis. args :

  • ('info,'asm) Prog.func (function to analyse) returns :d
  • (domain Annotation.annotation, 'asm) Prog.func (annotated function)