Skip to content

Commit dcc907a

Browse files
author
Daniel Kroening
committed
introduce unwindsett for unwinding limits
1 parent da61186 commit dcc907a

File tree

9 files changed

+156
-124
lines changed

9 files changed

+156
-124
lines changed

‎src/cbmc/Makefile

+4-3
Original file line numberDiff line numberDiff line change
@@ -30,9 +30,6 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
3030
../pointer-analysis/add_failed_symbols$(OBJEXT) \
3131
../pointer-analysis/rewrite_index$(OBJEXT) \
3232
../pointer-analysis/goto_program_dereference$(OBJEXT) \
33-
../goto-instrument/reachability_slicer$(OBJEXT) \
34-
../goto-instrument/full_slicer$(OBJEXT) \
35-
../goto-instrument/nondet_static$(OBJEXT) \
3633
../goto-instrument/cover$(OBJEXT) \
3734
../goto-instrument/cover_basic_blocks$(OBJEXT) \
3835
../goto-instrument/cover_filter$(OBJEXT) \
@@ -43,6 +40,10 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
4340
../goto-instrument/cover_instrument_mcdc$(OBJEXT) \
4441
../goto-instrument/cover_instrument_other$(OBJEXT) \
4542
../goto-instrument/cover_util$(OBJEXT) \
43+
../goto-instrument/reachability_slicer$(OBJEXT) \
44+
../goto-instrument/nondet_static$(OBJEXT) \
45+
../goto-instrument/full_slicer$(OBJEXT) \
46+
../goto-instrument/unwindset$(OBJEXT) \
4647
../analyses/analyses$(LIBEXT) \
4748
../langapi/langapi$(LIBEXT) \
4849
../xmllang/xmllang$(LIBEXT) \

‎src/cbmc/bmc.cpp

+2-40
Original file line numberDiff line numberDiff line change
@@ -15,8 +15,6 @@ Author: Daniel Kroening, [email protected]
1515
#include <iostream>
1616

1717
#include <util/exit_codes.h>
18-
#include <util/string2int.h>
19-
#include <util/string_utils.h>
2018

2119
#include <langapi/language_util.h>
2220

@@ -319,7 +317,8 @@ void bmct::setup()
319317

320318
symex.last_source_location.make_nil();
321319

322-
setup_unwind();
320+
symex.unwindset.parse_unwind(options.get_option("unwind"));
321+
symex.unwindset.parse_unwindset(options.get_option("unwindset"));
323322
}
324323

325324
safety_checkert::resultt bmct::execute(
@@ -549,43 +548,6 @@ safety_checkert::resultt bmct::stop_on_fail(prop_convt &prop_conv)
549548
}
550549
}
551550

552-
void bmct::setup_unwind()
553-
{
554-
const std::string &set=options.get_option("unwindset");
555-
std::vector<std::string> unwindset_loops;
556-
split_string(set, ',', unwindset_loops, true, true);
557-
558-
for(auto &val : unwindset_loops)
559-
{
560-
unsigned thread_nr=0;
561-
bool thread_nr_set=false;
562-
563-
if(!val.empty() &&
564-
isdigit(val[0]) &&
565-
val.find(":")!=std::string::npos)
566-
{
567-
std::string nr=val.substr(0, val.find(":"));
568-
thread_nr=unsafe_string2unsigned(nr);
569-
thread_nr_set=true;
570-
val.erase(0, nr.size()+1);
571-
}
572-
573-
if(val.rfind(":")!=std::string::npos)
574-
{
575-
std::string id=val.substr(0, val.rfind(":"));
576-
long uw=unsafe_string2int(val.substr(val.rfind(":")+1));
577-
578-
if(thread_nr_set)
579-
symex.set_unwind_thread_loop_limit(thread_nr, id, uw);
580-
else
581-
symex.set_unwind_loop_limit(id, uw);
582-
}
583-
}
584-
585-
if(options.get_option("unwind")!="")
586-
symex.set_unwind_limit(options.get_unsigned_int_option("unwind"));
587-
}
588-
589551
/// Perform core BMC, using an abstract model to supply GOTO function bodies
590552
/// (perhaps created on demand).
591553
/// \param opts: command-line options affecting BMC

‎src/cbmc/bmc.h

-2
Original file line numberDiff line numberDiff line change
@@ -183,8 +183,6 @@ class bmct:public safety_checkert
183183
const goto_functionst &,
184184
prop_convt &);
185185

186-
// unwinding
187-
virtual void setup_unwind();
188186
void do_conversion();
189187

190188
virtual void freeze_program_variables();

‎src/cbmc/symex_bmc.cpp

+8-36
Original file line numberDiff line numberDiff line change
@@ -25,8 +25,6 @@ symex_bmct::symex_bmct(
2525
path_storaget &path_storage)
2626
: goto_symext(mh, outer_symbol_table, _target, path_storage),
2727
record_coverage(false),
28-
max_unwind(0),
29-
max_unwind_is_set(false),
3028
symex_coverage(ns)
3129
{
3230
}
@@ -131,25 +129,12 @@ bool symex_bmct::get_unwind(
131129
// / --unwind options to decide:
132130
if(abort_unwind_decision.is_unknown())
133131
{
134-
// We use the most specific limit we have,
135-
// and 'infinity' when we have none.
132+
auto limit=unwindset.get_limit(id, source.thread_nr);
136133

137-
loop_limitst &this_thread_limits=
138-
thread_loop_limits[source.thread_nr];
139-
140-
loop_limitst::const_iterator l_it=this_thread_limits.find(id);
141-
if(l_it!=this_thread_limits.end())
142-
this_loop_limit=l_it->second;
134+
if(!limit.has_value())
135+
abort_unwind_decision = tvt(false);
143136
else
144-
{
145-
l_it=loop_limits.find(id);
146-
if(l_it!=loop_limits.end())
147-
this_loop_limit=l_it->second;
148-
else if(max_unwind_is_set)
149-
this_loop_limit=max_unwind;
150-
}
151-
152-
abort_unwind_decision = tvt(unwind >= this_loop_limit);
137+
abort_unwind_decision = tvt(unwind >= *limit);
153138
}
154139

155140
INVARIANT(
@@ -187,25 +172,12 @@ bool symex_bmct::get_unwind_recursion(
187172
// / --unwind options to decide:
188173
if(abort_unwind_decision.is_unknown())
189174
{
190-
// We use the most specific limit we have,
191-
// and 'infinity' when we have none.
192-
193-
loop_limitst &this_thread_limits=
194-
thread_loop_limits[thread_nr];
175+
auto limit=unwindset.get_limit(id, thread_nr);
195176

196-
loop_limitst::const_iterator l_it=this_thread_limits.find(id);
197-
if(l_it!=this_thread_limits.end())
198-
this_loop_limit=l_it->second;
177+
if(!limit.has_value())
178+
abort_unwind_decision = tvt(false);
199179
else
200-
{
201-
l_it=loop_limits.find(id);
202-
if(l_it!=loop_limits.end())
203-
this_loop_limit=l_it->second;
204-
else if(max_unwind_is_set)
205-
this_loop_limit=max_unwind;
206-
}
207-
208-
abort_unwind_decision = tvt(unwind>this_loop_limit);
180+
abort_unwind_decision = tvt(unwind > *limit);
209181
}
210182

211183
INVARIANT(

‎src/cbmc/symex_bmc.h

+5-40
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,8 @@ Author: Daniel Kroening, [email protected]
1818
#include <goto-symex/path_storage.h>
1919
#include <goto-symex/goto_symex.h>
2020

21+
#include <goto-instrument/unwindset.h>
22+
2123
#include "symex_coverage.h"
2224

2325
class symex_bmct: public goto_symext
@@ -32,29 +34,6 @@ class symex_bmct: public goto_symext
3234
// To show progress
3335
source_locationt last_source_location;
3436

35-
// Control unwinding.
36-
37-
void set_unwind_limit(unsigned limit)
38-
{
39-
max_unwind=limit;
40-
max_unwind_is_set=true;
41-
}
42-
43-
void set_unwind_thread_loop_limit(
44-
unsigned thread_nr,
45-
const irep_idt &id,
46-
unsigned limit)
47-
{
48-
thread_loop_limits[thread_nr][id]=limit;
49-
}
50-
51-
void set_unwind_loop_limit(
52-
const irep_idt &id,
53-
unsigned limit)
54-
{
55-
loop_limits[id]=limit;
56-
}
57-
5837
/// Loop unwind handlers take the function ID and loop number, the unwind
5938
/// count so far, and an out-parameter specifying an advisory maximum, which
6039
/// they may set. If set the advisory maximum is set it is *only* used to
@@ -101,26 +80,12 @@ class symex_bmct: public goto_symext
10180

10281
bool record_coverage;
10382

104-
protected:
105-
// We have
106-
// 1) a global limit (max_unwind)
107-
// 2) a limit per loop, all threads
108-
// 3) a limit for a particular thread.
109-
// 4) zero or more handler functions that can special-case particular
110-
// functions or loops
111-
// We use the most specific of the above.
112-
113-
unsigned max_unwind;
114-
bool max_unwind_is_set;
115-
116-
typedef std::unordered_map<irep_idt, unsigned> loop_limitst;
117-
loop_limitst loop_limits;
118-
119-
typedef std::map<unsigned, loop_limitst> thread_loop_limitst;
120-
thread_loop_limitst thread_loop_limits;
83+
unwindsett unwindset;
12184

85+
protected:
12286
/// Callbacks that may provide an unwind/do-not-unwind decision for a loop
12387
std::vector<loop_unwind_handlert> loop_unwind_handlers;
88+
12489
/// Callbacks that may provide an unwind/do-not-unwind decision for a
12590
/// recursive call
12691
std::vector<recursion_unwind_handlert> recursion_unwind_handlers;

‎src/goto-instrument/Makefile

+1
Original file line numberDiff line numberDiff line change
@@ -61,6 +61,7 @@ SRC = accelerate/accelerate.cpp \
6161
undefined_functions.cpp \
6262
uninitialized.cpp \
6363
unwind.cpp \
64+
unwindset.cpp \
6465
wmm/abstract_event.cpp \
6566
wmm/cycle_collection.cpp \
6667
wmm/data_dp.cpp \

‎src/goto-instrument/unwindset.cpp

+79
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,79 @@
1+
/*******************************************************************\
2+
3+
Module: Loop unwinding setup
4+
5+
Author: Daniel Kroening, [email protected]
6+
7+
\*******************************************************************/
8+
9+
#include "unwindset.h"
10+
11+
#include <util/string2int.h>
12+
#include <util/string_utils.h>
13+
14+
void unwindsett::parse_unwind(const std::string &unwind)
15+
{
16+
if(!unwind.empty())
17+
global_limit = unsafe_string2unsigned(unwind);
18+
}
19+
20+
void unwindsett::parse_unwindset(const std::string &unwindset)
21+
{
22+
std::vector<std::string> unwindset_loops;
23+
split_string(unwindset, ',', unwindset_loops, true, true);
24+
25+
for(auto &val : unwindset_loops)
26+
{
27+
unsigned thread_nr = 0;
28+
bool thread_nr_set = false;
29+
30+
if(!val.empty() && isdigit(val[0]) && val.find(":") != std::string::npos)
31+
{
32+
std::string nr = val.substr(0, val.find(":"));
33+
thread_nr = unsafe_string2unsigned(nr);
34+
thread_nr_set = true;
35+
val.erase(0, nr.size() + 1);
36+
}
37+
38+
if(val.rfind(":") != std::string::npos)
39+
{
40+
std::string id = val.substr(0, val.rfind(":"));
41+
std::string uw_string = val.substr(val.rfind(":") + 1);
42+
43+
// the below initialisation makes g++-5 happy
44+
optionalt<unsigned> uw(0);
45+
46+
if(uw_string.empty())
47+
uw = { };
48+
else
49+
uw = unsafe_string2unsigned(uw_string);
50+
51+
if(thread_nr_set)
52+
thread_loop_map[std::pair<irep_idt, unsigned>(id, thread_nr)] = uw;
53+
else
54+
loop_map[id] = uw;
55+
}
56+
}
57+
}
58+
59+
optionalt<unsigned>
60+
unwindsett::get_limit(const irep_idt &loop_id, unsigned thread_nr) const
61+
{
62+
// We use the most specific limit we have
63+
64+
// thread x loop
65+
auto tl_it =
66+
thread_loop_map.find(std::pair<irep_idt, unsigned>(loop_id, thread_nr));
67+
68+
if(tl_it != thread_loop_map.end())
69+
return tl_it->second;
70+
71+
// loop
72+
auto l_it = loop_map.find(loop_id);
73+
74+
if(l_it != loop_map.end())
75+
return l_it->second;
76+
77+
// global, if any
78+
return global_limit;
79+
}

‎src/goto-instrument/unwindset.h

+53
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,53 @@
1+
/*******************************************************************\
2+
3+
Module: Loop unwinding setup
4+
5+
Author: Daniel Kroening, [email protected]
6+
7+
\*******************************************************************/
8+
9+
/// \file
10+
/// Loop unwinding
11+
12+
#ifndef CPROVER_GOTO_INSTRUMENT_UNWINDSET_H
13+
#define CPROVER_GOTO_INSTRUMENT_UNWINDSET_H
14+
15+
#include <map>
16+
#include <string>
17+
18+
#include <util/irep.h>
19+
#include <util/optional.h>
20+
21+
class unwindsett
22+
{
23+
public:
24+
// We have
25+
// 1) a global limit
26+
// 2) a limit per loop, all threads
27+
// 3) a limit for a particular thread.
28+
// We use the most specific of the above.
29+
30+
// global limit for all loops
31+
void parse_unwind(const std::string &unwind);
32+
33+
// limit for instances of a loop
34+
void parse_unwindset(const std::string &unwindset);
35+
36+
// queries
37+
optionalt<unsigned> get_limit(const irep_idt &loop, unsigned thread_id) const;
38+
39+
protected:
40+
optionalt<unsigned> global_limit;
41+
42+
// Limit for all instances of a loop.
43+
// This may have 'no value'.
44+
typedef std::map<irep_idt, optionalt<unsigned>> loop_mapt;
45+
loop_mapt loop_map;
46+
47+
// separate limits per thread
48+
using thread_loop_mapt =
49+
std::map<std::pair<irep_idt, unsigned>, optionalt<unsigned>>;
50+
thread_loop_mapt thread_loop_map;
51+
};
52+
53+
#endif // CPROVER_GOTO_INSTRUMENT_UNWINDSET_H

‎src/jbmc/Makefile

+4-3
Original file line numberDiff line numberDiff line change
@@ -17,9 +17,6 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
1717
../pointer-analysis/add_failed_symbols$(OBJEXT) \
1818
../pointer-analysis/rewrite_index$(OBJEXT) \
1919
../pointer-analysis/goto_program_dereference$(OBJEXT) \
20-
../goto-instrument/full_slicer$(OBJEXT) \
21-
../goto-instrument/reachability_slicer$(OBJEXT) \
22-
../goto-instrument/nondet_static$(OBJEXT) \
2320
../goto-instrument/cover$(OBJEXT) \
2421
../goto-instrument/cover_basic_blocks$(OBJEXT) \
2522
../goto-instrument/cover_filter$(OBJEXT) \
@@ -30,6 +27,10 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
3027
../goto-instrument/cover_instrument_mcdc$(OBJEXT) \
3128
../goto-instrument/cover_instrument_other$(OBJEXT) \
3229
../goto-instrument/cover_util$(OBJEXT) \
30+
../goto-instrument/full_slicer$(OBJEXT) \
31+
../goto-instrument/nondet_static$(OBJEXT) \
32+
../goto-instrument/reachability_slicer$(OBJEXT) \
33+
../goto-instrument/unwindset$(OBJEXT) \
3334
../analyses/analyses$(LIBEXT) \
3435
../langapi/langapi$(LIBEXT) \
3536
../xmllang/xmllang$(LIBEXT) \

0 commit comments

Comments
 (0)