Skip to content

Commit 6e94c41

Browse files
author
Daniel Kroening
authored
Merge pull request #312 from tautschnig/dirty-variables
Treat local dirty variables as shared ones
2 parents 98c4526 + f56466c commit 6e94c41

16 files changed

+217
-110
lines changed

‎regression/cbmc-concurrency/dirty_local1/main.c

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
int * global_ptr;
2+
3+
void f()
4+
{
5+
*global_ptr=42;
6+
}
7+
8+
int main()
9+
{
10+
int a=0;
11+
global_ptr=&a;
12+
__CPROVER_ASYNC_1: f();
13+
assert(a==0);
14+
}
15+

‎regression/cbmc-concurrency/dirty_local1/test.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main.c
3+
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^VERIFICATION FAILED$
7+
--
8+
^warning: ignoring

‎regression/cbmc-concurrency/dirty_local2/main.c

Lines changed: 98 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,98 @@
1+
typedef unsigned bool;
2+
3+
#define true 1
4+
#define false 0
5+
6+
typedef char Register;
7+
8+
enum RegisterId
9+
{
10+
SIGNAL_REG_ID = 0,
11+
DATA_A_REG_ID = 1,
12+
13+
REG_NR = 2
14+
};
15+
16+
typedef enum RegisterId RegisterId;
17+
18+
struct Firmware;
19+
typedef void (*InterruptHandler)(struct Firmware *fw, RegisterId reg_id);
20+
21+
struct Hardware
22+
{
23+
struct Firmware* fw;
24+
25+
Register regs[REG_NR];
26+
bool is_on;
27+
28+
InterruptHandler interrupt_handler;
29+
};
30+
31+
Register read_data_register(struct Hardware *hw, RegisterId reg_id)
32+
{
33+
if (!hw->is_on)
34+
return '\0';
35+
36+
Register reg = hw->regs[reg_id];
37+
hw->regs[SIGNAL_REG_ID] &= ~reg_id;
38+
39+
return reg;
40+
}
41+
42+
void write_data_register(struct Hardware *hw, RegisterId reg_id, Register data)
43+
{
44+
check_data_register(reg_id);
45+
46+
if (!hw->is_on)
47+
return;
48+
49+
hw->regs[reg_id] = data;
50+
hw->regs[SIGNAL_REG_ID] |= reg_id;
51+
52+
__CPROVER_ASYNC_1: hw->interrupt_handler(hw->fw, reg_id);
53+
}
54+
55+
struct Firmware
56+
{
57+
struct Hardware* hw;
58+
};
59+
60+
void handle_interrupt(struct Firmware *fw, RegisterId reg_id)
61+
{
62+
assert(reg_id == DATA_A_REG_ID);
63+
read_data_register(fw->hw, DATA_A_REG_ID);
64+
}
65+
66+
void poll(struct Firmware *fw)
67+
{
68+
char byte;
69+
if (byte == '\0')
70+
{
71+
enable_interrupts(fw->hw, handle_interrupt);
72+
return;
73+
}
74+
}
75+
76+
void write_reg_a(struct Hardware *hw)
77+
{
78+
write_data_register(hw, DATA_A_REG_ID, nondet_char());
79+
}
80+
81+
int main(void)
82+
{
83+
// trivial bug
84+
assert(false);
85+
86+
struct Hardware hardware;
87+
struct Hardware* hw = &hardware;
88+
89+
struct Firmware firmware;
90+
struct Firmware* fw = &firmware;
91+
92+
firmware.hw = hw;
93+
hardware.fw = fw;
94+
95+
__CPROVER_ASYNC_1: write_reg_a(hw);
96+
97+
return 0;
98+
}

‎regression/cbmc-concurrency/dirty_local2/test.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main.c
3+
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^VERIFICATION FAILED$
7+
--
8+
^warning: ignoring

‎src/goto-symex/goto_symex_state.cpp

Lines changed: 20 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,8 @@ Author: Daniel Kroening, [email protected]
1313
#include <util/std_expr.h>
1414
#include <util/prefix.h>
1515

16+
#include <analyses/dirty.h>
17+
1618
#include "goto_symex_state.h"
1719

1820
/*******************************************************************\
@@ -31,7 +33,8 @@ goto_symex_statet::goto_symex_statet():
3133
depth(0),
3234
symex_target(NULL),
3335
atomic_section_id(0),
34-
record_events(true)
36+
record_events(true),
37+
dirty(0)
3538
{
3639
threads.resize(1);
3740
new_frame();
@@ -640,17 +643,16 @@ bool goto_symex_statet::l2_thread_read_encoding(
640643
ssa_exprt &expr,
641644
const namespacet &ns)
642645
{
643-
if(!record_events)
644-
return false;
645-
646646
// do we have threads?
647647
if(threads.size()<=1)
648648
return false;
649649

650650
// is it a shared object?
651+
assert(dirty!=0);
651652
const irep_idt &obj_identifier=expr.get_object_name();
652653
if(obj_identifier=="goto_symex::\\guard" ||
653-
!ns.lookup(obj_identifier).is_shared())
654+
(!ns.lookup(obj_identifier).is_shared() &&
655+
!(*dirty)(obj_identifier)))
654656
return false;
655657

656658
ssa_exprt ssa_l1=expr;
@@ -754,9 +756,18 @@ bool goto_symex_statet::l2_thread_read_encoding(
754756
return true;
755757
}
756758

757-
// produce a fresh L2 name
758759
if(level2.current_names.find(l1_identifier)==level2.current_names.end())
759760
level2.current_names[l1_identifier]=std::make_pair(ssa_l1, 0);
761+
762+
// No event and no fresh index, but avoid constant propagation
763+
if(!record_events)
764+
{
765+
set_ssa_indices(ssa_l1, ns, L2);
766+
expr=ssa_l1;
767+
return true;
768+
}
769+
770+
// produce a fresh L2 name
760771
level2.increase_counter(l1_identifier);
761772
set_ssa_indices(ssa_l1, ns, L2);
762773
expr=ssa_l1;
@@ -792,9 +803,11 @@ bool goto_symex_statet::l2_thread_write_encoding(
792803
return false;
793804

794805
// is it a shared object?
806+
assert(dirty!=0);
795807
const irep_idt &obj_identifier=expr.get_object_name();
796808
if(obj_identifier=="goto_symex::\\guard" ||
797-
!ns.lookup(obj_identifier).is_shared())
809+
(!ns.lookup(obj_identifier).is_shared() &&
810+
!(*dirty)(obj_identifier)))
798811
return false; // not shared
799812

800813
// see whether we are within an atomic section

‎src/goto-symex/goto_symex_state.h

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -21,6 +21,8 @@ Author: Daniel Kroening, [email protected]
2121

2222
#include "symex_target.h"
2323

24+
class dirtyt;
25+
2426
// central data structure: state
2527
class goto_symex_statet
2628
{
@@ -331,6 +333,7 @@ class goto_symex_statet
331333

332334
void switch_to_thread(unsigned t);
333335
bool record_events;
336+
const dirtyt * dirty;
334337
};
335338

336339
#endif // CPROVER_GOTO_SYMEX_GOTO_SYMEX_STATE_H

‎src/goto-symex/memory_model_pso.cpp

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -51,19 +51,19 @@ bool memory_model_psot::program_order_is_relaxed(
5151
partial_order_concurrencyt::event_it e1,
5252
partial_order_concurrencyt::event_it e2) const
5353
{
54-
assert(is_shared_read(e1) || is_shared_write(e1));
55-
assert(is_shared_read(e2) || is_shared_write(e2));
54+
assert(e1->is_shared_read() || e1->is_shared_write());
55+
assert(e2->is_shared_read() || e2->is_shared_write());
5656

5757
// no po relaxation within atomic sections
5858
if(e1->atomic_section_id!=0 &&
5959
e1->atomic_section_id==e2->atomic_section_id)
6060
return false;
6161

6262
// no relaxation if induced wsi
63-
if(is_shared_write(e1) && is_shared_write(e2) &&
63+
if(e1->is_shared_write() && e2->is_shared_write() &&
6464
address(e1)==address(e2))
6565
return false;
6666

6767
// only read/read and read/write are maintained
68-
return is_shared_write(e1);
68+
return e1->is_shared_write();
6969
}

‎src/goto-symex/memory_model_sc.cpp

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -69,8 +69,8 @@ bool memory_model_sct::program_order_is_relaxed(
6969
partial_order_concurrencyt::event_it e1,
7070
partial_order_concurrencyt::event_it e2) const
7171
{
72-
assert(is_shared_read(e1) || is_shared_write(e1));
73-
assert(is_shared_read(e2) || is_shared_write(e2));
72+
assert(e1->is_shared_read() || e1->is_shared_write());
73+
assert(e2->is_shared_read() || e2->is_shared_write());
7474

7575
return false;
7676
}
@@ -99,10 +99,10 @@ void memory_model_sct::build_per_thread_map(
9999
e_it++)
100100
{
101101
// concurreny-related?
102-
if(!is_shared_read(e_it) &&
103-
!is_shared_write(e_it) &&
104-
!is_spawn(e_it) &&
105-
!is_memory_barrier(e_it)) continue;
102+
if(!e_it->is_shared_read() &&
103+
!e_it->is_shared_write() &&
104+
!e_it->is_spawn() &&
105+
!e_it->is_memory_barrier()) continue;
106106

107107
dest[e_it->source.thread_nr].push_back(e_it);
108108
}
@@ -133,7 +133,7 @@ void memory_model_sct::thread_spawn(
133133
e_it!=equation.SSA_steps.end();
134134
e_it++)
135135
{
136-
if(is_spawn(e_it))
136+
if(e_it->is_spawn())
137137
{
138138
per_thread_mapt::const_iterator next_thread=
139139
per_thread_map.find(++next_thread_id);
@@ -238,7 +238,7 @@ void memory_model_sct::program_order(
238238
e_it!=events.end();
239239
e_it++)
240240
{
241-
if(is_memory_barrier(*e_it))
241+
if((*e_it)->is_memory_barrier())
242242
continue;
243243

244244
if(previous==equation.SSA_steps.end())

‎src/goto-symex/memory_model_tso.cpp

Lines changed: 11 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -72,16 +72,16 @@ bool memory_model_tsot::program_order_is_relaxed(
7272
partial_order_concurrencyt::event_it e1,
7373
partial_order_concurrencyt::event_it e2) const
7474
{
75-
assert(is_shared_read(e1) || is_shared_write(e1));
76-
assert(is_shared_read(e2) || is_shared_write(e2));
75+
assert(e1->is_shared_read() || e1->is_shared_write());
76+
assert(e2->is_shared_read() || e2->is_shared_write());
7777

7878
// no po relaxation within atomic sections
7979
if(e1->atomic_section_id!=0 &&
8080
e1->atomic_section_id==e2->atomic_section_id)
8181
return false;
8282

8383
// write to read program order is relaxed
84-
return is_shared_write(e1) && is_shared_read(e2);
84+
return e1->is_shared_write() && e2->is_shared_read();
8585
}
8686

8787
/*******************************************************************\
@@ -120,7 +120,7 @@ void memory_model_tsot::program_order(
120120
e_it!=events.end();
121121
e_it++)
122122
{
123-
if(is_memory_barrier(*e_it))
123+
if((*e_it)->is_memory_barrier())
124124
continue;
125125

126126
event_listt::const_iterator next=e_it;
@@ -135,30 +135,30 @@ void memory_model_tsot::program_order(
135135
e_it2!=events.end();
136136
e_it2++)
137137
{
138-
if((is_spawn(*e_it) && !is_memory_barrier(*e_it2)) ||
139-
is_spawn(*e_it2))
138+
if(((*e_it)->is_spawn() && !(*e_it2)->is_memory_barrier()) ||
139+
(*e_it2)->is_spawn())
140140
{
141141
add_constraint(
142142
equation,
143143
before(*e_it, *e_it2),
144144
"po",
145145
(*e_it)->source);
146146

147-
if(is_spawn(*e_it2))
147+
if((*e_it2)->is_spawn())
148148
break;
149149
else
150150
continue;
151151
}
152152

153-
if(is_memory_barrier(*e_it2))
153+
if((*e_it2)->is_memory_barrier())
154154
{
155155
const codet &code=to_code((*e_it2)->source.pc->code);
156156

157-
if(is_shared_read(*e_it) &&
157+
if((*e_it)->is_shared_read() &&
158158
!code.get_bool(ID_RRfence) &&
159159
!code.get_bool(ID_RWfence))
160160
continue;
161-
else if(is_shared_write(*e_it) &&
161+
else if((*e_it)->is_shared_write() &&
162162
!code.get_bool(ID_WRfence) &&
163163
!code.get_bool(ID_WWfence))
164164
continue;
@@ -184,7 +184,7 @@ void memory_model_tsot::program_order(
184184
}
185185
else if(program_order_is_relaxed(*e_it, *e_it2))
186186
{
187-
if(is_shared_read(*e_it2))
187+
if((*e_it2)->is_shared_read())
188188
cond=mb_guard_r;
189189
else
190190
cond=mb_guard_w;

0 commit comments

Comments
 (0)