2021-03-03 04:12 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000780Frama-CPlug-in > slicingpublic2014-02-12 16:54
Reporterpascal 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C Nitrogen-20111001 
Summary0000780: r12793: slicing generates uncompilable code (sliced function called with too few arguments) (csmith)
DescriptionBug occurred with pre-processing done on a 64-bit machine.

~/ppc/bin/toplevel.opt -val-signed-overflow-alarms noresult.11005403.1.c -cpp-command "gcc -C -E -I. -I$CSMITH/runtime " -machdep x86_64 -slice-calls printf -slevel 5000 -slevel-function crc32_gentab:0 -then-on 'Slicing export' -no-val -slevel 0 -print -ocode noresult.11005403.1.s.c

produced the provided noresult.11005403.1.s.c file, which does not compile:

gcc -I runtime noresult.11005403.1.s.c
noresult.11005403.1.s.c: In function ‘func_1_slice_1’:
noresult.11005403.1.s.c:466: error: too few arguments to function ‘func_28_slice_1’
noresult.11005403.1.s.c: In function ‘func_28_slice_1’:
noresult.11005403.1.s.c:741: error: ‘p_29’ undeclared (first use in this function)
noresult.11005403.1.s.c:741: error: (Each undeclared identifier is reported only once
noresult.11005403.1.s.c:741: error: for each function it appears in.)


The original compiles, although it does have some warnings:

gcc -I runtime noresult.11005403.1.c
noresult.11005403.1.c: In function ‘func_56’:
noresult.11005403.1.c:819: warning: comparison of distinct pointer types lacks a cast
noresult.11005403.1.c:879: warning: comparison of distinct pointer types lacks a cast
noresult.11005403.1.c:886: warning: comparison of distinct pointer types lacks a cast
noresult.11005403.1.c: In function ‘func_116’:
noresult.11005403.1.c:2053: warning: comparison of distinct pointer types lacks a cast
noresult.11005403.1.c:2054: warning: comparison of distinct pointer types lacks a cast
TagsNo tags attached.
Attached Files
  • tgz file icon slice_missing_arg.tgz (56,651 bytes) 2011-04-11 01:07
  • ? file icon frama_c_journal.ml (3,304 bytes) 2011-04-11 10:26 -
    (* Frama-C journal generated at 10:20 the 11/04/2011 *)
    
    exception Unreachable
    exception Exception of string
    
    (* Run the user commands *)
    let run () =
      Parameters.Dynamic.Bool.set "-val-signed-overflow-alarms" true;
      Parameters.CppCommand.set "gcc -C -E -I. -I./runtime ";
      Parameters.Machdep.set "x86_64";
      Parameters.Dynamic.StringSet.set "-slice-calls"
        (Datatype.String.Set.singleton "printf");
      Parameters.Dynamic.Int.set "-slevel" 5000;
      Parameters.Dynamic.StringSet.set "-slevel-function"
        (Datatype.String.Set.singleton "crc32_gentab:0");
      Parameters.Files.set [ "noresult.11005403.1.c" ];
      !Db.Value.compute ();
      let sl_project_Slicing = !Db.Slicing.Project.mk_project "Slicing" in
      !Db.Slicing.Project.set_project
        (Some (!Db.Slicing.Project.from_unique_name "Slicing"));
      !Db.Slicing.Request.add_persistent_cmdline sl_project_Slicing;
      !Db.Slicing.Request.apply_all_internal sl_project_Slicing;
      !Db.Slicing.Slice.remove_uncalled sl_project_Slicing;
      let p_Slicing__export =
        !Db.Slicing.Project.extract "Slicing export" sl_project_Slicing
      in
      Parameters.Dynamic.Bool.set "-slice-force" false;
      Parameters.Dynamic.Bool.clear "-wp-dot" ();
      Parameters.Dynamic.Bool.clear "-wp-print" ();
      Parameters.Dynamic.String.clear "-wp-check" ();
      Parameters.Dynamic.StringSet.clear "-wp-prop" ();
      Parameters.Dynamic.StringSet.clear "-wp-bhv" ();
      Parameters.Dynamic.StringSet.clear "-wp-fct" ();
      Parameters.Dynamic.Bool.clear "-wp" ();
      Project.set_current ~on:true p_Slicing__export;
      Parameters.Dynamic.Bool.set "-val" false;
      Parameters.Dynamic.Int.set "-slevel" 0;
      Parameters.PrintCode.set true;
      Parameters.CodeOutput.set "noresult.11005403.1.s.c";
      !Db.Value.compute ();
      let sl_project_Slicing_2 = !Db.Slicing.Project.mk_project "Slicing" in
      !Db.Slicing.Project.set_project
        (Some (!Db.Slicing.Project.from_unique_name "Slicing"));
      !Db.Slicing.Request.add_persistent_cmdline sl_project_Slicing_2;
      !Db.Slicing.Request.apply_all_internal sl_project_Slicing_2;
      !Db.Slicing.Slice.remove_uncalled sl_project_Slicing_2;
      let p_Slicing__export_2 =
        !Db.Slicing.Project.extract "Slicing export" sl_project_Slicing_2
      in
      Parameters.Dynamic.Bool.set "-slice-force" false;
      Parameters.Dynamic.Bool.clear "-wp-dot" ();
      Parameters.Dynamic.Bool.clear "-wp-print" ();
      Parameters.Dynamic.String.clear "-wp-check" ();
      Parameters.Dynamic.StringSet.clear "-wp-prop" ();
      Parameters.Dynamic.StringSet.clear "-wp-bhv" ();
      Parameters.Dynamic.StringSet.clear "-wp-fct" ();
      Parameters.Dynamic.Bool.clear "-wp" ();
      File.pretty_ast ~prj:p_Slicing__export ();
      Project.set_current ~on:true (Project.from_unique_name "default");
      ()
    
    (* Main *)
    let main () =
      Journal.keep_file "frama_c_journal.ml";
      try run ()
      with
      | Unreachable -> Kernel.fatal "Journal reachs an assumed dead code" 
      | Exception s -> Kernel.log "Journal re-raised the exception %S" s
      | exn ->
        Kernel.fatal
          "Journal raised an unexpected exception: %s"
          (Printexc.to_string exn)
    
    (* Registering *)
    let main : unit -> unit =
      Dynamic.register
        ~plugin:"Frama_c_journal"
        "main"
        (Datatype.func Datatype.unit Datatype.unit)
        ~journalize:false
        main
    
    (* Hooking *)
    let () = Cmdline.run_after_loading_stage main; Cmdline.is_going_to_load ()
    
    ? file icon frama_c_journal.ml (3,304 bytes) 2011-04-11 10:26 +

-Relationships
related to 0000791closedpascal Cash in value analysis of sliced project 
+Relationships

-Notes

~0001692

Anne (reporter)

Ok : I'll have a look. The result seems quite strange !

~0001693

Anne (reporter)

It seems that the slicing is applied twice. The first result looks better... I have to investigate :
- why the slicing is done a second time;
- why is the result incorrect the second time;

~0001694

pascal (reporter)

I noticed that the value analysis was launched a second time. I wasn't able to prevent it, so I set slevel to zero the second time.

This other bug (slicing launching again on sliced project) should be investigated, and the bug occurring here may only be a consequence of the strange circumstances this causes.

~0001695

monate (reporter)

I uploaded the generated journal. Some slicing options have probably not been reset correctly upon completion.

~0001697

Anne (reporter)

A workaround is to use the option [-no-slice-force] in the second part of the command (after the [-then-on]).

~0001698

Anne (reporter)

When saving the result of the first slicing, and applying the slicing again, the second result is correct (at least gcc is happy with it).

~0001699

pascal (reporter)

Regarding the workaround, how is one supposed to use it?

I have the line:

~/ppc/bin/toplevel.opt -val-signed-overflow-alarms t$N.c -cpp-command "gcc -C -E -I. -I$CSMITH/runtime " -machdep x86_64 -slice-calls printf -slevel 5000 -slevel-function crc32_gentab:0 -then-on 'Slicing export' -no-slice-force -no-val -print -ocode s$N.c

The wrong actions are still taken on the sliced project: I can see clearly the value analysis being launched the second time, because function crc32_gentab has been renamed crc32_gentab_slice1, so "-slevel-function crc32_gentab:0 " does not apply to it and this function takes a long time.

Or do I need to write a journal ?

~0001700

Anne (reporter)

I have just added the [-no-slice-force] to the end of your first command... but I forgot that I have done a test with Patrick so that I have changed something : sorry! The modification is to move [SlicingParameters.set_off ()] before the call to [Db.Slicing.Project.extract] in [slicing/register.ml]. I don't commit it yet because I am waiting for Patrick and Julien recommendation.

~0001702

Anne (reporter)

The initial problem is still there and can now be seen using an explicit call to the slicer on the generated project (ie. [-slice-calls printf] after [-then-on]).

~0001714

Anne (reporter)

The initial problem disappeared ! I don't manage to reproduce it... sorry.

~0001715

patrick (developer)

Last edited: 2011-04-11 15:41

I got the following error during the second slicing:
[kernel] user error: Function tmp_50 invoked on a non function type
[kernel] Frama-C aborted because of invalid user input.

with command:
frama-c -val-signed-overflow-alarms noresult.11005403.1.c -cpp-command "gcc -C -E -I. -Iruntime " -machdep x86_64 -slice-calls printf -slevel 5000 -slevel-function crc32_gentab:0 -check -then-on 'Slicing export' -slice-calls printf -check -print -slice-force

~0001717

signoles (manager)

Just add option "-slice-force" after "-then-on":

~/ppc/bin/toplevel.opt -val-signed-overflow-alarms noresult.11005403.1.c -cpp-command "gcc -C -E -I. -I$CSMITH/runtime " -machdep x86_64 -slice-calls printf -slevel 5000 -slevel-function crc32_gentab:0 -then-on 'Slicing export' -no-val -slevel 0 -print -ocode noresult.11005403.1.s.c -slice-force

~0001719

Anne (reporter)

Ok : thanks ! I'll have a look again.

~0001720

Anne (reporter)

The problem doesn't have the same symptom than before, but it is still there and is even more strange : a function in a call ([safe_add_func_uint32_t_u_u_slice_1]) is substituted by a variable ([tmp_50] which is detected by the [-check] option) ! While doing the exportation, the function name seems to be still there (in the debug messages) but in the result (printed by [-slice-print]) it has been substituted...
It seems that it is not the only case : many [tmp_xx] variables appear in function calls.

~0001721

Anne (reporter)

I think that the problem comes from [Filter.compute_fct_definitions] which does suspicious things about function variables. While processing the function body, everything seems ok, but when the visitor prints "Adding definition %s (vid: %d) for project %s", the definition is not ok anymore.
I not sure to understand what is done here.

Could you have a look Virgile ? Thanks.

~0001722

Anne (reporter)

My command line :
frama-c noresult.11005403.1.c -cpp-command "gcc -C -E -I. -Iruntime " \
  -machdep x86_64 -val-signed-overflow-alarms -slevel 0 \
  -slice-calls printf -slice-print \
-then-on 'Slicing export' \
  -slice-calls printf -slice-print -slice-force \
  -debug 1 -check \
> slice.log

~0001788

yakobowski (manager)

Fixed by changeset 12885. Varinfos were created by the slicing in the wrong project.
+Notes

-Issue History
Date Modified Username Field Change
2011-04-11 01:07 pascal New Issue
2011-04-11 01:07 pascal Status new => assigned
2011-04-11 01:07 pascal Assigned To => Anne
2011-04-11 01:07 pascal File Added: slice_missing_arg.tgz
2011-04-11 09:02 Anne Note Added: 0001692
2011-04-11 09:02 Anne Status assigned => acknowledged
2011-04-11 09:46 Anne Note Added: 0001693
2011-04-11 10:12 pascal Note Added: 0001694
2011-04-11 10:26 monate File Added: frama_c_journal.ml
2011-04-11 10:27 monate Note Added: 0001695
2011-04-11 10:40 Anne Note Added: 0001697
2011-04-11 10:46 Anne Note Added: 0001698
2011-04-11 10:53 pascal Note Added: 0001699
2011-04-11 11:05 Anne Note Added: 0001700
2011-04-11 11:39 svn
2011-04-11 11:41 Anne Note Added: 0001702
2011-04-11 15:01 Anne Note Added: 0001714
2011-04-11 15:36 patrick Note Added: 0001715
2011-04-11 15:41 patrick Note Edited: 0001715
2011-04-11 15:48 signoles Note Added: 0001717
2011-04-11 15:50 Anne Note Added: 0001719
2011-04-11 16:23 Anne Note Added: 0001720
2011-04-11 17:11 Anne Note Added: 0001721
2011-04-11 17:11 Anne Status acknowledged => assigned
2011-04-11 17:11 Anne Assigned To Anne => virgile
2011-04-11 17:18 Anne Note Added: 0001722
2011-04-14 14:33 yakobowski Relationship added related to 0000791
2011-04-14 14:34 yakobowski Note Added: 0001788
2011-04-14 14:34 yakobowski Status assigned => resolved
2011-04-14 14:34 yakobowski Fixed in Version => Frama-C GIT, precise the release id
2011-04-14 14:34 yakobowski Resolution open => fixed
2011-10-10 14:13 signoles Fixed in Version Frama-C GIT, precise the release id => Frama-C Nitrogen-20111001
2011-10-10 14:14 signoles Status resolved => closed
2013-12-19 01:12 Anne Source_changeset_attached => framac master 0df1243f
2014-02-12 16:54 Anne Source_changeset_attached => framac stable/neon 0df1243f
+Issue History