在 Frama-C 中从原始源代码执行死代码消除/切片

Question

编辑：原来的问题有不必要的细节

我有一个源文件，我在 Frama-C 中进行值分析，一些代码在标准化 window 中被突出显示为死代码，没有原始源代码。

我可以获取一段删除死代码的原始代码吗？

Answer 1

简短回答：当前的 Frama-C 版本中没有任何内容可以让您直接执行此操作。此外，如果您的原始代码包含宏，Frama-C 甚至看不到真正的原始代码，因为它依赖于外部预处理器（例如 cpp）来进行宏扩展。

更长的答案：规范化（aka CIL）抽象语法树（AST，Frama-C 中 C 代码的内部表示）中的每个语句都包含有关原始语句位置（起点和终点）的信息它来自哪里，并且这些信息也可以在原始 AST（又名 Cabs）中找到。因此，对于 Frama-C 的内部工作原理（例如 developer's manual 的 reader）有很好了解的人可能会在两者之间建立对应关系，并使用它来检测死语句出租车。更进一步，可以绕过 Cabs，并在程序的原始文本中识别出死代码区域。但是请注意，这将是一项乏味且很容易出错的任务（特别是因为单个原始语句可以扩展为多个规范化语句）。

Answer 2

鉴于您的说明，我支持@Virgile 的回答；但是对于那些有兴趣在 Frama-C 中执行一些简单的死代码消除的人来说，下面的脚本（由没有 SO 帐户的同事赠送）可能会有所帮助。

(* 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

用法：

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

请注意，此脚本并非在所有情况下都有效，还可以进一步改进（例如处理初始化程序），但对于一些快速而肮脏的黑客攻击，它仍然会有帮助。

在 Frama-C 中从原始源代码执行死代码消除/切片

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

frama-c