1+ using System . Collections . Generic ;
2+ using System . Diagnostics ;
3+
4+ namespace Microsoft . Boogie ;
5+
6+ /// <summary>
7+ /// Add `{:id ...}` attributes to all assertions, assumptions, requires
8+ /// clauses, ensures clauses, and call statements so that verification
9+ /// coverage tracking is possible. This exists primarily to support the
10+ /// automatic detection of vacuous proofs in the case where no front
11+ /// end has added these already.
12+ /// </summary>
13+ public class CoverageAnnotator : StandardVisitor
14+ {
15+ private int idCount = 0 ;
16+ private string currentImplementation ;
17+ private Dictionary < string , ISet < string > > implementationGoalIds = new ( ) ;
18+ private Dictionary < string , Absy > idMap = new ( ) ;
19+
20+ private void AddImplementationGoalId ( string id )
21+ {
22+ implementationGoalIds [ currentImplementation ] . Add ( id ) ;
23+ }
24+
25+ private void AddIdIfMissing ( ICarriesAttributes node , bool isGoal )
26+ {
27+ Absy absy = node as Absy ;
28+ if ( absy == null ) {
29+ return ;
30+ }
31+ var idStr = node . FindStringAttribute ( "id" ) ;
32+ if ( idStr == null ) {
33+ idStr = $ "id_l{ absy . tok . line } _c{ absy . tok . col } _{ NodeType ( node ) } _{ idCount } ";
34+ idCount ++ ;
35+ }
36+ idMap . Add ( idStr , absy ) ;
37+ if ( isGoal ) {
38+ AddImplementationGoalId ( idStr ) ;
39+ }
40+ node . AddStringAttribute ( absy . tok , "id" , idStr ) ;
41+ }
42+
43+ private string NodeType ( ICarriesAttributes node )
44+ {
45+ return node switch
46+ {
47+ Requires _ => "requires" ,
48+ Ensures _ => "ensures" ,
49+ AssertCmd _ => "assert" ,
50+ AssumeCmd _ => "assume" ,
51+ CallCmd _ => "call" ,
52+ _ => "other"
53+ } ;
54+ }
55+
56+ /// <summary>
57+ /// Get the set of IDs that correspond to goals within the named
58+ /// implementation.
59+ /// </summary>
60+ /// <param name="implName">The name of the implementation.</param>
61+ /// <returns>The IDs for all goal elements within the implementation.</returns>
62+ public ISet < string > GetImplementationGoalIds ( string implName ) => implementationGoalIds [ implName ] ;
63+
64+ /// <summary>
65+ /// Get the AST node corresponding to the given ID.
66+ /// </summary>
67+ /// <param name="idStr">The `id` attribute placed on an AST node.</param>
68+ /// <returns>The node where that `id` occurs.</returns>
69+ public Absy GetIdNode ( string idStr ) => idMap [ idStr ] ;
70+
71+ public override Implementation VisitImplementation ( Implementation node )
72+ {
73+ currentImplementation = node . Name ;
74+ implementationGoalIds . TryAdd ( currentImplementation , new HashSet < string > ( ) ) ;
75+ return base . VisitImplementation ( node ) ;
76+ }
77+
78+ public override Cmd VisitAssertCmd ( AssertCmd node )
79+ {
80+ if ( node . Expr is LiteralExpr { IsTrue : true } ) {
81+ return node ;
82+ }
83+
84+ AddIdIfMissing ( node , true ) ;
85+ return base . VisitAssertCmd ( node ) ;
86+ }
87+
88+ public override Cmd VisitAssumeCmd ( AssumeCmd node )
89+ {
90+ AddIdIfMissing ( node , false ) ;
91+ return base . VisitAssumeCmd ( node ) ;
92+ }
93+
94+ public override Cmd VisitCallCmd ( CallCmd node )
95+ {
96+ AddIdIfMissing ( node , false ) ;
97+ return base . VisitCallCmd ( node ) ;
98+ }
99+
100+ public override Requires VisitRequires ( Requires requires )
101+ {
102+ AddIdIfMissing ( requires , false ) ;
103+ return base . VisitRequires ( requires ) ;
104+ }
105+
106+ public override Ensures VisitEnsures ( Ensures ensures )
107+ {
108+ if ( ensures . Free ) {
109+ return ensures ;
110+ }
111+
112+ AddIdIfMissing ( ensures , true ) ;
113+ return base . VisitEnsures ( ensures ) ;
114+ }
115+ }
0 commit comments