Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Simplifying branches

  • Subject: [Frama-c-discuss] Simplifying branches
  • From: Julien.Signoles at cea.fr (Julien Signoles)
  • Date: Mon, 22 Aug 2011 14:17:59 +0200
  • In-reply-to: <1313591386.20010.50.camel@coquet>
  • References: <1313591386.20010.50.camel@coquet>
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