1 /*
2 * This file is part of the Yices SMT Solver.
3 * Copyright (C) 2017 SRI International.
4 *
5 * Yices is free software: you can redistribute it and/or modify
6 * it under the terms of the GNU General Public License as published by
7 * the Free Software Foundation, either version 3 of the License, or
8 * (at your option) any later version.
9 *
10 * Yices is distributed in the hope that it will be useful,
11 * but WITHOUT ANY WARRANTY; without even the implied warranty of
12 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
13 * GNU General Public License for more details.
14 *
15 * You should have received a copy of the GNU General Public License
16 * along with Yices. If not, see <http://www.gnu.org/licenses/>.
17 */
18
19 /*
20 * Support for printing trace/messages depending on a verbosity level.
21 */
22
23 #ifndef __TRACER_H
24 #define __TRACER_H
25
26 #include <stdio.h>
27 #include <stdint.h>
28 #include <stdbool.h>
29
30 #include "io/yices_pp.h"
31 #include "terms/terms.h"
32 #include "terms/types.h"
33
34
35 /*
36 * Tracer structure:
37 * - an open FILE
38 * + an optional pretty printing object
39 * + a verbosity level (higher means more verbose)
40 * + error codes if printing fails
41 */
42 typedef struct tracer_s {
43 FILE *file;
44 yices_pp_t *pp;
45 uint32_t vlevel;
46 bool print_failed; // true if printing fails
47 int err_code; // copy of errno when failure was reported
48 pvector_t trace_tags; // list of tags
49 } tracer_t;
50
51
52 /*
53 * Initialize to defaults
54 */
init_trace(tracer_t * tracer)55 static inline void init_trace(tracer_t *tracer) {
56 tracer->file = stderr;
57 tracer->pp = NULL;
58 tracer->vlevel = 0;
59 tracer->print_failed = false;
60 tracer->err_code = 0;
61 init_pvector(&tracer->trace_tags, 5);
62 }
63
64
65 /*
66 * Set verbosity level
67 */
set_trace_vlevel(tracer_t * tracer,uint32_t level)68 static inline void set_trace_vlevel(tracer_t *tracer, uint32_t level) {
69 tracer->vlevel = level;
70 }
71
72 /*
73 * Enable a tag to trace.
74 */
enable_trace_tag(tracer_t * tracer,const char * tag)75 static inline void enable_trace_tag(tracer_t *tracer, const char* tag) {
76 pvector_push(&tracer->trace_tags, strdup(tag));
77 }
78
79 /*
80 * Check whether the verbosity level is at least lvl
81 * - return false if trace is NULL
82 */
tracing(tracer_t * tracer,uint32_t lvl)83 static inline bool tracing(tracer_t *tracer, uint32_t lvl) {
84 return tracer != NULL && tracer->vlevel >= lvl;
85 }
86
87 /*
88 * Check whether the tracing tag has been enabled.
89 * - return false if trace is NULL;
90 */
91 bool tracing_tag(tracer_t *tracer, const char *tag);
92
93 /*
94 * Change output file:
95 * - f must be open and writable
96 * - close the current file if it's not stderr
97 * - reset the print_failed and err_code flags
98 * - also close and delete the tracer->pp object if there is one
99 */
100 extern void set_trace_file(tracer_t *tracer, FILE *f);
101
102 /*
103 * Close/delete the tracer
104 * - close the current file if it's not stderr
105 * - close and delete the pp object if any
106 */
107 extern void delete_trace(tracer_t *tracer);
108
109 /*
110 * Output functions:
111 * - if tracer is NULL, they do nothing
112 * - otherwise, they print stuff to tracer->file provided
113 * tracer->vlevel >= level
114 * - both trace_printf and trace_puts call fflush
115 *
116 * - if the output fails then tracer->print_failed is set to true
117 * and tracer->err_code is set to errno
118 */
119
120 /*
121 * Formatted output (as in fprintf)
122 * - level = verbosity
123 * - fmt = a format string as in printf
124 * - rest = stuff to print (as in prinf too)
125 */
126 extern void trace_printf(tracer_t *tracer, uint32_t level, const char *format, ...)
127 __attribute__ ((format (printf, 3, 4)));
128
129
130 /*
131 * Print string s if tracer->vlevel >= level
132 * (same as fputs)
133 */
134 extern void trace_puts(tracer_t *tracer, uint32_t level, const char *s);
135
136
137 /*
138 * Newline
139 */
140 extern void trace_newline(tracer_t *trace, uint32_t level);
141
142
143 /*
144 * Pretty printing:
145 * - the tracer->pp object is created and initialized on the
146 * first call to one of these functions (provided tracer->vlevel >= level)
147 */
148
149 /*
150 * Pretty printing of term t + newline
151 * - tbl = corresponding term table
152 * - use the default printing area
153 */
154 extern void trace_pp_term(tracer_t *trace, uint32_t level, term_table_t *tbl, term_t t);
155
156 /*
157 * Pretty printing of type tau + newline
158 * - tbl = corresponding type table
159 * - use the default printing area
160 */
161 extern void trace_pp_type(tracer_t *traced, uint32_t level, type_table_t *tbl, type_t tau);
162
163
164 #endif /* __TRACER_H */
165