--- layout: fc_discuss_archives title: Message 21 from Frama-C-discuss on August 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Simplifying branches



Hello,

Le 17/08/2011 16:29, Daniel Sheridan a ?crit :
> I am working on a plugin which eliminates branches of code under certain
> circumstances. Using a combination of constant propagation and spare
> code analysis, I end up with code of the form
>
>   if (1) {
>      ...
>   }
>
> which is technically correct, but would be more useful if it were
> simplified. I notice that saving the code to disk and loading it in to
> Frama-C is enough to eliminate the unnecessary "if".

If I well understand what you are saying, you pretty print the generated 
code into a C file by using options "-print" and "-ocode", then you 
re-execute Frama-c on this file. Is it correct?

> Is it possible to access this simplification step from a plugin, or do I
> need to write my own visitor-based implementation of it?

In the next Frama-C version, there will be a function 
File.create_rebuilt_project_from_visitor which will do the job [*].

Thus you can write for instance the following script:

=== a.ml ===
let main () =
   (* propagates constants and put the resulting AST into project [p] *)
   let p =
     !Db.Constant_Propagation.get
       Datatype.String.Set.empty
       ~cast_intro:false
   in
   Project.on
     p
     (fun () ->
       (* print on stdout the unsimplified AST of constant propagation *)
       File.pretty_ast ();
       (* simplify the AST of project [p] and put the resulting AST
          in project [prj] *)
       let prj =
	File.create_rebuilt_project_from_visitor "p"
          (new Visitor.frama_c_copy)
       in
       (* print on stdout the simplified AST *)
       File.pretty_ast ~prj ())
     ()

let () = Db.Main.extend main
============

and run it in the following file:
=== a.c ===
int main(void) {
   int x = 0;
   if (x == 0) x = 1; else x = 2;
   return 0;
}
============

$ frama-c -load-script a.ml a.c
<snip information lines>
/* Generated by Frama-C */ // that is the unsimplified AST
int main(void)
{
   int __retres;
   int x;
   x = 0;
   if (1) { x = 1; }
   else { x = 2; }
   __retres = 0;
   return (__retres);
}


/* Generated by Frama-C */ // that is the simplified AST
int main(void)
{
   int __retres;
   int x;
   x = 0;
   x = 1;
   __retres = 0;
   return (__retres);
}

Hope this helps,
Julien

--------------------------------------------------------------------
[*] If you want to use this solution with the current Frama-C Carbon, 
below is an "almost correct" version of 
File.create_rebuilt_project_from_visitor. "Almost correct" means that 
you use neither plug-in which analyses non-C files, nor any module 
Cabs*, nor module Ast.UntypedFiles. The fully correct solution uses 
internal kernel values and the workaround is quite ugly.

let get_preprocessor_command () =
   let cmdline = Kernel.CppCommand.get() in
   if cmdline <> "" then cmdline
   else
     try Sys.getenv "CPP"
     with Not_found -> "gcc -C -E -I."

let from_filename ?(cpp=get_preprocessor_command ()) f =
   if Filename.check_suffix f ".i" then
     File.NoCPP f
   else
     let suf =
       try
         let suf_idx = String.rindex f '.' in
         String.sub f suf_idx (String.length f - suf_idx)
       with Not_found -> (* raised by String.rindex if '.' \notin f *)
         ""
     in
     File.External (f, suf)

let create_rebuilt_project_from_visitor ?(preprocess=false) prj_name 
visitor =
   let prj = File.create_project_from_visitor prj_name visitor in
   try
     let f =
       let name = "frama_c_project_" ^ prj_name ^ "_" in
       let ext = if preprocess then ".c" else ".i" in
       if Kernel.Debug.get () > 0 then Filename.temp_file name ext
       else Extlib.temp_file_cleanup_at_exit name ext
     in
     let cout = open_out f in
     let fmt = Format.formatter_of_out_channel cout in
     (*unjournalized_pretty prj (Some fmt) ();*)
     File.pretty_ast ~prj ~fmt ();
     let redo () =
       Project.clear
	~selection:(State_selection.Dynamic.with_dependencies Ast.self)
	();
       File.init_from_c_files
	[ if preprocess then from_filename f else File.NoCPP f ]
     in
     Project.on prj redo ();
     prj
   with Extlib.Temp_file_error s | Sys_error s ->
     Kernel.abort "cannot create temporary file: %s" s