2021-02-27 10:55 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000679Frama-CPlug-in > slicingpublic2014-02-12 16:54
Reporterpatrick 
Assigned ToAnne 
PrioritynormalSeveritycrashReproducibilityhave not tried
StatusclosedResolutionfixed 
Product Version 
Target VersionFixed in VersionFrama-C Oxygen-20120901 
Summary0000679: untypable ACSL in a sliced program containing \at(p,label) when the label was removed
Descriptionbug when a code annotation refers to a label and the label is removed into the sliced program.

Additional Information===== bug.c =====
void f(void) { return; }
int X = 1 ;
int main(void) {
 call: f();
  //@ assert X == \at(X,call);
  return X;
}
==================

$frama-c bug.c -slice-return main -then-on "Slicing export" -print -ocode sliced_bug.c
...
[kernel] failure: Cannot find label for \at

$ frama-c sliced_bug.c
TagsNo tags attached.
Attached Files

-Relationships
+Relationships

-Notes

~0001402

patrick (developer)

A first action fixing the bug can be done:
1) filter out code annotations containing \at(e,L) constructs when the statement labeled by L is filtered out

A better alternative could be:
2a) filter out code annotations containing \at(e,L) constructs when control dependency of the statement labeled by L is not preserved (control mark=bottom).
2b) do not filter out a labeled statement when its control dependency is preserved : if the statement effects are not preserved then replace the statement by a skip statement otherwise keep the statement as it is.

~0002427

Anne (reporter)

I think that the easiest way to fix this problem is to change [!Db.Properties.Interp.To_zone.from_stmt_annot] in order that it also returns the user labels needed by the annotation so that [find_code_annot_nodes] (in src/pdg/annot.ml) could include the nodes of the labels in its result.

~0002434

patrick (developer)

As there are some extract functions into cil.ml, I can add a function
Cil.extract_labels_from_annot:
  Cil_types.code_annotation -> Cil_datatype.Logic_label.Set.t

From it, it is possible to build a function extracting C stmt :
Cil.extract_stmts_from_labels
 Cil_datatype.Logic_label.Set.t -> Cil_datatype.Stmt.Set.t

Anne, will it be ok for you ?

~0002435

patrick (developer)

In fact I modified the type t_decl returned by most of the functions of To_zone.from_xxxx. It was Cil_datatype.Varinfo.Set.t.
t_decl contents a field var -> the previous Cil_datatype.Varinfo.Set.t,
and a field lbl:Cil_datatype.Stmt.Set.t -> the statement referenced labels of the At() constructions.

~0002437

patrick (developer)

The new field lbl has to be used into [src/pdg/annot.ml]...

~0002438

patrick (developer)

Bug fixed

Sending src/pdg/annot.ml
Adding tests/slicing/bts679.i
Adding tests/slicing/oracle/bts679.res.oracle

Committed revision 15974.

~0002445

Anne (reporter)

Well, I think that the bug is still there :

int X = 1 ;
int main(void) {
  int y;
L: y = 0;
  //@ assert X == \at(X,L);
  return X;
}

$ frama-c -slice-assert main toto.c -slicing-debug 2
[slicing] [SlicingTransform.Visibility.label_visible] label L: is invisible
[slicing] [SlicingTransform.Visibility.annotation_visible] -> yes
[kernel] failure: Cannot find label for \at

and this is because the label and the statement are two separate things in the PDG. So it would be better if [Db.Properties.Interp.To_zone.from_stmt_annot] could return real labels instead of statements. (set of pairs [(stmt * label)] would be perfect).

~0002446

Anne (reporter)

Well, finally, many things about labels are missing: for instance, the PDG only has nodes for labels that are used for jumps, and high level function to find labels in PDG or to select them in slicing are also missing... I try to add this as soon as possible.

~0002447

Anne (reporter)

The example above is now in [tests/slicing/bts679b.i].

It is working in rev16020 (had finally to also change [slicingCommand] since [pdg/annot] seems to be not used in that context).

Anyway, the slicing could be better: I don't know why [y=0] is selected as [spare] instead of being sliced away...

~0002448

Anne (reporter)

@Patrick: sorry ! I didn't succeed to fix the problem. Our idea was good: changing [select_stmt_zone] by [select_stmt_zone_internal] at the end of [select_ZoneAnnot_zones_decl_vars] solve the problem above, but some other tests (like [tests/slicing/bts341.c] for instance) don't work anymore then.

I think that the main problem is that, on one hand, we build requests to slice for an annotation in [slicingCmd] but on the other hand, we use PDG [find_code_annot_nodes] in [slicingTransform] to decide if the annotation is visible at the end.
I guess that the selections are probably not the same (as they should be!), but I haven't found why :-(

We probably tests the visibility of two many nodes for the control dependencies in [find_code_annot_nodes]...

~0002451

patrick (developer)

The remaining problem is that some slicing results have too much [spare] selections. This isn't directly due to the previous changes.

That comes from [slicingCmd] and the interface of To_zone.from_xxxx functions. These functions return couples of [Zones*Stmt], and [slicingCmd] selects the ctrl of theses [Stmt], and their integrality as [spare].
To solve the remaining problem, they should return [Zones*Label] instead and [slicingCmd] should select the ctrl of theses [Label], and their integrality as [spare].

This work can be considered as another feature wished.
The initial bug is now fixed.
+Notes

-Issue History
Date Modified Username Field Change
2011-01-19 17:04 patrick New Issue
2011-01-19 17:04 patrick Status new => assigned
2011-01-19 17:04 patrick Assigned To => Anne
2011-01-21 11:16 patrick Note Added: 0001402
2011-04-14 09:50 patrick Severity minor => crash
2011-10-27 15:54 Anne Note Added: 0002427
2011-10-28 09:36 patrick Note Added: 0002434
2011-10-28 10:58 patrick Note Added: 0002435
2011-10-28 10:58 svn
2011-10-28 11:00 patrick Note Added: 0002437
2011-10-28 11:23 patrick Note Added: 0002438
2011-11-03 06:41 Anne Note Added: 0002445
2011-11-03 11:28 Anne Note Added: 0002446
2011-11-03 13:14 Anne Note Added: 0002447
2011-11-03 17:01 Anne Note Added: 0002448
2011-11-04 08:45 patrick Note Added: 0002451
2011-11-04 08:46 patrick Status assigned => resolved
2011-11-04 08:46 patrick 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
2013-12-19 01:12 patrick Source_changeset_attached => framac master f82bc43b
2014-02-12 16:54 patrick Source_changeset_attached => framac stable/neon f82bc43b
+Issue History