2021-01-26 19:09 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001194Frama-CPlug-in > scopepublic2012-09-19 17:16
ReporterAnne 
Assigned Toyakobowski 
PrioritynormalSeverityminorReproducibilityhave not tried
StatusclosedResolutionfixed 
Product VersionFrama-C Nitrogen-20111001 
Target VersionFixed in VersionFrama-C Oxygen-20120901 
Summary0001194: imprecision in PDG when unreachable statements
DescriptionThe PDG computation propagates a state that roughly maps zones to PDG nodes. It uses a Lmap_bitwise.Location_map_bitwise. After an unreachable statement, the state is said to be "empty" instead of "bottom", which leads to some imprecision when merging with another state because instead of having:
{ x --> XXX } U bottom = { x --> XXX }
we get :
{ x --> XXX } U { } = { x --> XXX or SELF }

Please, ask if you need more information to fix it.
Additional InformationCan see the problem with the enclosed script :
and pdg_pb.c :

int main (void) {
  int x = 0;
  char * name = get_name ();
  if (x > 0) {
    x ++;
  }
  f (name);
  return x;
}


$ frama-c pdg_pb.c -load-script pdg_pb.ml
TagsNo tags attached.
Attached Files
  • ? file icon pdg_pb.ml (1,196 bytes) 2012-06-11 12:09 -
    open Cil_types
    open Cil_datatype
    
    let main () =
      Ast.compute ();
      let kf = Globals.Functions.find_by_name "f" in
      let sites = Kernel_function.find_syntactic_callsites kf in
      let kf_main, stmt = match sites with
        | (kf, s)::[] -> kf, s
        | _ -> assert false
      in
        Format.printf "[script] call in '%a' : %a@." Kf.pretty kf_main Stmt.pretty stmt;
      let pdg = !Db.Pdg.get kf_main in
      let num_arg = 1 in
      let exp = match stmt.skind with
             | Instr (Call (_, _fct, args, _)) -> List.nth args (num_arg-1)
             | _ -> assert false
      in
      let lval = match exp.enode with
        | Lval lval -> lval
        | _ -> assert false
      in
         Format.printf "[script] lval of %d arg = %a@."
           num_arg  !Ast_printer.d_lval lval;
      let zone = !Db.Value.lval_to_zone (Kstmt stmt)
                     ~with_alarms:CilE.warn_none_mode lval in
      let nodes, undef =
        !Db.Pdg.find_location_nodes_at_stmt pdg stmt ~before:true zone
      in match undef with None ->
        Format.printf "[script] %d nodes + no undef @."
          (List.length nodes) 
        | Some undef ->
        Format.printf "[script] %d nodes + undef = %a@."
          (List.length nodes) Locations.Zone.pretty undef
    
    
    let () = Db.Main.extend main
    
    ? file icon pdg_pb.ml (1,196 bytes) 2012-06-11 12:09 +

-Relationships
+Relationships

-Notes

~0003101

Anne (reporter)

I thing that the easiest fix would be to have a option type in PdgTypes.t_data_state to be able to encode bottom as None and to adapt Pdg_state accordingly.

~0003104

yakobowski (manager)

Nicely spotted, thanks.

Do you have an example where one of the plugins derived from the PDG (slicing or scope?) are less precise than they should because of this?

~0003105

Anne (reporter)

I don't have any at the moment since I have seen this in my development, but I can build one as soon as I have a moment (this afternoon I think).

~0003106

Anne (reporter)

Here is an example :
$ frama-c -slice-assert f ex.c -slice-print
int Y;
void f (void) {
  int x = 0;
  Y = input ();
  if (x > 0) {
    Y ++;
  }
  //@ assert Y > 0;
}
void main (void) {
  Y = 3;
  f ();
  return 0;
}
The statement Y=3 in 'main' is kept and it shouldn't.
(Notice that if you remove the dead code in 'f', it isn't).
If you need more explanation, please ask.

~0003107

yakobowski (manager)

Thanks. There were no differences after adding dummy affectations to 'name' before the call to 'get_name', and I wasn't sure there was a real impact. Moreover, Scope/Defs seems to be happy, although I'm not completely sure why.

I believe I have a fix directly inside Lmap_bitwise. This would be more general then a change to pdg_state, and would also improve the precision of some From computations. Thus, this is likely to get fixed for Oxygen.

~0003108

Anne (reporter)

I don't think that the problem comes from Lmap_bitwise !
{ x --> XXX } U { } = { x --> XXX or SELF }
is correct since x is mapped to XXX in one branch and to nothing in the other.
Exemple :
void f (void) {
  if (c) x = 2;
  y = x;
}
You are really interested by 'x' value before calls to 'f'.


The bug is really in PDG because it uses 'empty' instead of 'bottom' for unreachable statements..

~0003111

yakobowski (manager)

Fixed in revision 18807
+Notes

-Issue History
Date Modified Username Field Change
2012-06-11 12:09 Anne New Issue
2012-06-11 12:09 Anne Status new => assigned
2012-06-11 12:09 Anne Assigned To => yakobowski
2012-06-11 12:09 Anne File Added: pdg_pb.ml
2012-06-11 12:23 Anne Note Added: 0003101
2012-06-12 11:10 yakobowski Note Added: 0003104
2012-06-12 11:15 Anne Note Added: 0003105
2012-06-12 14:26 Anne Note Added: 0003106
2012-06-12 15:19 yakobowski Note Added: 0003107
2012-06-12 15:51 Anne Note Added: 0003108
2012-06-12 17:57 yakobowski Note Added: 0003111
2012-06-12 17:57 yakobowski Status assigned => resolved
2012-06-12 17:57 yakobowski Resolution open => fixed
2012-09-19 17:15 signoles Fixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16 signoles Status resolved => closed
+Issue History