Skip to content

Commit 5699c13

Browse files
author
Daniel Kroening
committed
protect opX in codet subclasses
This will prevent accesses that are not type safe.
1 parent 165c012 commit 5699c13

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
@@ -264,6 +264,12 @@ class code_skipt:public codet
264264
code_skipt():codet(ID_skip)
265265
{
266266
}
267+
268+
protected:
269+
using codet::op0;
270+
using codet::op1;
271+
using codet::op2;
272+
using codet::op3;
267273
};
268274

269275
template<> inline bool can_cast_expr<code_skipt>(const exprt &base)
@@ -343,6 +349,12 @@ class code_assignt:public codet
343349

344350
validate(code, ns, vm);
345351
}
352+
353+
protected:
354+
using codet::op0;
355+
using codet::op1;
356+
using codet::op2;
357+
using codet::op3;
346358
};
347359

348360
template<> inline bool can_cast_expr<code_assignt>(const exprt &base)
@@ -481,6 +493,12 @@ class code_deadt:public codet
481493
"removing a non-symbol: " +
482494
id2string(to_symbol_expr(code.op0()).get_identifier()) + "from scope");
483495
}
496+
497+
protected:
498+
using codet::op0;
499+
using codet::op1;
500+
using codet::op2;
501+
using codet::op3;
484502
};
485503

486504
template<> inline bool can_cast_expr<code_deadt>(const exprt &base)
@@ -538,6 +556,12 @@ class code_assumet:public codet
538556
{
539557
return op0();
540558
}
559+
560+
protected:
561+
using codet::op0;
562+
using codet::op1;
563+
using codet::op2;
564+
using codet::op3;
541565
};
542566

543567
template<> inline bool can_cast_expr<code_assumet>(const exprt &base)
@@ -589,6 +613,12 @@ class code_assertt:public codet
589613
{
590614
return op0();
591615
}
616+
617+
protected:
618+
using codet::op0;
619+
using codet::op1;
620+
using codet::op2;
621+
using codet::op3;
592622
};
593623

594624
template<> inline bool can_cast_expr<code_assertt>(const exprt &base)
@@ -692,6 +722,12 @@ class code_ifthenelset:public codet
692722
{
693723
return static_cast<codet &>(op2());
694724
}
725+
726+
protected:
727+
using codet::op0;
728+
using codet::op1;
729+
using codet::op2;
730+
using codet::op3;
695731
};
696732

697733
template<> inline bool can_cast_expr<code_ifthenelset>(const exprt &base)
@@ -754,6 +790,12 @@ class code_switcht:public codet
754790
{
755791
return static_cast<codet &>(op1());
756792
}
793+
794+
protected:
795+
using codet::op0;
796+
using codet::op1;
797+
using codet::op2;
798+
using codet::op3;
757799
};
758800

759801
template<> inline bool can_cast_expr<code_switcht>(const exprt &base)
@@ -814,6 +856,12 @@ class code_whilet:public codet
814856
{
815857
return static_cast<codet &>(op1());
816858
}
859+
860+
protected:
861+
using codet::op0;
862+
using codet::op1;
863+
using codet::op2;
864+
using codet::op3;
817865
};
818866

819867
template<> inline bool can_cast_expr<code_whilet>(const exprt &base)
@@ -874,6 +922,12 @@ class code_dowhilet:public codet
874922
{
875923
return static_cast<codet &>(op1());
876924
}
925+
926+
protected:
927+
using codet::op0;
928+
using codet::op1;
929+
using codet::op2;
930+
using codet::op3;
877931
};
878932

879933
template<> inline bool can_cast_expr<code_dowhilet>(const exprt &base)
@@ -963,6 +1017,12 @@ class code_fort:public codet
9631017
{
9641018
return static_cast<codet &>(op3());
9651019
}
1020+
1021+
protected:
1022+
using codet::op0;
1023+
using codet::op1;
1024+
using codet::op2;
1025+
using codet::op3;
9661026
};
9671027

9681028
template<> inline bool can_cast_expr<code_fort>(const exprt &base)
@@ -1012,6 +1072,12 @@ class code_gotot:public codet
10121072
{
10131073
return get(ID_destination);
10141074
}
1075+
1076+
protected:
1077+
using codet::op0;
1078+
using codet::op1;
1079+
using codet::op2;
1080+
using codet::op3;
10151081
};
10161082

10171083
template<> inline bool can_cast_expr<code_gotot>(const exprt &base)
@@ -1165,6 +1231,12 @@ class code_function_callt:public codet
11651231

11661232
validate(code, ns, vm);
11671233
}
1234+
1235+
protected:
1236+
using codet::op0;
1237+
using codet::op1;
1238+
using codet::op2;
1239+
using codet::op3;
11681240
};
11691241

11701242
template<> inline bool can_cast_expr<code_function_callt>(const exprt &base)
@@ -1229,6 +1301,12 @@ class code_returnt:public codet
12291301
{
12301302
DATA_CHECK(vm, code.operands().size() == 1, "return must have one operand");
12311303
}
1304+
1305+
protected:
1306+
using codet::op0;
1307+
using codet::op1;
1308+
using codet::op2;
1309+
using codet::op3;
12321310
};
12331311

12341312
template<> inline bool can_cast_expr<code_returnt>(const exprt &base)
@@ -1298,6 +1376,12 @@ class code_labelt:public codet
12981376
{
12991377
return static_cast<const codet &>(op0());
13001378
}
1379+
1380+
protected:
1381+
using codet::op0;
1382+
using codet::op1;
1383+
using codet::op2;
1384+
using codet::op3;
13011385
};
13021386

13031387
template<> inline bool can_cast_expr<code_labelt>(const exprt &base)
@@ -1369,6 +1453,12 @@ class code_switch_caset:public codet
13691453
{
13701454
return static_cast<const codet &>(op1());
13711455
}
1456+
1457+
protected:
1458+
using codet::op0;
1459+
using codet::op1;
1460+
using codet::op2;
1461+
using codet::op3;
13721462
};
13731463

13741464
template<> inline bool can_cast_expr<code_switch_caset>(const exprt &base)
@@ -1405,6 +1495,12 @@ class code_breakt:public codet
14051495
code_breakt():codet(ID_break)
14061496
{
14071497
}
1498+
1499+
protected:
1500+
using codet::op0;
1501+
using codet::op1;
1502+
using codet::op2;
1503+
using codet::op3;
14081504
};
14091505

14101506
template<> inline bool can_cast_expr<code_breakt>(const exprt &base)
@@ -1435,6 +1531,12 @@ class code_continuet:public codet
14351531
code_continuet():codet(ID_continue)
14361532
{
14371533
}
1534+
1535+
protected:
1536+
using codet::op0;
1537+
using codet::op1;
1538+
using codet::op2;
1539+
using codet::op3;
14381540
};
14391541

14401542
template<> inline bool can_cast_expr<code_continuet>(const exprt &base)
@@ -1524,6 +1626,12 @@ class code_expressiont:public codet
15241626
{
15251627
return op0();
15261628
}
1629+
1630+
protected:
1631+
using codet::op0;
1632+
using codet::op1;
1633+
using codet::op2;
1634+
using codet::op3;
15271635
};
15281636

15291637
template<> inline bool can_cast_expr<code_expressiont>(const exprt &base)
@@ -2001,6 +2109,12 @@ class code_push_catcht:public codet
20012109
const exception_listt &exception_list() const {
20022110
return (const exception_listt &)find(ID_exception_list).get_sub();
20032111
}
2112+
2113+
protected:
2114+
using codet::op0;
2115+
using codet::op1;
2116+
using codet::op2;
2117+
using codet::op3;
20042118
};
20052119

20062120
template<> inline bool can_cast_expr<code_push_catcht>(const exprt &base)
@@ -2032,6 +2146,12 @@ class code_pop_catcht:public codet
20322146
code_pop_catcht():codet(ID_pop_catch)
20332147
{
20342148
}
2149+
2150+
protected:
2151+
using codet::op0;
2152+
using codet::op1;
2153+
using codet::op2;
2154+
using codet::op3;
20352155
};
20362156

20372157
template<> inline bool can_cast_expr<code_pop_catcht>(const exprt &base)
@@ -2077,6 +2197,12 @@ class code_landingpadt:public codet
20772197
{
20782198
return op0();
20792199
}
2200+
2201+
protected:
2202+
using codet::op0;
2203+
using codet::op1;
2204+
using codet::op2;
2205+
using codet::op3;
20802206
};
20812207

20822208
template<> inline bool can_cast_expr<code_landingpadt>(const exprt &base)
@@ -2153,6 +2279,12 @@ class code_try_catcht:public codet
21532279
{
21542280
add_to_operands(to_catch, code_catch);
21552281
}
2282+
2283+
protected:
2284+
using codet::op0;
2285+
using codet::op1;
2286+
using codet::op2;
2287+
using codet::op3;
21562288
};
21572289

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

0 commit comments

Comments
 (0)