search

utwente-fmt / ltsmin

The LTSmin model checking toolset
http://ltsmin.utwente.nl
BSD 3-Clause "New" or "Revised" License
52 stars 30 forks source link

make sure all fields are 0/NULL initially #142

Closed yanntm closed 6 years ago

yanntm commented 6 years ago

valgrind was complaining about "conditional jump on uninitialized"

This seems to concern three unintialized fields :

model->default_filter (line 589) model->covered_by (l. 655) model->covered_by_short (l. 657)

Patch consists in : just malloc and set to zero the whole model struct in createBase.

Another patch could have been to add them to the intialization list in the same function GBcreateBase, but this is more resistant to adding other fields (and forgetting to init them)

Some traces before the patch :

[ythierry@oxygen ltsmin (next)]$ valgrind src/pins2lts-mc/pins2lts-mc ../ITS-Tools-pnmcc/INPUTS/Railroad-PT-005/gal.so  --when --ltl 'X(<>(X([]((LTLAP15==true)))))'  --strategy=bfs --procs=1  
==2676== Memcheck, a memory error detector
==2676== Copyright (C) 2002-2015, and GNU GPL'd, by Julian Seward et al.
==2676== Using Valgrind-3.12.0 and LibVEX; rerun with -h for copyright info
==2676== Command: src/pins2lts-mc/pins2lts-mc ../ITS-Tools-pnmcc/INPUTS/Railroad-PT-005/gal.so --when --ltl X(\<\>(X([]((LTLAP15==true))))) --strategy=bfs --procs=1
==2676== 
pins2lts-mc, 0.038: Registering PINS so language module
pins2lts-mc, 0.066, ** error **: Unable to open cgroup memory limit file /sys/fs/cgroup/memory/memory.limit_in_bytes: No such file or directory
==2676== Warning: set address range perms: large range [0x804f6d040, 0xfded45840) (undefined)
pins2lts-mc, 0.072: Loading model from ../ITS-Tools-pnmcc/INPUTS/Railroad-PT-005/gal.so
pins2lts-mc, 0.085: library has no initializer
pins2lts-mc, 0.086: loading model GAL
pins2lts-mc, 0.132: completed loading model GAL
pins2lts-mc, 0.134: LTL layer: formula: X(<>(X([]((LTLAP15==true)))))
pins2lts-mc, 0.136: "X(<>(X([]((LTLAP15==true)))))" is not a file, parsing as formula...
pins2lts-mc, 0.171: Using Spin LTL semantics
pins2lts-mc, 0.221: buchi has 2 states
==2676== Conditional jump or move depends on uninitialised value(s)
==2676==    at 0x43A003: GBinitModelDefaults (pins.c:589)
==2676==    by 0x451C90: GBaddLTL (pins2pins-ltl.c:1003)
==2676==    by 0x43C916: wrapModel (pins.c:1211)
==2676==    by 0x43CBD2: GBloadFile (pins.c:1280)
==2676==    by 0x4188A8: create_pins_model (pins2lts-mc.c:122)
==2676==    by 0x4188D5: global_and_model_init (pins2lts-mc.c:138)
==2676==    by 0x418A89: main (pins2lts-mc.c:203)
==2676== 
==2676== Conditional jump or move depends on uninitialised value(s)
==2676==    at 0x43A395: GBinitModelDefaults (pins.c:655)
==2676==    by 0x451C90: GBaddLTL (pins2pins-ltl.c:1003)
==2676==    by 0x43C916: wrapModel (pins.c:1211)
==2676==    by 0x43CBD2: GBloadFile (pins.c:1280)
==2676==    by 0x4188A8: create_pins_model (pins2lts-mc.c:122)
==2676==    by 0x4188D5: global_and_model_init (pins2lts-mc.c:138)
==2676==    by 0x418A89: main (pins2lts-mc.c:203)
==2676== 
==2676== Conditional jump or move depends on uninitialised value(s)
==2676==    at 0x43A3C2: GBinitModelDefaults (pins.c:657)
==2676==    by 0x451C90: GBaddLTL (pins2pins-ltl.c:1003)
==2676==    by 0x43C916: wrapModel (pins.c:1211)
==2676==    by 0x43CBD2: GBloadFile (pins.c:1280)
==2676==    by 0x4188A8: create_pins_model (pins2lts-mc.c:122)
==2676==    by 0x4188D5: global_and_model_init (pins2lts-mc.c:138)
==2676==    by 0x418A89: main (pins2lts-mc.c:203)
==2676== 
==2676== Warning: set address range perms: large range [0x39600000, 0x239600000) (defined)
==2676== Warning: set address range perms: large range [0x239600000, 0x2b9600000) (defined)
pins2lts-mc, 0.293: There are 76 state labels and 1 edge labels
pins2lts-mc, 0.294: State length is 55, there are 60 groups
pins2lts-mc, 0.294: Running bfs using 1 core (sequential)
pins2lts-mc, 0.294: Using a non-indexing tree table with 2^30 elements
pins2lts-mc, 0.295: Successor permutation: none
pins2lts-mc, 0.295: Global bits: 0, count bits: 0, local bits: 0
pins2lts-mc, 0.564: 15 levels 1000 states 3749 transitions
pins2lts-mc, 0.794:  
pins2lts-mc, 0.794:  
pins2lts-mc, 0.795: Explored 1853 states 7739 transitions, fanout: 4.176
pins2lts-mc, 0.800: Total exploration time 0.490 sec (0.490 sec minimum, 0.490 sec on average)
pins2lts-mc, 0.802: States per second: 3782, Transitions per second: 15794
pins2lts-mc, 0.807:  
pins2lts-mc, 0.808: Queue width: 8B, total height: 251, memory: 0.00MB
pins2lts-mc, 0.809: Tree memory: 0.0MB, 21.8 B/state, compr.: 9.8%
pins2lts-mc, 0.810: Tree fill ratio (roots/leafs): 0.0%/0.0%
pins2lts-mc, 0.811: Stored 56 string chucks using 0MB
pins2lts-mc, 0.813: Total memory used for chunk indexing: 0MB
pins2lts-mc, 0.813: Est. total memory use: 0.0MB (~8192.0MB paged-in)
==2676== Warning: set address range perms: large range [0x239600000, 0x2b9600000) (noaccess)
==2676== Warning: set address range perms: large range [0x39600000, 0x239600000) (noaccess)
==2676== 
==2676== HEAP SUMMARY:
==2676==     in use at exit: 33,764,823,198 bytes in 994 blocks
==2676==   total heap usage: 104,894 allocs, 103,900 frees, 33,824,307,591 bytes allocated
==2676== 
==2676== LEAK SUMMARY:
==2676==    definitely lost: 2,869 bytes in 148 blocks
==2676==    indirectly lost: 45,688 bytes in 47 blocks
==2676==      possibly lost: 33,764,613,161 bytes in 85 blocks
==2676==    still reachable: 161,480 bytes in 714 blocks
==2676==         suppressed: 0 bytes in 0 blocks
==2676== Rerun with --leak-check=full to see details of leaked memory
==2676== 
==2676== For counts of detected and suppressed errors, rerun with: -v
==2676== Use --track-origins=yes to see where uninitialised values come from
==2676== ERROR SUMMARY: 3 errors from 3 contexts (suppressed: 0 from 0)

These errors go away with this patch. Still can't find the counter-example unfortunately.

yanntm commented 4 years ago

afaics, this bug still exists in the most recent LTSmin, sorry to reopen the issue, but it is not patched.