Skip to content

Commit 9a5345e

Browse files
author
Daniel Kroening
committed
protect opX in codet subclasses
This will prevent accesses that are not type safe.
1 parent 41d097d commit 9a5345e

File tree

9 files changed

+150
-16
lines changed

9 files changed

+150
-16
lines changed

‎src/cpp/cpp_typecheck_initializer.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -326,7 +326,7 @@ void cpp_typecheckt::zero_initializer(
326326
code_assignt assign(object, *value);
327327
assign.add_source_location()=source_location;
328328

329-
typecheck_expr(assign.op0());
329+
typecheck_expr(assign.lhs());
330330
assign.lhs().type().set(ID_C_constant, false);
331331
already_typechecked(assign.lhs());
332332

‎src/goto-instrument/accelerate/accelerate.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -379,7 +379,7 @@ void acceleratet::add_dirty_checks()
379379
// variables is clean _before_ clearing any dirty flags.
380380
if(it->is_assign())
381381
{
382-
exprt &lhs=it->code.op0();
382+
exprt &lhs = it->get_assign().lhs();
383383
expr_mapt::iterator dirty_var=dirty_vars_map.find(lhs);
384384

385385
if(dirty_var!=dirty_vars_map.end())
@@ -398,7 +398,7 @@ void acceleratet::add_dirty_checks()
398398

399399
if(it->is_assign())
400400
{
401-
find_symbols(it->code.op1(), read);
401+
find_symbols(it->get_assign().rhs(), read);
402402
}
403403

404404
for(find_symbols_sett::iterator jt=read.begin();

‎src/goto-instrument/accelerate/acceleration_utils.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -927,8 +927,8 @@ bool acceleration_utilst::do_nonrecursive(
927927
{
928928
if(it->is_assign())
929929
{
930-
exprt lhs=it->code.op0();
931-
exprt rhs=it->code.op1();
930+
exprt lhs = it->get_assign().lhs();
931+
exprt rhs = it->get_assign().rhs();
932932

933933
if(lhs.id()==ID_dereference)
934934
{

‎src/goto-instrument/rw_set.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -48,8 +48,8 @@ void _rw_set_loct::compute()
4848
{
4949
if(target->is_assign())
5050
{
51-
assert(target->code.operands().size()==2);
52-
assign(target->code.op0(), target->code.op1());
51+
const auto &assignment = target->get_assign();
52+
assign(assignment.lhs(), assignment.rhs());
5353
}
5454
else if(target->is_goto() ||
5555
target->is_assume() ||

‎src/goto-programs/goto_convert.cpp

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -317,18 +317,19 @@ void goto_convertt::convert_label(
317317
// the body of the thread is expected to be
318318
// in the operand.
319319
DATA_INVARIANT(
320-
code.op0().is_not_nil(), "op0 in magic thread creation label is null");
320+
to_code_label(code).code().is_not_nil(),
321+
"code() in magic thread creation label is null");
321322

322323
// replace the magic thread creation label with a
323324
// thread block (START_THREAD...END_THREAD).
324325
code_blockt thread_body;
325-
thread_body.add(to_code(code.op0()));
326+
thread_body.add(to_code_label(code).code());
326327
thread_body.add_source_location()=code.source_location();
327328
generate_thread_block(thread_body, dest, mode);
328329
}
329330
else
330331
{
331-
convert(to_code(code.op0()), tmp, mode);
332+
convert(to_code_label(code).code(), tmp, mode);
332333

333334
goto_programt::targett target=tmp.instructions.begin();
334335
dest.destructive_append(tmp);

‎src/jsil/jsil_typecheck.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -840,10 +840,10 @@ void jsil_typecheckt::typecheck_ifthenelse(code_ifthenelset &code)
840840

841841
void jsil_typecheckt::typecheck_assign(code_assignt &code)
842842
{
843-
typecheck_expr(code.op0());
844-
typecheck_expr(code.op1());
843+
typecheck_expr(code.lhs());
844+
typecheck_expr(code.rhs());
845845

846-
make_type_compatible(code.op0(), code.op1().type(), false);
846+
make_type_compatible(code.lhs(), code.rhs().type(), false);
847847
}
848848

849849
/// typechecking procedure declaration; any other symbols should have been

‎src/pointer-analysis/goto_program_dereference.cpp

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -326,8 +326,9 @@ void goto_program_dereferencet::dereference_instruction(
326326
function_call.function(),
327327
checks_only,
328328
value_set_dereferencet::modet::READ);
329-
dereference_expr(
330-
function_call.op2(), checks_only, value_set_dereferencet::modet::READ);
329+
330+
for(auto &arg : function_call.arguments())
331+
dereference_expr(arg, checks_only, value_set_dereferencet::modet::READ);
331332
}
332333
else if(i.is_return())
333334
{

‎src/pointer-analysis/value_set.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1525,7 +1525,7 @@ void value_sett::apply_code_rec(
15251525
}
15261526
else if(statement==ID_assume)
15271527
{
1528-
guard(to_code_assume(code).op0(), ns);
1528+
guard(to_code_assume(code).assumption(), ns);
15291529
}
15301530
else if(statement==ID_user_specified_predicate ||
15311531
statement==ID_user_specified_parameter_predicates ||

‎src/util/std_code.h

Lines changed: 132 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -251,6 +251,12 @@ class code_skipt:public codet
251251
code_skipt():codet(ID_skip)
252252
{
253253
}
254+
255+
protected:
256+
using codet::op0;
257+
using codet::op1;
258+
using codet::op2;
259+
using codet::op3;
254260
};
255261

256262
template<> inline bool can_cast_expr<code_skipt>(const exprt &base)
@@ -330,6 +336,12 @@ class code_assignt:public codet
330336

331337
validate(code, ns, vm);
332338
}
339+
340+
protected:
341+
using codet::op0;
342+
using codet::op1;
343+
using codet::op2;
344+
using codet::op3;
333345
};
334346

335347
template<> inline bool can_cast_expr<code_assignt>(const exprt &base)
@@ -468,6 +480,12 @@ class code_deadt:public codet
468480
"removing a non-symbol: " +
469481
id2string(to_symbol_expr(code.op0()).get_identifier()) + "from scope");
470482
}
483+
484+
protected:
485+
using codet::op0;
486+
using codet::op1;
487+
using codet::op2;
488+
using codet::op3;
471489
};
472490

473491
template<> inline bool can_cast_expr<code_deadt>(const exprt &base)
@@ -525,6 +543,12 @@ class code_assumet:public codet
525543
{
526544
return op0();
527545
}
546+
547+
protected:
548+
using codet::op0;
549+
using codet::op1;
550+
using codet::op2;
551+
using codet::op3;
528552
};
529553

530554
template<> inline bool can_cast_expr<code_assumet>(const exprt &base)
@@ -576,6 +600,12 @@ class code_assertt:public codet
576600
{
577601
return op0();
578602
}
603+
604+
protected:
605+
using codet::op0;
606+
using codet::op1;
607+
using codet::op2;
608+
using codet::op3;
579609
};
580610

581611
template<> inline bool can_cast_expr<code_assertt>(const exprt &base)
@@ -679,6 +709,12 @@ class code_ifthenelset:public codet
679709
{
680710
return static_cast<codet &>(op2());
681711
}
712+
713+
protected:
714+
using codet::op0;
715+
using codet::op1;
716+
using codet::op2;
717+
using codet::op3;
682718
};
683719

684720
template<> inline bool can_cast_expr<code_ifthenelset>(const exprt &base)
@@ -741,6 +777,12 @@ class code_switcht:public codet
741777
{
742778
return static_cast<codet &>(op1());
743779
}
780+
781+
protected:
782+
using codet::op0;
783+
using codet::op1;
784+
using codet::op2;
785+
using codet::op3;
744786
};
745787

746788
template<> inline bool can_cast_expr<code_switcht>(const exprt &base)
@@ -801,6 +843,12 @@ class code_whilet:public codet
801843
{
802844
return static_cast<codet &>(op1());
803845
}
846+
847+
protected:
848+
using codet::op0;
849+
using codet::op1;
850+
using codet::op2;
851+
using codet::op3;
804852
};
805853

806854
template<> inline bool can_cast_expr<code_whilet>(const exprt &base)
@@ -861,6 +909,12 @@ class code_dowhilet:public codet
861909
{
862910
return static_cast<codet &>(op1());
863911
}
912+
913+
protected:
914+
using codet::op0;
915+
using codet::op1;
916+
using codet::op2;
917+
using codet::op3;
864918
};
865919

866920
template<> inline bool can_cast_expr<code_dowhilet>(const exprt &base)
@@ -950,6 +1004,12 @@ class code_fort:public codet
9501004
{
9511005
return static_cast<codet &>(op3());
9521006
}
1007+
1008+
protected:
1009+
using codet::op0;
1010+
using codet::op1;
1011+
using codet::op2;
1012+
using codet::op3;
9531013
};
9541014

9551015
template<> inline bool can_cast_expr<code_fort>(const exprt &base)
@@ -999,6 +1059,12 @@ class code_gotot:public codet
9991059
{
10001060
return get(ID_destination);
10011061
}
1062+
1063+
protected:
1064+
using codet::op0;
1065+
using codet::op1;
1066+
using codet::op2;
1067+
using codet::op3;
10021068
};
10031069

10041070
template<> inline bool can_cast_expr<code_gotot>(const exprt &base)
@@ -1152,6 +1218,12 @@ class code_function_callt:public codet
11521218

11531219
validate(code, ns, vm);
11541220
}
1221+
1222+
protected:
1223+
using codet::op0;
1224+
using codet::op1;
1225+
using codet::op2;
1226+
using codet::op3;
11551227
};
11561228

11571229
template<> inline bool can_cast_expr<code_function_callt>(const exprt &base)
@@ -1216,6 +1288,12 @@ class code_returnt:public codet
12161288
{
12171289
DATA_CHECK(vm, code.operands().size() == 1, "return must have one operand");
12181290
}
1291+
1292+
protected:
1293+
using codet::op0;
1294+
using codet::op1;
1295+
using codet::op2;
1296+
using codet::op3;
12191297
};
12201298

12211299
template<> inline bool can_cast_expr<code_returnt>(const exprt &base)
@@ -1285,6 +1363,12 @@ class code_labelt:public codet
12851363
{
12861364
return static_cast<const codet &>(op0());
12871365
}
1366+
1367+
protected:
1368+
using codet::op0;
1369+
using codet::op1;
1370+
using codet::op2;
1371+
using codet::op3;
12881372
};
12891373

12901374
template<> inline bool can_cast_expr<code_labelt>(const exprt &base)
@@ -1356,6 +1440,12 @@ class code_switch_caset:public codet
13561440
{
13571441
return static_cast<const codet &>(op1());
13581442
}
1443+
1444+
protected:
1445+
using codet::op0;
1446+
using codet::op1;
1447+
using codet::op2;
1448+
using codet::op3;
13591449
};
13601450

13611451
template<> inline bool can_cast_expr<code_switch_caset>(const exprt &base)
@@ -1392,6 +1482,12 @@ class code_breakt:public codet
13921482
code_breakt():codet(ID_break)
13931483
{
13941484
}
1485+
1486+
protected:
1487+
using codet::op0;
1488+
using codet::op1;
1489+
using codet::op2;
1490+
using codet::op3;
13951491
};
13961492

13971493
template<> inline bool can_cast_expr<code_breakt>(const exprt &base)
@@ -1422,6 +1518,12 @@ class code_continuet:public codet
14221518
code_continuet():codet(ID_continue)
14231519
{
14241520
}
1521+
1522+
protected:
1523+
using codet::op0;
1524+
using codet::op1;
1525+
using codet::op2;
1526+
using codet::op3;
14251527
};
14261528

14271529
template<> inline bool can_cast_expr<code_continuet>(const exprt &base)
@@ -1511,6 +1613,12 @@ class code_expressiont:public codet
15111613
{
15121614
return op0();
15131615
}
1616+
1617+
protected:
1618+
using codet::op0;
1619+
using codet::op1;
1620+
using codet::op2;
1621+
using codet::op3;
15141622
};
15151623

15161624
template<> inline bool can_cast_expr<code_expressiont>(const exprt &base)
@@ -1988,6 +2096,12 @@ class code_push_catcht:public codet
19882096
const exception_listt &exception_list() const {
19892097
return (const exception_listt &)find(ID_exception_list).get_sub();
19902098
}
2099+
2100+
protected:
2101+
using codet::op0;
2102+
using codet::op1;
2103+
using codet::op2;
2104+
using codet::op3;
19912105
};
19922106

19932107
template<> inline bool can_cast_expr<code_push_catcht>(const exprt &base)
@@ -2019,6 +2133,12 @@ class code_pop_catcht:public codet
20192133
code_pop_catcht():codet(ID_pop_catch)
20202134
{
20212135
}
2136+
2137+
protected:
2138+
using codet::op0;
2139+
using codet::op1;
2140+
using codet::op2;
2141+
using codet::op3;
20222142
};
20232143

20242144
template<> inline bool can_cast_expr<code_pop_catcht>(const exprt &base)
@@ -2064,6 +2184,12 @@ class code_landingpadt:public codet
20642184
{
20652185
return op0();
20662186
}
2187+
2188+
protected:
2189+
using codet::op0;
2190+
using codet::op1;
2191+
using codet::op2;
2192+
using codet::op3;
20672193
};
20682194

20692195
template<> inline bool can_cast_expr<code_landingpadt>(const exprt &base)
@@ -2140,6 +2266,12 @@ class code_try_catcht:public codet
21402266
{
21412267
add_to_operands(to_catch, code_catch);
21422268
}
2269+
2270+
protected:
2271+
using codet::op0;
2272+
using codet::op1;
2273+
using codet::op2;
2274+
using codet::op3;
21432275
};
21442276

21452277
template<> inline bool can_cast_expr<code_try_catcht>(const exprt &base)

0 commit comments

Comments
 (0)