Skip to content

Commit 4603c31

Browse files
committed
Fix goto-program conversion of fence instructions
Using it->code.set(ID_statement, ...) no longer suffices as it will not set code.id(), which is ID_nil after initialisation. Thus any such instruction is removed during goto-program cleanup. Use the recently added APIs instead, which will ensure proper initialisation.
1 parent 8f27a56 commit 4603c31

File tree

2 files changed

+17
-22
lines changed

2 files changed

+17
-22
lines changed

regression/cbmc-concurrency/memory_barrier2/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
KNOWNBUG
1+
CORE
22
main.c
33
--mm tso
44
^EXIT=0$

src/goto-programs/builtin_functions.cpp

Lines changed: 16 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -1065,15 +1065,14 @@ void goto_convertt::do_function_call_symbol(
10651065
throw 0;
10661066
}
10671067

1068-
goto_programt::targett t=dest.add_instruction(OTHER);
1069-
t->source_location=function.source_location();
1070-
t->code.set(ID_statement, ID_fence);
1071-
1068+
codet fence(ID_fence);
10721069
forall_expr(it, arguments)
10731070
{
10741071
const irep_idt kind=get_string_constant(*it);
1075-
t->code.set(kind, true);
1072+
fence.set(kind, true);
10761073
}
1074+
1075+
dest.add(goto_programt::make_other(fence, function.source_location()));
10771076
}
10781077
else if(identifier=="__builtin_prefetch")
10791078
{
@@ -1268,10 +1267,9 @@ void goto_convertt::do_function_call_symbol(
12681267
t3->code=code_assignt(deref_ptr, op_expr);
12691268

12701269
// this instruction implies an mfence, i.e., WRfence
1271-
goto_programt::targett t4=dest.add_instruction(OTHER);
1272-
t4->source_location=function.source_location();
1273-
t4->code=codet(ID_fence);
1274-
t4->code.set(ID_WRfence, true);
1270+
codet fence(ID_fence);
1271+
fence.set(ID_WRfence, true);
1272+
dest.add(goto_programt::make_other(fence, function.source_location()));
12751273

12761274
goto_programt::targett t5=dest.add_instruction(ATOMIC_END);
12771275
t5->source_location=function.source_location();
@@ -1339,10 +1337,9 @@ void goto_convertt::do_function_call_symbol(
13391337
}
13401338

13411339
// this instruction implies an mfence, i.e., WRfence
1342-
goto_programt::targett t4=dest.add_instruction(OTHER);
1343-
t4->source_location=function.source_location();
1344-
t4->code=codet(ID_fence);
1345-
t4->code.set(ID_WRfence, true);
1340+
codet fence(ID_fence);
1341+
fence.set(ID_WRfence, true);
1342+
dest.add(goto_programt::make_other(fence, function.source_location()));
13461343

13471344
goto_programt::targett t5=dest.add_instruction(ATOMIC_END);
13481345
t5->source_location=function.source_location();
@@ -1410,10 +1407,9 @@ void goto_convertt::do_function_call_symbol(
14101407
t3->code=code_assignt(deref_ptr, if_expr);
14111408

14121409
// this instruction implies an mfence, i.e., WRfence
1413-
goto_programt::targett t4=dest.add_instruction(OTHER);
1414-
t4->source_location=function.source_location();
1415-
t4->code=codet(ID_fence);
1416-
t4->code.set(ID_WRfence, true);
1410+
codet fence(ID_fence);
1411+
fence.set(ID_WRfence, true);
1412+
dest.add(goto_programt::make_other(fence, function.source_location()));
14171413

14181414
goto_programt::targett t5=dest.add_instruction(ATOMIC_END);
14191415
t5->source_location=function.source_location();
@@ -1471,10 +1467,9 @@ void goto_convertt::do_function_call_symbol(
14711467
t3->code=code_assignt(deref_ptr, if_expr);
14721468

14731469
// this instruction implies an mfence, i.e., WRfence
1474-
goto_programt::targett t4=dest.add_instruction(OTHER);
1475-
t4->source_location=function.source_location();
1476-
t4->code=codet(ID_fence);
1477-
t4->code.set(ID_WRfence, true);
1470+
codet fence(ID_fence);
1471+
fence.set(ID_WRfence, true);
1472+
dest.add(goto_programt::make_other(fence, function.source_location()));
14781473

14791474
goto_programt::targett t5=dest.add_instruction(ATOMIC_END);
14801475
t5->source_location=function.source_location();

0 commit comments

Comments
 (0)