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] interfacing non-OCaml programs with Frama-C

  • Subject: [Frama-c-discuss] interfacing non-OCaml programs with Frama-C
  • From: Pascal.CUOQ at cea.fr (CUOQ Pascal)
  • Date: Sat, 17 Jan 2009 20:38:07 +0100
  • References: <5EFD4D7AC6265F4D9D3A849CEA9219191AB11D@LAXA.intra.cea.fr><bacfeaa40811280930r1b6f0e46xad400ebefbdf4646@mail.gmail.com><5EFD4D7AC6265F4D9D3A849CEA9219191AB120@LAXA.intra.cea.fr> <bacfeaa40901160754h432d2715u5627b90af7080e57@mail.gmail.com>
Hi!

First, much kudos. What you are doing is pretty impressive
considering how the thread started. Maybe it's time to change
the title.

Calling List.nth iteratively is a little inefficient.
The usual way to write something more efficient in OCaml is
to use List.map, which takes a function and applies it to each
element of the list. In your example, you could apply List.map to
the function that transforms one variable into its value,
and this would build the function that takes the list of variables
and returns the list of their respective values.

Please see 
http://caml.inria.fr/pub/docs/manual-ocaml/libref/List.html#6_Iterators
and take a look at the functions fold_left and iter while you're there,
they could both be useful to you too for what you want to do.

What you really want to do (obtaining tuples) is just one step from
there: in order to get the tuples the way you want them, 
you have to iterate over the states the function that constructs
the list of values of your variables.

> I know that (List.length vars_list) will be limited by SemanticUnrollingLevel

Actually, it won't. What will be limited will be the number of tuples
you can get this way. (List.length vars_list) is the size of each tuple,
and you can make it as big as you want.

What you are asking requires access to the several states attached to
a statement instead of just their union. These states are not kept in
memory, only their union is accumulated during the analysis, because
it would take up too much memory to store them individually.  However,
if you are not targeting big programs for your project, the
instructions below allow you to get access to the states while the
analysis is taking place.

0/ start with version 20081201
1/ move src/value/state_set.ml and src/value/state_set.mli to src/memory_state
2/ apply the attached patch
3/ run configure and "make depend" again. Remove any file
   named src/value/state_set.cm* if they exist.

It goes without saying that you surrender the privilege of being able to
report bugs in the Bug Tracking System when you do this. Better tell
me privately if you encounter problems.

You can now register a caml function (let us assume you call it
"youhou") as a hook to be called on a data structure that contains all
the computed states, indexed by kinstr, 
at the end of the analysis of each function of the analyzed code. Be
aware that if the analyzed code contains function calls, youhou will
be called several times, and may even be called several times for the
same analyzed function f if f is either called from several places or
called from within a loop. However, do not make assumptions on the
number of times youhou will be called. It can be more or less that the
number of times it would be called in a real execution.  The only
guarantee is that any concrete execution is included in at least one
of the abstract executions that youhou will see.

youhou is passed a representation of the (abstract) call stack, so that
it knows what stage of the analysis the states correspond to. I would
have recommended to take a look at the plug-in "from" for an example
of use of such hooks, but the code of this plug-in is a little messy
and I am not sure it's a good idea to send you there.

Here is a short example instead:

(* defining our youhou function: *)
let youhou (_call_stack, instrstates) =
    InstrHashtbl.iter 
      (fun ki superposition ->
         let kinstr_string = 
           match ki with
           | Cil_types.Kglobal ->
               "entry point"
           | Cil_types.Kstmt s ->
               string_of_int s.Cil_types.sid
        in             
        Format.printf "kinstr:%s at ." kinstr_string;
        State_set.iter 
          (fun state -> 
             Format.printf "state:%a at ."
               Relations_type.Model.pretty state)
           superposition)
       instrstates

(* registering youhou to be called while the analysis is taking place: *)
 Db.Value.Record_Value_Superposition_Callbacks.extend youhou;

Testing on an example:
int a, b;
void main(int c)
{
  c = c ? 0 : 1;
  if (c)
    b = 2;
  a = c;
}

command:
bin/toplevel.byte -val -slevel 10 t.c

result:
...
kinstr:8
state:a IN {0; }
      b IN {0; }
      c IN {0; }
      
state:a IN {0; }
      b IN {2; }
      c IN {1; }
      
kinstr:10
state:a IN {0; }
      b IN {0; }
      c IN {0; }
      
state:a IN {1; }
      b IN {2; }
      c IN {1; }
...



-------------- section suivante --------------
Une pi?ce jointe non texte a ?t? nettoy?e...
Nom: states_hook.patch
Type: application/octet-stream
Taille: 3549 octets
Desc: states_hook.patch
Url: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090117/20ebc20c/attachment.obj