search

utwente-fmt / ltsmin

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

more valgrind warnings : reading freed memory #143

Closed yanntm closed 6 years ago

yanntm commented 7 years ago

These errors are not too critical as they happen at deinit time, when the result is already computed essentially

Same example used in my other issue, see https://github.com/utwente-fmt/ltsmin/issues/109

A trace on valgrind :

[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=cndfs --procs=1
==27631== Memcheck, a memory error detector
==27631== Copyright (C) 2002-2015, and GNU GPL'd, by Julian Seward et al.
==27631== Using Valgrind-3.12.0 and LibVEX; rerun with -h for copyright info
==27631== Command: src/pins2lts-mc/pins2lts-mc ../ITS-Tools-pnmcc/INPUTS/Railroad-PT-005/gal.so --when --ltl X(\<\>(X([]((LTLAP15==true))))) --strategy=cndfs --procs=1
==27631== 
pins2lts-mc, 0.039: Registering PINS so language module
pins2lts-mc, 0.067, ** error **: Unable to open cgroup memory limit file /sys/fs/cgroup/memory/memory.limit_in_bytes: No such file or directory
==27631== Warning: set address range perms: large range [0x804f6d040, 0xfded45840) (undefined)
pins2lts-mc, 0.073: Loading model from ../ITS-Tools-pnmcc/INPUTS/Railroad-PT-005/gal.so
pins2lts-mc, 0.086: library has no initializer
pins2lts-mc, 0.087: loading model GAL
pins2lts-mc, 0.134: completed loading model GAL
pins2lts-mc, 0.136: LTL layer: formula: X(<>(X([]((LTLAP15==true)))))
pins2lts-mc, 0.138: "X(<>(X([]((LTLAP15==true)))))" is not a file, parsing as formula...
pins2lts-mc, 0.173: Using Spin LTL semantics
pins2lts-mc, 0.223: buchi has 2 states
==27631== Warning: set address range perms: large range [0x39600000, 0x239600000) (defined)
==27631== Warning: set address range perms: large range [0x239600000, 0x2b9600000) (defined)
pins2lts-mc, 0.304: There are 76 state labels and 1 edge labels
pins2lts-mc, 0.305: State length is 55, there are 60 groups
pins2lts-mc, 0.305: Running cndfs using 1 core (sequential)
pins2lts-mc, 0.305: Using a tree table with 2^30 elements
pins2lts-mc, 0.306: Successor permutation: dynamic
pins2lts-mc, 0.306: Global bits: 2, count bits: 0, local bits: 0
pins2lts-mc, 0.721: [Blue] 876 levels 1000 states 4097 transitions
pins2lts-mc, 1.152:  
pins2lts-mc, 1.153: Explored 1853 states 7739 transitions, fanout: 4.176
pins2lts-mc, 1.158: Total exploration time 0.850 sec (0.850 sec minimum, 0.850 sec on average)
pins2lts-mc, 1.160: States per second: 2180, Transitions per second: 9105
pins2lts-mc, 1.164:  
pins2lts-mc, 1.164: State space has 1853 states, 0 are accepting
pins2lts-mc, 1.165: cndfs_1 (permutation: dynamic) stats:
pins2lts-mc, 1.166: blue states: 1853 (100.00%), transitions: 0 (per worker)
pins2lts-mc, 1.167: red states: 0 (0.00%), bogus: 0  (0.00%), transitions: 0, waits: 0 (0.00 sec)
pins2lts-mc, 1.167: all-red states: 0 (0.00%), bogus 0 (0.00%)
pins2lts-mc, 1.168:  
pins2lts-mc, 1.168: Total memory used for local state coloring: 0.0MB
pins2lts-mc, 1.170:  
pins2lts-mc, 1.170: Queue width: 8B, total height: 1304, memory: 0.01MB
pins2lts-mc, 1.171: Tree memory: 0.0MB, 21.8 B/state, compr.: 9.8%
pins2lts-mc, 1.172: Tree fill ratio (roots/leafs): 0.0%/0.0%
pins2lts-mc, 1.173: Stored 56 string chucks using 0MB
pins2lts-mc, 1.175: Total memory used for chunk indexing: 0MB
pins2lts-mc, 1.175: Est. total memory use: 0.0MB (~8192.0MB paged-in)
==27631== Invalid read of size 8
==27631==    at 0x4236F1: cndfs_local_deinit (cndfs.c:617)
==27631==    by 0x4208FC: alg_local_deinit (algorithm.c:90)
==27631==    by 0x41D0E2: run_deinit (run.c:92)
==27631==    by 0x418A2C: deinit_all (pins2lts-mc.c:183)
==27631==    by 0x418AE6: main (pins2lts-mc.c:216)
==27631==  Address 0x6846658 is 280 bytes inside a block of size 320 free'd
==27631==    at 0x4C29060: free (vg_replace_malloc.c:530)
==27631==    by 0x469196: RTfree (hre_malloc.c:139)
==27631==    by 0x427F97: ndfs_local_deinit (ndfs.c:234)
==27631==    by 0x4236EC: cndfs_local_deinit (cndfs.c:616)
==27631==    by 0x4208FC: alg_local_deinit (algorithm.c:90)
==27631==    by 0x41D0E2: run_deinit (run.c:92)
==27631==    by 0x418A2C: deinit_all (pins2lts-mc.c:183)
==27631==    by 0x418AE6: main (pins2lts-mc.c:216)
==27631==  Block was alloc'd at
==27631==    at 0x4C29CF8: calloc (vg_replace_malloc.c:711)
==27631==    by 0x468B7B: RTmallocZero (hre_malloc.c:49)
==27631==    by 0x42361A: cndfs_local_init (cndfs.c:597)
==27631==    by 0x4204DC: alg_local_init (algorithm.c:58)
==27631==    by 0x41D1E0: run_init (run.c:118)
==27631==    by 0x41897F: local_init (pins2lts-mc.c:157)
==27631==    by 0x418A99: main (pins2lts-mc.c:205)
==27631== 
==27631== Warning: set address range perms: large range [0xd2e7068, 0x1d2e7098) (noaccess)
==27631== Warning: set address range perms: large range [0x239600000, 0x2b9600000) (noaccess)
==27631== Warning: set address range perms: large range [0x39600000, 0x239600000) (noaccess)
==27631== 
==27631== HEAP SUMMARY:
==27631==     in use at exit: 34,167,460,528 bytes in 1,004 blocks
==27631==   total heap usage: 104,917 allocs, 103,913 frees, 34,525,746,999 bytes allocated
==27631== 
==27631== LEAK SUMMARY:
==27631==    definitely lost: 134,220,741 bytes in 152 blocks
==27631==    indirectly lost: 29,624 bytes in 52 blocks
==27631==      possibly lost: 34,033,048,617 bytes in 86 blocks
==27631==    still reachable: 161,546 bytes in 714 blocks
==27631==         suppressed: 0 bytes in 0 blocks
==27631== Rerun with --leak-check=full to see details of leaked memory
==27631== 
==27631== For counts of detected and suppressed errors, rerun with: -v
==27631== ERROR SUMMARY: 1 errors from 1 contexts (suppressed: 0 from 0)
alaarman commented 6 years ago

Fixed in 9909d85ae88335f7387006f127990bb256d16648. Thanks for reporting.