CODEWITHSUNDEEP
frama-c
depechec0de
depechec0de

Reputation: 131

Performing dead code elimination / slicing from original source code in Frama-C

EDIT: The original question had unnecessary details

I have a source file which I do value analysis in Frama-C, some of the code is highlighted as dead code in the normalized window, no the original source code.

Can I obtain a slice of the original code that removes the dead code?

Upvotes: 1

Views: 181

Answers (2)

anol
anol

Reputation: 8953

Given your clarifications, I stand by @Virgile's answer; but for people interested in performing some simplistic dead code elimination within Frama-C, the script below, gifted by a colleague who has no SO account, could be helpful.

(* remove_dead_code.ml *)
let main () =
  !Db.Value.compute ();
  Slicing.Api.Project.reset_slicing ();
  let selection = ref Slicing.Api.Select.empty_selects in
  let o = object (self)
    inherit Visitor.frama_c_inplace
    method !vstmt_aux stmt =
      if Db.Value.is_reachable_stmt stmt then
        selection :=
          Slicing.Api.Select.select_stmt ~spare:true
            !selection
            stmt
            (Extlib.the self#current_kf);
      Cil.DoChildren
  end in
  Visitor.visitFramacFileSameGlobals o (Ast.get ());
  Slicing.Api.Request.add_persistent_selection !selection;
  Slicing.Api.Request.apply_all_internal ();
  Slicing.Api.Slice.remove_uncalled ();
  ignore (Slicing.Api.Project.extract "no-dead")

let () = Db.Main.extend main

Usage:

frama-c -load-script remove_dead_code.ml file.c -then-last -print -ocode output.c

Note that this script does not work in all cases and could have further improvements (e.g. to handle initializers), but for some quick-and-dirty hacking, it can still be helpful.

Upvotes: 1

Virgile
Virgile

Reputation: 10148

Short answer: there's nothing in the current Frama-C version that will let you do that directly. Moreover, if your original code contains macros, Frama-C will not even see the real original code, as it relies on an external preprocessor (e.g. cpp) to do macro expansion.

Longer answer: Each statement in the normalized (aka CIL) Abstract Syntax Tree (AST, the internal representation of C code within Frama-C) contains information about the location (start point and end point) of the original statement where it stems from, and this information is also available in the original AST (aka Cabs). It might thus be possible for someone with a good knowledge of Frama-C's inner workings (e.g. a reader of the developer's manual), to build a correspondance between both, and to use that to detect dead statement in Cabs. Going even further, one could bypass Cabs, and identify zones in the original text of the program which are dead code. Note however that it would be a tedious and quite error prone (notably because a single original statement can be expanded in several normalized ones) task.

Upvotes: 1

Related Questions