@@ -104,7 +104,9 @@ exprt make_or_update_initialiser(
104
104
const std::set<taint_instrumentert::automaton_variable_idt> &
105
105
names_of_shadow_variables)
106
106
{
107
- if (new_type.id ()!=ID_struct)
107
+ if (new_type.id ()!=ID_struct ||
108
+ (initialiser.id () == ID_side_effect &&
109
+ to_side_effect_expr (initialiser).get_statement () == ID_nondet))
108
110
{
109
111
// Rewrite type regardless, for example to turn (array*)null into
110
112
// (wrapped_array*)null
@@ -308,6 +310,7 @@ exprt taint_instrumentert::drive_access_path_through_super_classes(
308
310
namespacet (get_instrumented_symbol_table ())));
309
311
const typet &fixed_type=static_cast <const typet &>(fixed_type_irep);
310
312
bool result_type_changed=fixed_type!=access_path.type ();
313
+ const auto &full_fixed_type = instrumented_namespace.follow (fixed_type);
311
314
312
315
if (const auto symbol=expr_try_dynamic_cast<symbol_exprt>(access_path))
313
316
{
@@ -381,6 +384,60 @@ exprt taint_instrumentert::drive_access_path_through_super_classes(
381
384
result.op0 ()=unary_op;
382
385
return result;
383
386
}
387
+ else if (access_path.id () == ID_typecast &&
388
+ is_primitive_type (access_path.type ()) &&
389
+ full_fixed_type.id () == ID_struct)
390
+ {
391
+ // Special case for handling typecasts of instances of wrapped primitive
392
+ // data types. We resolve the typecast so that we build the struct
393
+ // initialiser for the wrapper type and we initialise all members by making
394
+ // accesses to the corresponding members in the origin wrapped access path.
395
+ exprt uncast_access_path = access_path;
396
+ while (uncast_access_path.id () == ID_typecast)
397
+ uncast_access_path = to_typecast_expr (uncast_access_path).op ();
398
+ uncast_access_path =
399
+ drive_access_path_through_super_classes (uncast_access_path);
400
+ const typet uncasted_access_path_type =
401
+ instrumented_namespace.follow (uncast_access_path.type ());
402
+ struct_exprt struct_expr (fixed_type);
403
+ // First we set the super instance (i.e. '@__CPROVER__super' member,
404
+ // which is actually the instance of the primitive type).
405
+ struct_expr.operands ().push_back (
406
+ typecast_exprt (
407
+ get_super_if_subclassed (
408
+ uncast_access_path,
409
+ get_inverse_type_substitutions (),
410
+ get_instrumented_symbol_table ()),
411
+ access_path.type ()));
412
+ // Next we iterate over all shadow variables in the fixed (final) type
413
+ // and we set each of them either the value of the corresponding shadow
414
+ // variable in the original expression (if it has that shadow variable),
415
+ // or we set it to FALSE.
416
+ // NOTE: Wrapper structures of primitive data types always have only
417
+ // the super instance and shadow variables (so, nothing else!).
418
+ for (const auto &component : to_struct_type (full_fixed_type).components ())
419
+ {
420
+ // We have to skip the super instance.
421
+ if (names_of_shadow_variables.count (as_string (
422
+ component.get_name ())) != 0UL )
423
+ {
424
+ if (uncasted_access_path_type.id () == ID_struct &&
425
+ to_struct_type (uncasted_access_path_type).has_component (
426
+ component.get_name ())
427
+ )
428
+ {
429
+ struct_expr.operands ().push_back (member_exprt (
430
+ uncast_access_path, component.get_name (), bool_typet ()));
431
+ }
432
+ else
433
+ {
434
+ struct_expr.operands ().push_back (
435
+ constant_exprt (ID_false, bool_typet ()));
436
+ }
437
+ }
438
+ }
439
+ return struct_expr;
440
+ }
384
441
else
385
442
{
386
443
// Default case: apply transformation to operands; apply operation to
@@ -393,7 +450,6 @@ exprt taint_instrumentert::drive_access_path_through_super_classes(
393
450
op=get_super_if_subclassed (
394
451
op, get_inverse_type_substitutions (), get_instrumented_symbol_table ());
395
452
}
396
-
397
453
result=make_or_update_initialiser (
398
454
result,
399
455
instrumented_namespace.follow (fixed_type),
@@ -528,6 +584,42 @@ void taint_instrumentert::instrument_instructions_with_shadow_variables(
528
584
{
529
585
asgn.lhs ()=drive_access_path_through_super_classes (asgn.lhs ());
530
586
asgn.rhs ()=drive_access_path_through_super_classes (asgn.rhs ());
587
+
588
+ // There is a possibility, that asgn.lhs().type()!=asgn.rhs().type().
589
+ // This may occur only when asgn.rhs().type() is a wrapper of
590
+ // a primitive data type and asgn.lhs() is an unwrapped primitive
591
+ // (e.g. array length) that cannot carry taint.
592
+ // The code below resolves the inconsistency, by applying member
593
+ // access to the super field of the asgn.rhs() until we get to
594
+ // the right one.
595
+
596
+ const auto &lhs_type =
597
+ instrumented_namespace.follow (asgn.lhs ().type ());
598
+ while (true )
599
+ {
600
+ const auto &rhs_type =
601
+ instrumented_namespace.follow (asgn.rhs ().type ());
602
+
603
+ // We check whether the inconsistency is not present (or has been
604
+ // fixed already).
605
+ if (rhs_type.id () != ID_struct || (lhs_type.id () == ID_struct &&
606
+ to_struct_type (lhs_type).get_tag () ==
607
+ to_struct_type (rhs_type).get_tag ()))
608
+ {
609
+ break ;
610
+ }
611
+
612
+ // And we fix the inconsistency by accessing the super instance (
613
+ // i.e. the wrapped type).
614
+ const auto &struct_type = to_struct_type (rhs_type);
615
+ INVARIANT (
616
+ struct_type.has_component (taint_name_of_super_variable ()),
617
+ " Assignment has type mismatch that couldn't be resolved by "
618
+ " unwrapping the rhs." );
619
+ asgn.rhs () = member_exprt (
620
+ asgn.rhs (),
621
+ struct_type.get_component (taint_name_of_super_variable ()));
622
+ }
531
623
}
532
624
}
533
625
break ;
0 commit comments