Example: pointer_copy_user_ctrlflow_bytewise.c

#include <stdio.h>
#include <string.h>
#include <assert.h>
#include <limits.h>
int x=1;
unsigned char control_flow_copy(unsigned char c) {
assert(UCHAR_MAX==255);
switch (c) {
case 0: return(0);
case 1: return(1);
case 2: return(2);
case 3: return(3);
case 4: return(4);
case 5: return(5);
case 6: return(6);
case 7: return(7);
case 8: return(8);
case 9: return(9);
case 10: return(10);
case 11: return(11);
case 12: return(12);
case 13: return(13);
case 14: return(14);
case 15: return(15);
case 16: return(16);
case 17: return(17);
case 18: return(18);
case 19: return(19);
case 20: return(20);
case 21: return(21);
case 22: return(22);
case 23: return(23);
case 24: return(24);
case 25: return(25);
case 26: return(26);
case 27: return(27);
case 28: return(28);
case 29: return(29);
case 30: return(30);
case 31: return(31);
case 32: return(32);
case 33: return(33);
case 34: return(34);
case 35: return(35);
case 36: return(36);
case 37: return(37);
case 38: return(38);
case 39: return(39);
case 40: return(40);
case 41: return(41);
case 42: return(42);
case 43: return(43);
case 44: return(44);
case 45: return(45);
case 46: return(46);
case 47: return(47);
case 48: return(48);
case 49: return(49);
case 50: return(50);
case 51: return(51);
case 52: return(52);
case 53: return(53);
case 54: return(54);
case 55: return(55);
case 56: return(56);
case 57: return(57);
case 58: return(58);
case 59: return(59);
case 60: return(60);
case 61: return(61);
case 62: return(62);
case 63: return(63);
case 64: return(64);
case 65: return(65);
case 66: return(66);
case 67: return(67);
case 68: return(68);
case 69: return(69);
case 70: return(70);
case 71: return(71);
case 72: return(72);
case 73: return(73);
case 74: return(74);
case 75: return(75);
case 76: return(76);
case 77: return(77);
case 78: return(78);
case 79: return(79);
case 80: return(80);
case 81: return(81);
case 82: return(82);
case 83: return(83);
case 84: return(84);
case 85: return(85);
case 86: return(86);
case 87: return(87);
case 88: return(88);
case 89: return(89);
case 90: return(90);
case 91: return(91);
case 92: return(92);
case 93: return(93);
case 94: return(94);
case 95: return(95);
case 96: return(96);
case 97: return(97);
case 98: return(98);
case 99: return(99);
case 100: return(100);
case 101: return(101);
case 102: return(102);
case 103: return(103);
case 104: return(104);
case 105: return(105);
case 106: return(106);
case 107: return(107);
case 108: return(108);
case 109: return(109);
case 110: return(110);
case 111: return(111);
case 112: return(112);
case 113: return(113);
case 114: return(114);
case 115: return(115);
case 116: return(116);
case 117: return(117);
case 118: return(118);
case 119: return(119);
case 120: return(120);
case 121: return(121);
case 122: return(122);
case 123: return(123);
case 124: return(124);
case 125: return(125);
case 126: return(126);
case 127: return(127);
case 128: return(128);
case 129: return(129);
case 130: return(130);
case 131: return(131);
case 132: return(132);
case 133: return(133);
case 134: return(134);
case 135: return(135);
case 136: return(136);
case 137: return(137);
case 138: return(138);
case 139: return(139);
case 140: return(140);
case 141: return(141);
case 142: return(142);
case 143: return(143);
case 144: return(144);
case 145: return(145);
case 146: return(146);
case 147: return(147);
case 148: return(148);
case 149: return(149);
case 150: return(150);
case 151: return(151);
case 152: return(152);
case 153: return(153);
case 154: return(154);
case 155: return(155);
case 156: return(156);
case 157: return(157);
case 158: return(158);
case 159: return(159);
case 160: return(160);
case 161: return(161);
case 162: return(162);
case 163: return(163);
case 164: return(164);
case 165: return(165);
case 166: return(166);
case 167: return(167);
case 168: return(168);
case 169: return(169);
case 170: return(170);
case 171: return(171);
case 172: return(172);
case 173: return(173);
case 174: return(174);
case 175: return(175);
case 176: return(176);
case 177: return(177);
case 178: return(178);
case 179: return(179);
case 180: return(180);
case 181: return(181);
case 182: return(182);
case 183: return(183);
case 184: return(184);
case 185: return(185);
case 186: return(186);
case 187: return(187);
case 188: return(188);
case 189: return(189);
case 190: return(190);
case 191: return(191);
case 192: return(192);
case 193: return(193);
case 194: return(194);
case 195: return(195);
case 196: return(196);
case 197: return(197);
case 198: return(198);
case 199: return(199);
case 200: return(200);
case 201: return(201);
case 202: return(202);
case 203: return(203);
case 204: return(204);
case 205: return(205);
case 206: return(206);
case 207: return(207);
case 208: return(208);
case 209: return(209);
case 210: return(210);
case 211: return(211);
case 212: return(212);
case 213: return(213);
case 214: return(214);
case 215: return(215);
case 216: return(216);
case 217: return(217);
case 218: return(218);
case 219: return(219);
case 220: return(220);
case 221: return(221);
case 222: return(222);
case 223: return(223);
case 224: return(224);
case 225: return(225);
case 226: return(226);
case 227: return(227);
case 228: return(228);
case 229: return(229);
case 230: return(230);
case 231: return(231);
case 232: return(232);
case 233: return(233);
case 234: return(234);
case 235: return(235);
case 236: return(236);
case 237: return(237);
case 238: return(238);
case 239: return(239);
case 240: return(240);
case 241: return(241);
case 242: return(242);
case 243: return(243);
case 244: return(244);
case 245: return(245);
case 246: return(246);
case 247: return(247);
case 248: return(248);
case 249: return(249);
case 250: return(250);
case 251: return(251);
case 252: return(252);
case 253: return(253);
case 254: return(254);
case 255: return(255);
}
}

void user_memcpy2(unsigned char* dest,
unsigned char *src, size_t n) {
while (n > 0) {
*dest = control_flow_copy(*src);
src += 1;
dest += 1;
n -= 1;
}
}
int main() {
int *p = &x;
int *q;
user_memcpy2((unsigned char*)&q, (unsigned char*)&p,
sizeof(p));
*q = 11; // does this have undefined behaviour?
printf("*p=%d *q=%d\n",*p,*q);
}
[link to test in Cerberus and Compiler Explorer]

Experimental data (what does this mean?)

gcc-8.1-O0 *p=11 *q=11
gcc-8.1-O2 *p=11 *q=11
gcc-8.1-O3 *p=11 *q=11
gcc-8.1-O2-no-strict-aliasing *p=11 *q=11
gcc-8.1-O3-no-strict-aliasing *p=11 *q=11
clang-6.0-O0 pointer_copy_user_ctrlflow_bytewise.c:266:1: warning: control may reach end of non-void function [-Wreturn-type]
}
^
1 warning generated.
*p=11 *q=11
clang-6.0-O2 pointer_copy_user_ctrlflow_bytewise.c:266:1: warning: control may reach end of non-void function [-Wreturn-type]
}
^
1 warning generated.
*p=11 *q=11
clang-6.0-O3 pointer_copy_user_ctrlflow_bytewise.c:266:1: warning: control may reach end of non-void function [-Wreturn-type]
}
^
1 warning generated.
*p=11 *q=11
clang-6.0-O2-no-strict-aliasing pointer_copy_user_ctrlflow_bytewise.c:266:1: warning: control may reach end of non-void function [-Wreturn-type]
}
^
1 warning generated.
*p=11 *q=11
clang-6.0-O3-no-strict-aliasing pointer_copy_user_ctrlflow_bytewise.c:266:1: warning: control may reach end of non-void function [-Wreturn-type]
}
^
1 warning generated.
*p=11 *q=11
clang-6.0-UBSAN pointer_copy_user_ctrlflow_bytewise.c:266:1: warning: control may reach end of non-void function [-Wreturn-type]
}
^
1 warning generated.
*p=11 *q=11
clang-6.0-ASAN pointer_copy_user_ctrlflow_bytewise.c:266:1: warning: control may reach end of non-void function [-Wreturn-type]
}
^
1 warning generated.
*p=11 *q=11
clang-6.0-MSAN pointer_copy_user_ctrlflow_bytewise.c:266:1: warning: control may reach end of non-void function [-Wreturn-type]
}
^
1 warning generated.
*p=11 *q=11
icc-19-O0 pointer_copy_user_ctrlflow_bytewise.c(266): warning #1011: missing return statement at end of non-void function "control_flow_copy"
}
^

*p=11 *q=11
icc-19-O2 pointer_copy_user_ctrlflow_bytewise.c(266): warning #1011: missing return statement at end of non-void function "control_flow_copy"
}
^

*p=11 *q=11
icc-19-O3 pointer_copy_user_ctrlflow_bytewise.c(266): warning #1011: missing return statement at end of non-void function "control_flow_copy"
}
^

*p=11 *q=11
icc-19-O2-no-strict-aliasing pointer_copy_user_ctrlflow_bytewise.c(266): warning #1011: missing return statement at end of non-void function "control_flow_copy"
}
^

*p=11 *q=11
icc-19-O3-no-strict-aliasing pointer_copy_user_ctrlflow_bytewise.c(266): warning #1011: missing return statement at end of non-void function "control_flow_copy"
}
^

*p=11 *q=11
cerberus-concrete BEGIN EXEC[0]
Undefined [pointer_copy_user_ctrlflow_bytewise.c:282:3-5]{id: [UB043_indirection_invalid_value]}
END EXEC[0]
Time spent: 0.101601 seconds
cerberus-symbolic exit codes: compile 0 / execute 1 cerberus: internal error, uncaught exception:
Failure("TODO: Symbolic defacto, isWellAligned_ptrval")

gcc-4.9-shadowprov exit codes: compile 0 / execute 134
CHERI:MIPS-O0 pointer_copy_user_ctrlflow_bytewise.c:266:1: warning: control may reach end of non-void function [-Wreturn-type]
}
^
1 warning generated.
*p=11 *q=11
CHERI:MIPS-O2 pointer_copy_user_ctrlflow_bytewise.c:266:1: warning: control may reach end of non-void function [-Wreturn-type]
}
^
1 warning generated.
*p=11 *q=11
CHERI:MIPS-O2-no-strict-aliasing pointer_copy_user_ctrlflow_bytewise.c:266:1: warning: control may reach end of non-void function [-Wreturn-type]
}
^
1 warning generated.
*p=11 *q=11
CHERI:CHERI-O0-uintcap-addr-exact-equals exit codes: compile 0 / execute -1 Terminated with signal 34: In-address space security exceptionpointer_copy_user_ctrlflow_bytewise.c:266:1: warning: control may reach end of non-void function [-Wreturn-type]
}
^
1 warning generated.
CHERI:CHERI-O2-uintcap-addr-exact-equals exit codes: compile 0 / execute -1 Terminated with signal 34: In-address space security exceptionpointer_copy_user_ctrlflow_bytewise.c:266:1: warning: control may reach end of non-void function [-Wreturn-type]
}
^
1 warning generated.
CHERI:CHERI-O2-no-strict-aliasing-uintcap-addr-exact-equals exit codes: compile 0 / execute -1 Terminated with signal 34: In-address space security exceptionpointer_copy_user_ctrlflow_bytewise.c:266:1: warning: control may reach end of non-void function [-Wreturn-type]
}
^
1 warning generated.
CHERI:CHERI-O0-uintcap-offset-exact-equals exit codes: compile 0 / execute -1 Terminated with signal 34: In-address space security exceptionpointer_copy_user_ctrlflow_bytewise.c:266:1: warning: control may reach end of non-void function [-Wreturn-type]
}
^
1 warning generated.
CHERI:CHERI-O2-uintcap-offset-exact-equals exit codes: compile 0 / execute -1 Terminated with signal 34: In-address space security exceptionpointer_copy_user_ctrlflow_bytewise.c:266:1: warning: control may reach end of non-void function [-Wreturn-type]
}
^
1 warning generated.
CHERI:CHERI-O2-no-strict-aliasing-uintcap-offset-exact-equals exit codes: compile 0 / execute -1 Terminated with signal 34: In-address space security exceptionpointer_copy_user_ctrlflow_bytewise.c:266:1: warning: control may reach end of non-void function [-Wreturn-type]
}
^
1 warning generated.
CHERI:CHERI-O0-uintcap-addr exit codes: compile 0 / execute -1 Terminated with signal 34: In-address space security exceptionpointer_copy_user_ctrlflow_bytewise.c:266:1: warning: control may reach end of non-void function [-Wreturn-type]
}
^
1 warning generated.
CHERI:CHERI-O2-uintcap-addr exit codes: compile 0 / execute -1 Terminated with signal 34: In-address space security exceptionpointer_copy_user_ctrlflow_bytewise.c:266:1: warning: control may reach end of non-void function [-Wreturn-type]
}
^
1 warning generated.
CHERI:CHERI-O2-no-strict-aliasing-uintcap-addr exit codes: compile 0 / execute -1 Terminated with signal 34: In-address space security exceptionpointer_copy_user_ctrlflow_bytewise.c:266:1: warning: control may reach end of non-void function [-Wreturn-type]
}
^
1 warning generated.
CHERI:CHERI-O0-uintcap-offset exit codes: compile 0 / execute -1 Terminated with signal 34: In-address space security exceptionpointer_copy_user_ctrlflow_bytewise.c:266:1: warning: control may reach end of non-void function [-Wreturn-type]
}
^
1 warning generated.
CHERI:CHERI-O2-uintcap-offset exit codes: compile 0 / execute -1 Terminated with signal 34: In-address space security exceptionpointer_copy_user_ctrlflow_bytewise.c:266:1: warning: control may reach end of non-void function [-Wreturn-type]
}
^
1 warning generated.
CHERI:CHERI-O2-no-strict-aliasing-uintcap-offset exit codes: compile 0 / execute -1 Terminated with signal 34: In-address space security exceptionpointer_copy_user_ctrlflow_bytewise.c:266:1: warning: control may reach end of non-void function [-Wreturn-type]
}
^
1 warning generated.
RV-Match exit codes: compile 0 / execute 1
ch2o pointer_copy_user_ctrlflow_bytewise.c:3:10: fatal error: assert.h: No such file or directory
#include <assert.h>
^~~~~~~~~~
compilation terminated.
compcert-3.2 pointer_copy_user_ctrlflow_bytewise.c:6: warning: control reaches end of non-void function [-Wreturn-type]
*p=11 *q=11
compcert-3.2-O pointer_copy_user_ctrlflow_bytewise.c:6: warning: control reaches end of non-void function [-Wreturn-type]
*p=11 *q=11
compcert-3.2-interp Time 0: calling main()
--[step_internal_function]-->
Time 1: in function main, statement
p = &x;
user_memcpy2((unsigned char *) &q, (unsigned char *) &p, sizeof(int *));
*q = 11;
printf(__stringlit_4, *p, *q);
return 0;
--[step_seq]-->
Time 2: in function main, statement
p = &x;
user_memcpy2((unsigned char *) &q, (unsigned char *) &p, sizeof(int *));
*q = 11;
printf(__stringlit_4, *p, *q);
--[step_seq]-->
Time 3: in function main, statement p = &x;
--[step_do_1]-->
Time 4: in function main, expression p = &x
--[red_var_local]-->
Time 5: in function main, expression <loc p> = &x
--[red_var_global]-->
Time 6: in function main, expression <loc p> = &<loc x>
--[red_addrof]-->
Time 7: in function main, expression <loc p> = <ptr x>
--[red_assign]-->
Time 8: in function main, expression <ptr x>
--[step_do_2]-->
Time 9: in function main, statement /*skip*/;
--[step_skip_seq]-->
Time 10: in function main, statement
user_memcpy2((unsigned char *) &q, (unsigned char *) &p, sizeof(int *));
*q = 11;
printf(__stringlit_4, *p, *q);
--[step_seq]-->
Time 11: in function main, statement
user_memcpy2((unsigned char *) &q, (unsigned char *) &p, sizeof(int *));
--[step_do_1]-->
Time 12: in function main, expression
user_memcpy2((unsigned char *) &q, (unsigned char *) &p, sizeof(int *))
--[red_var_global]-->
Time 13: in function main, expression
<loc user_memcpy2>((unsigned char *) &q,
(unsigned char *) &p,
sizeof(int *))
--[red_rvalof]-->
Time 14: in function main, expression
<ptr user_memcpy2>((unsigned char *) &q,
(unsigned char *) &p,
sizeof(int *))
--[red_var_local]-->
Time 15: in function main, expression
<ptr user_memcpy2>((unsigned char *) &<loc q>,
(unsigned char *) &p,
sizeof(int *))
--[red_addrof]-->
Time 16: in function main, expression
<ptr user_memcpy2>((unsigned char *) <ptr q>,
(unsigned char *) &p,
sizeof(int *))
--[red_cast]-->
Time 17: in function main, expression
<ptr user_memcpy2>(<ptr q>, (unsigned char *) &p, sizeof(int *))
--[red_var_local]-->
Time 18: in function main, expression
<ptr user_memcpy2>(<ptr q>, (unsigned char *) &<loc p>, sizeof(int *))
--[red_addrof]-->
Time 19: in function main, expression
<ptr user_memcpy2>(<ptr q>, (unsigned char *) <ptr p>, sizeof(int *))
--[red_cast]-->
Time 20: in function main, expression
<ptr user_memcpy2>(<ptr q>, <ptr p>, sizeof(int *))
--[red_sizeof]-->
Time 21: in function main, expression
<ptr user_memcpy2>(<ptr q>, <ptr p>, 4U)
--[red_call]-->
Time 22: calling user_memcpy2(<ptr>, <ptr>, 4)
--[step_internal_function]-->
Time 23: in function user_memcpy2, statement
while (n > 0) {
*dest = control_flow_copy(*.);
src += 1;
dest += 1;
n -= 1;
}
--[step_while]-->
Time 24: in function user_memcpy2, expression n > 0
--[red_var_local]-->
Time 25: in function user_memcpy2, expression <loc n> > 0
--[red_rvalof]-->
Time 26: in function user_memcpy2, expression 4U > 0
--[red_binop]-->
Time 27: in function user_memcpy2, expression 1
--[step_while_true]-->
Time 28: in function user_memcpy2, statement
*dest = control_flow_copy(*.); src += 1; dest += 1; n -= 1;
--[step_seq]-->
Time 29: in function user_memcpy2, statement *dest = control_flow_copy(*.);
--[step_do_1]-->
Time 30: in function user_memcpy2, expression *dest = control_flow_copy(*.)
--[red_var_local]-->
Time 31: in function user_memcpy2, expression
*<loc dest> = control_flow_copy(*.)
--[red_rvalof]-->
Time 32: in function user_memcpy2, expression *<ptr> = control_flow_copy(*.)
--[red_deref]-->
Time 33: in function user_memcpy2, expression <loc> = control_flow_copy(*.)
--[red_var_global]-->
Time 34: in function user_memcpy2, expression
<loc> = <loc control_flow_copy>(*.)
--[red_rvalof]-->
Time 35: in function user_memcpy2, expression
<loc> = <ptr control_flow_copy>(*.)
--[red_var_local]-->
Time 36: in function user_memcpy2, expression
<loc> = <ptr control_flow_copy>(*.)
--[red_rvalof]-->
Time 37: in function user_memcpy2, expression
<loc> = <ptr control_flow_copy>(*<ptr>)
--[red_deref]-->
Time 38: in function user_memcpy2, expression
<loc> = <ptr control_flow_copy>(<loc>)
--[red_rvalof]-->
Time 39: in function user_memcpy2, expression
<loc> = <ptr control_flow_copy>(<undef>)
Stuck state: in function user_memcpy2, expression
<loc> = <ptr control_flow_copy>(<undef>)
Stuck subexpression: <ptr control_flow_copy>(<undef>)
ERROR: Undefined behavior
In file included from pointer_copy_user_ctrlflow_bytewise.c:1:
In file included from /usr/include/stdio.h:64:
In file included from /usr/include/_stdio.h:68:
/usr/include/sys/cdefs.h:81:2: warning: "Unsupported compiler detected" [-W#warnings]
#warning "Unsupported compiler detected"
^
1 warning generated.
pointer_copy_user_ctrlflow_bytewise.c:6: warning: control reaches end of non-void function [-Wreturn-type]