search

evincarofautumn / Ward

A static analysis tool for C.
Other
26 stars 2 forks source link

Error disappears when a module is added #31

Open bgamari opened 6 years ago

bgamari commented 6 years ago

Using 05b02cf2a617886d5c064648d2ce415aa9043c86 I am seeing some rather concerning behavior when processing callmaps. I am using this configuration file:

sm_lock_held      "assume the storage manager lock is held";                
take_sm_lock      "the ability to take the storage manager lock"            
  -> ! sm_lock_held;                                                        

.enforce "sm/NonMovingMark.c";                                              
.enforce "sm/NonMovingMark.h";                                              
.enforce "sm/BlockAlloc.c";                                                 
.enforce "rts/sm/BlockAlloc.h";                                             
.enforce "Block.h";

I have two callmap files: rts/sm/BlockAlloc.c.ward.graph and rts/Capability.c.ward.graph.

Checking the Capability callmap alone correctly reports no errors:

$ ward gcc --mode=compiler --config=rts/config.ward    rts/Capability.c.ward.graph   
Loading config files...
Preprocessing and parsing...
Checking...
Warnings: 0, Errors: 0

Checking the BlockAlloc callmap alone correctly reports several errors:

$ ward gcc --mode=compiler --config=rts/config.ward rts/sm/BlockAlloc.c.ward.graph                                                                                                                                                       
Loading config files...
Preprocessing and parsing...
Checking...
rts/sm/BlockAlloc.h:13: error: missing required annotation on 'allocLargeChunk'; annotation [] is missing: [revoke(take_sm_lock),need(take_sm_lock),grant(sm_lock_held)]
includes/rts/storage/Block.h:320: error: missing required annotation on 'allocGroupOnNode_lock'; annotation [] is missing: [need(take_sm_lock)]
includes/rts/storage/Block.h:315: error: missing required annotation on 'allocGroup_lock'; annotation [] is missing: [need(take_sm_lock)]
includes/rts/storage/Block.h:317: error: missing required annotation on 'allocBlock_lock'; annotation [] is missing: [need(take_sm_lock)]
includes/rts/storage/Block.h:322: error: missing required annotation on 'allocBlockOnNode_lock'; annotation [] is missing: [need(take_sm_lock)]
includes/rts/storage/Block.h:333: error: missing required annotation on 'freeGroup_lock'; annotation [] is missing: [need(take_sm_lock)]
includes/rts/storage/Block.h:335: error: missing required annotation on 'freeChain_lock'; annotation [] is missing: [need(take_sm_lock)]
Warnings: 0, Errors: 7

However, when I check the Capability and BlockAlloc callmaps together the error vanishes:

$ ward gcc --mode=compiler --config=rts/config.ward rts/Capability.c.ward.graph rts/sm/BlockAlloc.c.ward.graph
Loading config files...
Preprocessing and parsing...
Checking...
Warnings: 0, Errors: 0

Even stranger, when I flip the order of the two the errors are again correctly reported,

$ ward gcc --mode=compiler --config=rts/config.ward rts/sm/BlockAlloc.c.ward.graph rts/Capability.c.ward.graph
Loading config files...
Preprocessing and parsing...
Checking...
rts/sm/BlockAlloc.h:13: error: missing required annotation on 'allocLargeChunk'; annotation [] is missing: [revoke(take_sm_lock),need(take_sm_lock),grant(sm_lock_held)]
includes/rts/storage/Block.h:320: error: missing required annotation on 'allocGroupOnNode_lock'; annotation [] is missing: [need(take_sm_lock)]
includes/rts/storage/Block.h:315: error: missing required annotation on 'allocGroup_lock'; annotation [] is missing: [need(take_sm_lock)]
includes/rts/storage/Block.h:317: error: missing required annotation on 'allocBlock_lock'; annotation [] is missing: [need(take_sm_lock)]
includes/rts/storage/Block.h:322: error: missing required annotation on 'allocBlockOnNode_lock'; annotation [] is missing: [need(take_sm_lock)]
includes/rts/storage/Block.h:333: error: missing required annotation on 'freeGroup_lock'; annotation [] is missing: [need(take_sm_lock)]
includes/rts/storage/Block.h:335: error: missing required annotation on 'freeChain_lock'; annotation [] is missing: [need(take_sm_lock)]
Warnings: 0, Errors: 7
bgamari commented 6 years ago

I've pushed the two necessary callmap files to https://github.com/bgamari/ward-T31-repro

bgamari commented 6 years ago

While debugging this I have noticed if I export the callgraph of the failing case I find that allocLargeChunk has no calls. This is likely why the errors aren't being reported.

bgamari commented 6 years ago

Indeed it looks like declarations aren't handled properly. Specifically, Capability.c.ward.graph contains:

(function (ident "allocLargeChunk" (node 40671 (span (source "rts/sm/BlockAlloc.h" 248117 13 9) 15 (source "rts/sm/BlockAlloc.h" 248117 13 9)))) (node 40685 (span (source "rts/sm/BlockAlloc.h" 248109 13 1) 1 (source "rts/sm/BlockAlloc.h" 248149 13 41)))                             
(actions )                                                                                                                                                                                                                                                                                
(calltree                                                                                                                                                                                                                                                                                 
))

that is, just a declaration for allocLargeChunk, which naturally has no calls.

However, BlockAlloc.c.ward.graph contains the definition of allocLargeChunk and consequently contains calls:

(function (ident "allocLargeChunk" (node 38563 (span (source "rts/sm/BlockAlloc.h" 233950 13 9) 15 (source "rts/sm/BlockAlloc.h" 233950 13 9)))) (node 38577 (span (source "rts/sm/BlockAlloc.h" 233942 13 1) 1 (source "rts/sm/BlockAlloc.h" 233982 13 41)))                             
(actions )                                                                                                                                                                                                                                                                                
(calltree                                                                                                                                                                                                                                                                                 
(call (ident "_acquire_sm_lock" (node 43174 (span (source "rts/sm/BlockAlloc.c" 256846 650 2) 16 (source "rts/sm/BlockAlloc.c" 256846 650 2)))))                                                                                                                                          
(call (ident "rts/sm/BlockAlloc.c`nodeWithLeastBlocks" (node 43180 (span (source "rts/sm/BlockAlloc.c" 256899 651 34) 19 (source "rts/sm/BlockAlloc.c" 256899 651 34)))))                                                                                                                 
(call (ident "allocLargeChunkOnNode" (node 43178 (span (source "rts/sm/BlockAlloc.c" 256877 651 12) 21 (source "rts/sm/BlockAlloc.c" 256877 651 12)))))))                                                                                                                                 
(function (ident "freeWSDeque" (node 36212 (span (source "rts/WSDeque.h" 220424 70 6) 11 (source "rts/WSDeque.h" 220424 70 6)))) (node 36222 (span (source "rts/WSDeque.h" 220419 70 1) 1 (source "rts/WSDeque.h" 220448 70 30)))                                                         
(actions )                                                                                                                                                                                                                                                                                
(calltree                                                                                                                                                                                                                                                                                 
))

It looks like depending upon the order the files are given in the declaration may override the definition.

lambdageek commented 6 years ago

I don't have a working Ward at the moment, but the first thing to check is whether this works out with simple examples smaller than the GHC rts.

The second thing to check is whether this is related to GHCs reliance on #pragma once instead of include guards and whether that's somehow messes up the graph merging. We've only ever tests on code that uses traditional include guards.

bgamari commented 6 years ago

To be clear, I described the underlying issue in my previous comment. It seems that the treatment of declarations and definitions is simply wrong.

I just pushed #35 which fixes the issue.