cprover
Loading...
Searching...
No Matches
shared_buffers.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#include "shared_buffers.h"
10
11#include <util/c_types.h>
12#include <util/fresh_symbol.h>
13#include <util/message.h>
14#include <util/pointer_expr.h>
15#include <util/std_code.h>
16
18
20
21#include "fence.h"
22
24std::string shared_bufferst::unique(void)
25{
26 message.debug()<<"$fresh#"+std::to_string(uniq)<<messaget::eom;
27 return "$fresh#"+std::to_string(uniq++);
28}
29
32 const irep_idt &object)
33{
34 var_mapt::const_iterator it=var_map.find(object);
35 if(it!=var_map.end())
36 return it->second;
37
38 varst &vars=var_map[object];
39
41 const symbolt &symbol=ns.lookup(object);
42
43 vars.type=symbol.type;
44
45 vars.w_buff0 = add(symbol, "$w_buff0", symbol.type);
46 vars.w_buff1 = add(symbol, "$w_buff1", symbol.type);
47
48 vars.w_buff0_used = add(symbol, "$w_buff0_used", bool_typet());
49 vars.w_buff1_used = add(symbol, "$w_buff1_used", bool_typet());
50
51 vars.mem_tmp = add(symbol, "$mem_tmp", symbol.type);
52 vars.flush_delayed = add(symbol, "$flush_delayed", bool_typet());
53
54 vars.read_delayed = add(symbol, "$read_delayed", bool_typet());
55 vars.read_delayed_var =
56 add(symbol, "$read_delayed_var", pointer_type(symbol.type));
57
58 for(unsigned cnt=0; cnt<nb_threads; cnt++)
59 {
60 vars.r_buff0_thds.push_back(shared_bufferst::add(
61 symbol, "$r_buff0_thd" + std::to_string(cnt), bool_typet()));
62 vars.r_buff1_thds.push_back(shared_bufferst::add(
63 symbol, "$r_buff1_thd" + std::to_string(cnt), bool_typet()));
64 }
65
66 return vars;
67}
68
73 const symbolt &object,
74 const std::string &suffix,
75 const typet &type,
76 bool instrument)
77{
78 const namespacet ns(symbol_table);
79
80 symbolt &new_symbol = get_fresh_aux_symbol(
81 type,
82 id2string(object.name) + suffix,
83 id2string(object.base_name) + suffix,
84 object.location,
85 object.mode,
87 new_symbol.is_static_lifetime=true;
88 new_symbol.value.make_nil();
89
90 if(instrument)
91 instrumentations.insert(new_symbol.name);
92
93 return new_symbol.name;
94}
95
97{
98 goto_programt::targett t=goto_program.instructions.begin();
99 const namespacet ns(symbol_table);
100
101 for(const auto &vars : var_map)
102 {
103 source_locationt source_location;
104 source_location.make_nil();
105
106 assignment(goto_program, t, source_location, vars.second.w_buff0_used,
107 false_exprt());
108 assignment(goto_program, t, source_location, vars.second.w_buff1_used,
109 false_exprt());
110 assignment(goto_program, t, source_location, vars.second.flush_delayed,
111 false_exprt());
112 assignment(goto_program, t, source_location, vars.second.read_delayed,
113 false_exprt());
114 assignment(goto_program, t, source_location, vars.second.read_delayed_var,
115 null_pointer_exprt(pointer_type(vars.second.type)));
116
117 for(const auto &id : vars.second.r_buff0_thds)
118 assignment(goto_program, t, source_location, id, false_exprt());
119
120 for(const auto &id : vars.second.r_buff1_thds)
121 assignment(goto_program, t, source_location, id, false_exprt());
122 }
123}
124
126 goto_functionst &goto_functions)
127{
128 // get "main"
129 goto_functionst::function_mapt::iterator
130 m_it=goto_functions.function_map.find(goto_functions.entry_point());
131
132 if(m_it==goto_functions.function_map.end())
133 throw "weak memory instrumentation needs an entry point";
134
135 goto_programt &main=m_it->second.body;
137}
138
141 goto_programt &goto_program,
143 const source_locationt &source_location,
144 const irep_idt &id_lhs,
145 const exprt &value)
146{
147 const namespacet ns(symbol_table);
148 std::string identifier=id2string(id_lhs);
149
150 const size_t pos=identifier.find("[]");
151
152 if(pos!=std::string::npos)
153 {
154 /* we don't distinguish the members of an array for the moment */
155 identifier.erase(pos);
156 }
157
158 try
159 {
160 const exprt symbol=ns.lookup(identifier).symbol_expr();
161
162 t = goto_program.insert_before(
163 t, goto_programt::make_assignment(symbol, value, source_location));
164
165 // instrumentations.insert((const irep_idt) (t->code.id()));
166
167 t++;
168 }
169 catch(const std::string &s)
170 {
171 message.warning() << s << messaget::eom;
172 }
173}
174
177 goto_programt &goto_program,
179 const source_locationt &source_location,
180 const irep_idt &read_object,
181 const irep_idt &write_object)
182{
183/* option 1: */
184/* trick using an additional variable whose value is to be defined later */
185
186#if 0
187 assignment(goto_program, target, source_location, vars.read_delayed,
188 true_exprt());
189 assignment(goto_program, target, source_location, vars.read_delayed_var,
191
193
194 assignment(goto_program, target, source_location, vars.read_new_var, new_var);
195
196 // initial write, but from the new variable now
197 assignment(goto_program, target, source_location, write_object, new_var);
198#endif
199
200/* option 2 */
201/* pointer */
202
203 const std::string identifier=id2string(write_object);
204
205 message.debug()<<"delay_read: " << messaget::eom;
206 const varst &vars=(*this)(write_object);
207
209
211 goto_program,
212 target,
213 source_location,
214 vars.read_delayed,
215 true_exprt());
217 goto_program,
218 target,
219 source_location,
220 vars.read_delayed_var,
222}
223
226 goto_programt &goto_program,
228 const source_locationt &source_location,
229 const irep_idt &write_object)
230{
231#if 0
232 // option 1
233 const varst &vars=(*this)(write_object);
234
235 const symbol_exprt fresh_var_expr=symbol_exprt(vars.read_new_var, vars.type);
236 const symbol_exprt var_expr=symbol_exprt(vars.read_delayed_var, vars.type);
238
240 bool_typet());
242
243 target=goto_program.insert_before(target);
244 target->type=ASSUME;
245 target->guard=if_expr;
246 target->guard.source_location()=source_location;
247 target->source_location=source_location;
248
249 target++;
250
251 assignment(goto_program, target, source_location, vars.read_delayed,
252 false_exprt());
253#else
254 // option 2: do nothing
255 // unused parameters
256 (void)goto_program;
257 (void)target;
258 (void)target;
259 (void)source_location;
261#endif
262}
263
266 goto_programt &goto_program,
268 const source_locationt &source_location,
269 const irep_idt &object,
271 const unsigned current_thread)
272{
273 const std::string identifier=id2string(object);
274
275 message.debug() << "write: " << object << messaget::eom;
276 const varst &vars=(*this)(object);
277
278 // We rotate the write buffers for anything that is written.
279 assignment(goto_program, target, source_location, vars.w_buff1, vars.w_buff0);
281 goto_program,
282 target,
283 source_location,
284 vars.w_buff0,
285 original_instruction.code().op1());
286
287 // We update the used flags
289 goto_program,
290 target,
291 source_location,
292 vars.w_buff1_used,
293 vars.w_buff0_used);
295 goto_program,
296 target,
297 source_location,
298 vars.w_buff0_used,
299 true_exprt());
300
301 // We should not exceed the buffer size -- inserts assertion for dynamically
302 // checking this
303 const exprt buff0_used_expr=symbol_exprt(vars.w_buff0_used, bool_typet());
304 const exprt buff1_used_expr=symbol_exprt(vars.w_buff1_used, bool_typet());
305 const exprt cond_expr=
307
308 target = goto_program.insert_before(
309 target, goto_programt::make_assertion(cond_expr, source_location));
310 target++;
311
312 // We update writers ownership of the values in the buffer
313 for(unsigned cnt=0; cnt<nb_threads; cnt++)
314 assignment(goto_program, target, source_location, vars.r_buff1_thds[cnt],
315 vars.r_buff0_thds[cnt]);
316
317 // We update the lucky new author of this value in the buffer
319 goto_program,
320 target,
321 source_location,
322 vars.r_buff0_thds[current_thread],
323 true_exprt());
324}
325
328 goto_programt &goto_program,
330 const source_locationt &source_location,
331 const irep_idt &object,
332 const unsigned current_thread)
333{
334 const std::string identifier=id2string(object);
335
336 // mostly for instrumenting the fences. A thread only flushes the values it
337 // wrote in the buffer.
338 message.debug() << "det flush: " << messaget::eom;
339 const varst &vars=(*this)(object);
340
341 // current value in the memory
342 const exprt lhs=symbol_exprt(object, vars.type);
343
344 // if buff0 from this thread, uses it to update the memory (the most recent
345 // value, or last write by -ws-> ); if not, if buff1 from this thread, uses
346 // it; if not, keeps the current memory value
347 const exprt buff0_expr=symbol_exprt(vars.w_buff0, vars.type);
348 const exprt buff1_expr=symbol_exprt(vars.w_buff1, vars.type);
349
350 const exprt buff0_used_expr=symbol_exprt(vars.w_buff0_used, bool_typet());
351 const exprt buff1_used_expr=symbol_exprt(vars.w_buff1_used, bool_typet());
352
353 const exprt buff0_mine_expr=symbol_exprt(vars.r_buff0_thds[current_thread],
354 bool_typet());
355 const exprt buff1_mine_expr=symbol_exprt(vars.r_buff1_thds[current_thread],
356 bool_typet());
357
362
363 const exprt new_value_expr=
364 if_exprt(
367 if_exprt(
370 lhs));
371
372 // We update (or not) the value in the memory
373 assignment(goto_program, target, source_location, object, new_value_expr);
374
375 // We update the flags of the buffer
376 // if buff0 used and mine, then it is no more used, as we flushed the last
377 // write and -ws-> imposes not to have other writes in the buffer
379 goto_program,
380 target,
381 source_location,
382 vars.w_buff0_used,
383 if_exprt(
385 false_exprt(),
387
388 // buff1 used and mine & not buff0 used and mine, then it no more used
389 // if buff0 is used and mine, then, by ws, buff1 is no more used
390 // otherwise, remains as it is
393
395 goto_program,
396 target,
397 source_location,
398 vars.w_buff1_used,
399 if_exprt(
401 false_exprt(),
403
404 // We update the ownerships
405 // if buff0 mine and used, flushed, so belongs to nobody
406 const exprt buff0_thd_expr=
407 symbol_exprt(vars.r_buff0_thds[current_thread], bool_typet());
408
410 goto_program,
411 target,
412 source_location,
413 vars.r_buff0_thds[current_thread],
415
416 // if buff1 used and mine, or if buff0 used and mine, then buff1 flushed and
417 // doesn't belong to anybody
418 const exprt buff1_thd_expr=
419 symbol_exprt(vars.r_buff1_thds[current_thread], bool_typet());
420
422 goto_program,
423 target,
424 source_location,
425 vars.r_buff1_thds[current_thread],
426 if_exprt(
428 false_exprt(),
430}
431
434 const irep_idt &function_id,
435 goto_programt &goto_program,
437 const source_locationt &source_location,
438 const irep_idt &object,
439 const unsigned current_thread,
440 const bool tso_pso_rmo) // true: tso/pso/rmo; false: power
441{
442 const std::string identifier=id2string(object);
443
444 message.debug() << "nondet flush: " << object << messaget::eom;
445
446 try
447 {
448 const varst &vars=(*this)(object);
449
450 // Non deterministic choice
451 irep_idt choice0 = choice(function_id, "0");
452 irep_idt choice2 = choice(function_id, "2"); // delays the write flush
453
456 const exprt nondet_bool_expr =
457 side_effect_expr_nondett(bool_typet(), source_location);
458
459 // throw Boolean dice
460 assignment(goto_program, target, source_location, choice0, nondet_bool_expr);
461 assignment(goto_program, target, source_location, choice2, nondet_bool_expr);
462
463 // Buffers and memory
464 const symbol_exprt buff0_expr=symbol_exprt(vars.w_buff0, vars.type);
465 const symbol_exprt buff1_expr=symbol_exprt(vars.w_buff1, vars.type);
466 const exprt lhs=symbol_exprt(object, vars.type);
467
468 // Buffer uses
470 bool_typet());
472 bool_typet());
473
474 // Buffer ownerships
476 symbol_exprt(vars.r_buff0_thds[current_thread], bool_typet());
478 symbol_exprt(vars.r_buff1_thds[current_thread], bool_typet());
479
480
481 // Will the write be directly flushed, or is it just a read?
483 goto_program, target, source_location, vars.flush_delayed, delay_expr);
484 assignment(goto_program, target, source_location, vars.mem_tmp, lhs);
485
486 // for POWER, only instrumented reads can read from the buffers of other
487 // threads
488 bool instrumented=false;
489
490 if(!tso_pso_rmo)
491 {
492 if(cycles.find(object)!=cycles.end())
493 {
494 typedef std::multimap<irep_idt, source_locationt>::iterator m_itt;
495 std::pair<m_itt, m_itt> ran=cycles_loc.equal_range(object);
496 for(m_itt ran_it=ran.first; ran_it!=ran.second; ran_it++)
497 if(ran_it->second==source_location)
498 {
499 instrumented=true;
500 break;
501 }
502 }
503 }
504
505 // TSO/PSO/RMO
507 {
508 // 7 cases
509
510 // (1) (3) (4)
511 // if buff0 unused
512 // or buff0 not mine and buff1 unused
513 // or buff0 not mine and buff1 not mine
514 // -> read from memory (and does not modify the buffer in any aspect)
515 const exprt cond_134_expr=
516 or_exprt(
518 or_exprt(
519 and_exprt(
522 and_exprt(
525 const exprt val_134_expr=lhs;
532
533 // (2) (6) (7)
534 // if buff0 used and mine
535 // -> read from buff0
544
545 // (5)
546 // buff0 and buff1 are used, buff0 is not mine, buff1 is mine
547 // -> read from buff1
548 const exprt cond_5_expr=
549 and_exprt(
551 and_exprt(
561
562 // Updates
563 // memory
565 goto_program,
566 target,
567 source_location,
568 object,
569 if_exprt(
572 if_exprt(
575 val_5_expr)));
576 // buff0
578 goto_program,
579 target,
580 source_location,
581 vars.w_buff0,
582 if_exprt(
585 if_exprt(
588 if_exprt(
591 buff0_5_expr))));
592 // buff1
594 goto_program,
595 target,
596 source_location,
597 vars.w_buff1,
598 if_exprt(
601 if_exprt(
604 if_exprt(
607 buff1_5_expr))));
608 // buff0_used
610 goto_program,
611 target,
612 source_location,
613 vars.w_buff0_used,
614 if_exprt(
617 if_exprt(
620 if_exprt(
624 // buff1_used
626 goto_program,
627 target,
628 source_location,
629 vars.w_buff1_used,
630 if_exprt(
633 if_exprt(
636 if_exprt(
640 // buff0_thd
642 goto_program,
643 target,
644 source_location,
645 vars.r_buff0_thds[current_thread],
646 if_exprt(
649 if_exprt(
652 if_exprt(
656 // buff1_thd
658 goto_program,
659 target,
660 source_location,
661 vars.r_buff1_thds[current_thread], if_exprt(
664 if_exprt(
667 if_exprt(
671 }
672 // POWER
673 else
674 {
675 // a thread can read the other threads' buffers
676
677 // One extra non-deterministic choice needed
678 irep_idt choice1 = choice(function_id, "1");
680
681 // throw Boolean dice
683 goto_program, target, source_location, choice1, nondet_bool_expr);
684
685 // 7 cases
686
687 // (1)
688 // if buff0 unused
689 // -> read from memory (and does not modify the buffer in any aspect)
691 const exprt val_1_expr=lhs;
698
699 // (2) (6) (7)
700 // if buff0 used and mine
701 // -> read from buff0
702 const exprt cond_267_expr=
711
712 // (3)
713 // if buff0 used and not mine, and buff1 not used
714 // -> read from buff0 or memory
715 const exprt cond_3_expr=
716 and_exprt(
718 and_exprt(
728
729 // (4)
730 // buff0 and buff1 are both used, and both not mine
731 // -> read from memory or buff0 or buff1
732 const exprt cond_4_expr=
733 and_exprt(
736 const exprt val_4_expr=
737 if_exprt(
739 lhs,
740 if_exprt(
743 buff1_expr));
752
753 // (5)
754 // buff0 and buff1 are both used, and buff0 not mine, and buff1 mine
755 // -> read buff1 or buff0
756 const exprt cond_5_expr=
757 and_exprt(
760 const exprt val_5_expr=
761 if_exprt(
764 buff0_expr);
771
772 // Updates
773 // memory
775 goto_program,
776 target,
777 source_location,
778 object,
779 if_exprt(
782 if_exprt(
785 if_exprt(
788 if_exprt(
791 val_3_expr)))));
792 // buff0
794 goto_program,
795 target,
796 source_location,
797 vars.w_buff0,
798 if_exprt(
801 if_exprt(
804 if_exprt(
807 if_exprt(
810 if_exprt(
813 buff0_3_expr))))));
814 // buff1
816 goto_program,
817 target,
818 source_location,
819 vars.w_buff1,
820 if_exprt(
823 if_exprt(
826 if_exprt(
829 if_exprt(
832 if_exprt(
835 buff1_3_expr))))));
836 // buff0_used
838 goto_program,
839 target,
840 source_location,
841 vars.w_buff0_used,
842 if_exprt(
845 if_exprt(
848 if_exprt(
851 if_exprt(
854 if_exprt(
857 buff0_used_3_expr))))));
858 // buff1_used
860 goto_program,
861 target,
862 source_location,
863 vars.w_buff1_used,
864 if_exprt(
867 if_exprt(
870 if_exprt(
873 if_exprt(
876 if_exprt(
879 buff1_used_3_expr))))));
880 // buff0_thd
882 goto_program,
883 target,
884 source_location,
885 vars.r_buff0_thds[current_thread],
886 if_exprt(
889 if_exprt(
892 if_exprt(
895 if_exprt(
898 if_exprt(
901 buff0_thd_3_expr))))));
902 // buff1_thd
904 goto_program,
905 target,
906 source_location,
907 vars.r_buff1_thds[current_thread],
908 if_exprt(
911 if_exprt(
914 if_exprt(
917 if_exprt(
920 if_exprt(
923 buff1_thd_3_expr))))));
924 }
925 }
926 catch(const std::string &s)
927 {
928 message.warning() << s << messaget::eom;
929 }
930}
931
933 const namespacet &ns,
934 const symbol_exprt &symbol_expr,
935 bool is_write
936 // are we asking for the variable (false), or for the variable and
937 // the source_location in the code (true)
938)
939{
940 const irep_idt &identifier=symbol_expr.get_identifier();
941
942 if(identifier==CPROVER_PREFIX "alloc" ||
943 identifier==CPROVER_PREFIX "alloc_size" ||
944 identifier=="stdin" ||
945 identifier=="stdout" ||
946 identifier=="stderr" ||
947 identifier=="sys_nerr" ||
948 has_prefix(id2string(identifier), "__unbuffered_") ||
949 has_prefix(id2string(identifier), "__CPROVER"))
950 return false; // not buffered
951
952 const symbolt &symbol=ns.lookup(identifier);
953
954 if(!symbol.is_static_lifetime)
955 return false; // these are local
956
957 if(symbol.is_thread_local)
958 return false; // these are local
959
960 if(instrumentations.find(identifier)!=instrumentations.end())
961 return false; // these are instrumentations
962
963 return is_buffered_in_general(symbol_expr, is_write);
964}
965
967 const symbol_exprt &symbol_expr,
968 bool is_write
969 // are we asking for the variable (false), or for the variable and the
970 // source_location in the code? (true)
971)
972{
973 if(cav11)
974 return true;
975
976 const irep_idt &identifier=symbol_expr.get_identifier();
977 const source_locationt &source_location=symbol_expr.source_location();
978
979 if(cycles.find(identifier)==cycles.end())
980 return false; // not to instrument
981
982 if(!is_write)
983 {
984 // to be uncommented only when we are sure all the cycles
985 // are detected (before detection of the pairs -- no hack)
986 // WARNING: on the FULL cycle, not reduced by PO
987 /*typedef std::multimap<irep_idt,source_locationt>::iterator m_itt;
988 std::pair<m_itt,m_itt> ran=cycles_r_loc.equal_range(identifier);
989 for(m_itt ran_it=ran.first; ran_it!=ran.second; ran_it++)
990 if(ran_it->second==source_location)*/
991 return true;
992 }
993 else
994 {
995 typedef std::multimap<irep_idt, source_locationt>::iterator m_itt;
996 std::pair<m_itt, m_itt> ran=cycles_loc.equal_range(identifier);
997 for(m_itt ran_it=ran.first; ran_it!=ran.second; ran_it++)
998 if(ran_it->second==source_location)
999 return true; // not to instrument
1000 }
1001
1002 return false;
1003}
1004
1009 value_setst &value_sets,
1010 goto_functionst &goto_functions)
1011{
1013
1014 for(auto &gf_entry : goto_functions.function_map)
1015 {
1016#ifdef LOCAL_MAY
1018#endif
1019
1021 {
1023 ns,
1024 value_sets,
1025 gf_entry.first,
1026 i_it
1028 ,
1029 local_may
1030#endif
1031 ); // NOLINT(whitespace/parens)
1032 for(const auto &w_entry : rw_set.w_entries)
1033 {
1034 for(const auto &r_entry : rw_set.r_entries)
1035 {
1036 message.debug() << "debug: " << id2string(w_entry.second.object)
1037 << " reads from " << id2string(r_entry.second.object)
1038 << messaget::eom;
1039 if(is_buffered_in_general(r_entry.second.symbol_expr, true))
1040 {
1041 // shouldn't it be true? false => overapprox
1042 affected_by_delay_set.insert(w_entry.second.object);
1043 }
1044 }
1045 }
1046 }
1047 }
1048}
1049
1052 value_setst &value_sets,
1053 const irep_idt &function_id,
1054 memory_modelt model)
1055{
1057 << "visit function " << function_id << messaget::eom;
1058 if(function_id == INITIALIZE_FUNCTION)
1059 return;
1060
1062 goto_programt &goto_program = goto_functions.function_map[function_id].body;
1063
1064#ifdef LOCAL_MAY
1066#endif
1067
1069 {
1070 goto_programt::instructiont &instruction=*i_it;
1071
1073 << "instruction " << instruction.type() << messaget::eom;
1074
1075 /* thread marking */
1076 if(instruction.is_start_thread())
1077 {
1081 }
1082 else if(instruction.is_end_thread())
1084
1085 if(instruction.is_assign())
1086 {
1087 try
1088 {
1090 ns,
1091 value_sets,
1092 function_id,
1093 i_it
1095 ,
1096 local_may
1097#endif
1098 ); // NOLINT(whitespace/parens)
1099
1100 if(rw_set.empty())
1101 continue;
1102
1103 // add all the written values (which are not instrumentations)
1104 // in a set
1105 for(const auto &w_entry : rw_set.w_entries)
1106 {
1107 if(shared_buffers.is_buffered(ns, w_entry.second.symbol_expr, false))
1108 past_writes.insert(w_entry.second.object);
1109 }
1110
1112 original_instruction.swap(instruction);
1113 const source_locationt &source_location =
1114 original_instruction.source_location();
1115
1116 // ATOMIC_BEGIN: we make the whole thing atomic
1117 instruction = goto_programt::make_atomic_begin(source_location);
1118 i_it++;
1119
1120 // we first perform (non-deterministically) up to 2 writes for
1121 // stuff that is potentially read
1122 for(const auto &r_entry : rw_set.r_entries)
1123 {
1124 // flush read -- do nothing in this implementation
1126 goto_program, i_it, source_location, r_entry.second.object);
1127
1128 if(shared_buffers.is_buffered(ns, r_entry.second.symbol_expr, false))
1130 function_id,
1131 goto_program,
1132 i_it,
1133 source_location,
1134 r_entry.second.object,
1136 (model == TSO || model == PSO || model == RMO));
1137 }
1138
1139 // Now perform the write(s).
1140 for(const auto &w_entry : rw_set.w_entries)
1141 {
1142 // if one of the previous read was to buffer, then delays the read
1143 if(model==RMO || model==Power)
1144 {
1145 for(const auto &r_entry : rw_set.r_entries)
1146 {
1148 ns, r_entry.second.symbol_expr, true))
1149 {
1151 goto_program,
1152 i_it,
1153 source_location,
1154 r_entry.second.object,
1155 w_entry.second.object);
1156 }
1157 }
1158 }
1159
1160 if(shared_buffers.is_buffered(ns, w_entry.second.symbol_expr, true))
1161 {
1163 goto_program,
1164 i_it,
1165 source_location,
1166 w_entry.second.object,
1169 }
1170 else
1171 {
1172 // unbuffered
1173 if(model==RMO || model==Power)
1174 {
1175 for(const auto &r_entry : rw_set.r_entries)
1176 {
1177 if(
1179 r_entry.second.object) !=
1181 {
1183 << "second: " << r_entry.second.object << messaget::eom;
1184 const varst &vars = (shared_buffers)(r_entry.second.object);
1185
1187 << "writer " << w_entry.second.object << " reads "
1188 << r_entry.second.object << messaget::eom;
1189
1190 // TO FIX: how to deal with rhs including calls?
1191 // if a read is delayed, use its alias instead of itself
1192 // -- or not
1194 symbol_exprt(r_entry.second.object, vars.type);
1196 vars.read_delayed_var,
1197 pointer_type(vars.type));
1199 vars.read_delayed, bool_typet());
1200
1201 // One extra non-deterministic choice needed
1202 irep_idt choice1 = shared_buffers.choice(function_id, "1");
1204 bool_typet());
1205 const exprt nondet_bool_expr =
1206 side_effect_expr_nondett(bool_typet(), source_location);
1207
1208 // throw Boolean dice
1210 goto_program,
1211 i_it,
1212 source_location,
1213 choice1,
1215
1216 const if_exprt rhs(
1218 if_exprt(
1222 to_replace_expr); // original_instruction.code().op1());
1223
1225 goto_program,
1226 i_it,
1227 source_location,
1228 r_entry.second.object,
1229 rhs);
1230 }
1231 }
1232 }
1233
1234 // normal assignment
1236 goto_program,
1237 i_it,
1238 source_location,
1239 w_entry.second.object,
1240 original_instruction.code().op1());
1241 }
1242 }
1243
1244 // if last writes was flushed to make the lhs reads the buffer but
1245 // without affecting the memory, restore the previous memory value
1246 // (buffer flush delay)
1247 for(const auto &r_entry : rw_set.r_entries)
1248 {
1249 if(shared_buffers.is_buffered(ns, r_entry.second.symbol_expr, false))
1250 {
1252 << "flush restore: " << r_entry.second.object << messaget::eom;
1253 const varst vars = (shared_buffers)(r_entry.second.object);
1254 const exprt delayed_expr=symbol_exprt(vars.flush_delayed,
1255 bool_typet());
1257 vars.type);
1258 const exprt cond_expr = if_exprt(
1259 delayed_expr, mem_value_expr, r_entry.second.symbol_expr);
1260
1262 goto_program,
1263 i_it,
1264 source_location,
1265 r_entry.second.object,
1266 cond_expr);
1268 goto_program, i_it, source_location,
1269 vars.flush_delayed, false_exprt());
1270 }
1271 }
1272
1273 // ATOMIC_END
1274 i_it = goto_program.insert_before(
1275 i_it, goto_programt::make_atomic_end(source_location));
1276 i_it++;
1277
1278 i_it--; // the for loop already counts us up
1279 }
1280 catch (...)
1281 {
1282 shared_buffers.message.warning() << "Identifier not found"
1283 << messaget::eom;
1284 }
1285 }
1286 else if(
1287 is_fence(instruction, ns) ||
1288 (instruction.is_other() &&
1289 instruction.code().get_statement() == ID_fence &&
1290 (instruction.code().get_bool("WRfence") ||
1291 instruction.code().get_bool("WWfence") ||
1292 instruction.code().get_bool("RWfence") ||
1293 instruction.code().get_bool("RRfence"))))
1294 {
1296 original_instruction.swap(instruction);
1297 const source_locationt &source_location =
1298 original_instruction.source_location();
1299
1300 // ATOMIC_BEGIN
1301 instruction = goto_programt::make_atomic_begin(source_location);
1302 i_it++;
1303
1304 // does it for all the previous statements
1305 for(std::set<irep_idt>::iterator s_it=past_writes.begin();
1306 s_it!=past_writes.end(); s_it++)
1307 {
1309 goto_program, i_it, source_location, *s_it,
1311 }
1312
1313 // ATOMIC_END
1314 i_it = goto_program.insert_before(
1315 i_it, goto_programt::make_atomic_end(source_location));
1316 i_it++;
1317
1318 i_it--; // the for loop already counts us up
1319 }
1320 else if(is_lwfence(instruction, ns))
1321 {
1322 // po -- remove the lwfence
1323 *i_it = goto_programt::make_skip(i_it->source_location());
1324 }
1325 else if(instruction.is_function_call())
1326 {
1327 const exprt &fun = instruction.call_function();
1328 weak_memory(value_sets, to_symbol_expr(fun).get_identifier(), model);
1329 }
1330 }
1331}
pointer_typet pointer_type(const typet &subtype)
Definition c_types.cpp:240
Operator to return the address of an object.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
Boolean AND.
Definition std_expr.h:2071
The Boolean type.
Definition std_types.h:36
Operator to dereference a pointer.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
Equality.
Definition std_expr.h:1306
Base class for all expressions.
Definition expr.h:56
const source_locationt & source_location() const
Definition expr.h:223
The Boolean constant false.
Definition std_expr.h:3017
A collection of goto functions.
function_mapt function_map
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
This class represents an instruction in the GOTO intermediate representation.
const goto_instruction_codet & code() const
Get the code represented by this instruction.
const exprt & call_function() const
Get the function that is called for FUNCTION_CALL.
goto_program_instruction_typet type() const
What kind of instruction?
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
instructionst::iterator targett
static instructiont make_atomic_end(const source_locationt &l=source_locationt::nil())
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
static instructiont make_atomic_begin(const source_locationt &l=source_locationt::nil())
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
targett insert_before(const_targett target)
Insertion before the instruction pointed-to by the given instruction iterator target.
The trinary if-then-else operator.
Definition std_expr.h:2323
void make_nil()
Definition irep.h:454
mstreamt & debug() const
Definition message.h:429
mstreamt & warning() const
Definition message.h:404
static eomt eom
Definition message.h:297
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Boolean negation.
Definition std_expr.h:2278
The null pointer constant.
Boolean OR.
Definition std_expr.h:2179
symbol_table_baset & symbol_table
void weak_memory(value_setst &value_sets, const irep_idt &function_id, memory_modelt model)
instruments the program for the pairs detected through the CFG
std::set< irep_idt > past_writes
std::multimap< irep_idt, source_locationt > cycles_loc
const varst & operator()(const irep_idt &object)
instruments the variable
void nondet_flush(const irep_idt &function_id, goto_programt &goto_program, goto_programt::targett &t, const source_locationt &source_location, const irep_idt &object, const unsigned current_thread, const bool tso_pso_rmo)
instruments read
std::string unique()
returns a unique id (for fresh variables)
void write(goto_programt &goto_program, goto_programt::targett &t, const source_locationt &source_location, const irep_idt &object, goto_programt::instructiont &original_instruction, const unsigned current_thread)
instruments write
void affected_by_delay(value_setst &value_sets, goto_functionst &goto_functions)
analysis over the goto-program which computes in affected_by_delay_set the variables (non necessarily...
void det_flush(goto_programt &goto_program, goto_programt::targett &t, const source_locationt &source_location, const irep_idt &object, const unsigned current_thread)
flush buffers (instruments fence)
irep_idt add_fresh_var(const symbolt &object, const std::string &suffix, const typet &type)
void add_initialization(goto_programt &goto_program)
bool is_buffered_in_general(const symbol_exprt &, bool is_write)
void assignment(goto_programt &goto_program, goto_programt::targett &t, const source_locationt &source_location, const irep_idt &id_lhs, const exprt &rhs)
add an assignment in the goto-program
irep_idt add(const symbolt &object, const std::string &suffix, const typet &type, bool added_as_instrumentation)
add a new var for instrumenting the input var
std::set< irep_idt > affected_by_delay_set
class symbol_table_baset & symbol_table
std::set< irep_idt > cycles
void delay_read(goto_programt &goto_program, goto_programt::targett &t, const source_locationt &source_location, const irep_idt &read_object, const irep_idt &write_object)
delays a read (POWER)
void flush_read(goto_programt &goto_program, goto_programt::targett &t, const source_locationt &source_location, const irep_idt &write_object)
flushes read (POWER)
irep_idt choice(const irep_idt &function_id, const std::string &suffix)
void add_initialization_code(goto_functionst &goto_functions)
bool is_buffered(const namespacet &, const symbol_exprt &, bool is_write)
std::set< irep_idt > instrumentations
A side_effect_exprt that returns a non-deterministically chosen value.
Definition std_code.h:1520
Expression to hold a symbol (variable)
Definition std_expr.h:113
const irep_idt & get_identifier() const
Definition std_expr.h:142
Symbol table entry.
Definition symbol.h:28
bool is_static_lifetime
Definition symbol.h:70
bool is_thread_local
Definition symbol.h:71
typet type
Type of symbol.
Definition symbol.h:31
irep_idt name
The unique identifier.
Definition symbol.h:40
exprt value
Initial value of symbol.
Definition symbol.h:34
The Boolean constant true.
Definition std_expr.h:3008
The type of an expression, extends irept.
Definition type.h:29
bool has_prefix(const std::string &s, const std::string &prefix)
Definition converter.cpp:13
#define CPROVER_PREFIX
int main()
Definition example.cpp:18
bool is_fence(const goto_programt::instructiont &instruction, const namespacet &ns)
Definition fence.cpp:19
bool is_lwfence(const goto_programt::instructiont &instruction, const namespacet &ns)
Definition fence.cpp:35
Fences for instrumentation.
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, const namespacet &ns, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with respect to the given namespace ns with the requested name pattern ...
Fresh auxiliary symbol creation.
#define Forall_goto_program_instructions(it, program)
@ ASSUME
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
literalt pos(literalt a)
Definition literal.h:194
API to expression classes for Pointers.
Race Detection for Threaded Goto Programs.
#define INITIALIZE_FUNCTION
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:222
memory_modelt
Definition wmm.h:18
@ TSO
Definition wmm.h:20
@ RMO
Definition wmm.h:22
@ PSO
Definition wmm.h:21
@ Power
Definition wmm.h:23