Example: pointer_offset_from_subtraction_1_malloc.c

#include <stdio.h>
#include <string.h> 
#include <stdint.h>
#include <stdlib.h>
#include <stddef.h>
#include <inttypes.h>
int main() {
  void *xp=malloc(sizeof(int)); // allocation P
  void *yp=malloc(sizeof(int)); // allocation Q
  *((int*)xp)=1;
  *((int*)yp)=2;
  ptrdiff_t offset=(unsigned char*)yp-(unsigned char*)xp; 
    // provenance ?
  unsigned char *p1 = (unsigned char*)xp;// provenance P
  unsigned char *p2 = p1 + offset;       // provenance ?
  int *p = (int*)p2;
  int *q = (int*)yp;
  printf("Addresses: p=%p q=%p "\
         " offset=%td \n",(void*)p,(void*)q,offset);
  if (memcmp(&p, &q, sizeof(p)) == 0) {
    *p = 11;  // is this free of undefined behaviour?
    printf("*xp=%d *yp=%d *p=%d *q=%d\n",
           *(int*)xp,*(int*)yp,*(int*)p,*(int*)q);
  }
  return 0;
}
[link to test in Cerberus and Compiler Explorer]

Experimental data (what does this mean?) 



gcc-8.1-O0 Addresses: p=0x21ae030 q=0x21ae030  offset=32 
*xp=1 *yp=11 *p=11 *q=11


gcc-8.1-O2 Addresses: p=0x1e30030 q=0x1e30030  offset=32 
*xp=1 *yp=11 *p=11 *q=11


gcc-8.1-O3 Addresses: p=0x1a44030 q=0x1a44030  offset=32 
*xp=1 *yp=11 *p=11 *q=11


gcc-8.1-O2-no-strict-aliasing Addresses: p=0x694030 q=0x694030  offset=32 
*xp=1 *yp=11 *p=11 *q=11


gcc-8.1-O3-no-strict-aliasing Addresses: p=0x18c4030 q=0x18c4030  offset=32 
*xp=1 *yp=11 *p=11 *q=11


clang-6.0-O0 Addresses: p=0x1e67030 q=0x1e67030  offset=32 
*xp=1 *yp=11 *p=11 *q=11


clang-6.0-O2 Addresses: p=0x1938030 q=0x1938030  offset=32 
*xp=1 *yp=11 *p=11 *q=11


clang-6.0-O3 Addresses: p=0x1013030 q=0x1013030  offset=32 
*xp=1 *yp=11 *p=11 *q=11


clang-6.0-O2-no-strict-aliasing Addresses: p=0x1f50030 q=0x1f50030  offset=32 
*xp=1 *yp=11 *p=11 *q=11


clang-6.0-O3-no-strict-aliasing Addresses: p=0xdde030 q=0xdde030  offset=32 
*xp=1 *yp=11 *p=11 *q=11


clang-6.0-UBSAN Addresses: p=0x29cb060 q=0x29cb060  offset=32 
*xp=1 *yp=11 *p=11 *q=11


clang-6.0-ASAN exit codes: compile 0 / execute 1

=================================================================
==20333==ERROR: LeakSanitizer: detected memory leaks

Direct leak of 4 byte(s) in 1 object(s) allocated from:
    #0 0x4ba4a3 in __interceptor_malloc /tmp/final/llvm.src/projects/compiler-rt/lib/asan/asan_malloc_linux.cc:88:3
    #1 0x4e71de in main (/auto/homes/vb358/charon2/pointer_offset_from_subtraction_1_malloc.c.clang-6.0-ASAN.out+0x4e71de)

Direct leak of 4 byte(s) in 1 object(s) allocated from:
    #0 0x4ba4a3 in __interceptor_malloc /tmp/final/llvm.src/projects/compiler-rt/lib/asan/asan_malloc_linux.cc:88:3
    #1 0x4e71d1 in main (/auto/homes/vb358/charon2/pointer_offset_from_subtraction_1_malloc.c.clang-6.0-ASAN.out+0x4e71d1)

SUMMARY: AddressSanitizer: 8 byte(s) leaked in 2 allocation(s).


clang-6.0-MSAN Addresses: p=0x701000000010 q=0x701000000010  offset=16 
*xp=1 *yp=11 *p=11 *q=11


icc-19-O0 Addresses: p=0x1968030 q=0x1968030  offset=32 
*xp=1 *yp=11 *p=11 *q=11


icc-19-O2 Addresses: p=0x2254030 q=0x2254030  offset=32 
*xp=1 *yp=11 *p=11 *q=11


icc-19-O3 Addresses: p=0x1da4030 q=0x1da4030  offset=32 
*xp=1 *yp=11 *p=11 *q=11


icc-19-O2-no-strict-aliasing Addresses: p=0xfe3030 q=0xfe3030  offset=32 
*xp=1 *yp=11 *p=11 *q=11


icc-19-O3-no-strict-aliasing Addresses: p=0xca5030 q=0xca5030  offset=32 
*xp=1 *yp=11 *p=11 *q=11


cerberus-concrete BEGIN EXEC[0]
Killed {msg: MerrPtrdiff}
END EXEC[0]
Time spent: 0.056474 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 Addresses: p=0x4003e010 q=0x4003e010  offset=8 
*xp=1 *yp=11 *p=11 *q=11


CHERI:MIPS-O2 Addresses: p=0x4003e010 q=0x4003e010  offset=8 
*xp=1 *yp=11 *p=11 *q=11


CHERI:MIPS-O2-no-strict-aliasing Addresses: p=0x4003e010 q=0x4003e010  offset=8 
*xp=1 *yp=11 *p=11 *q=11


CHERI:CHERI-O0-uintcap-addr-exact-equals Addresses: p=0x7c00006010 q=0x7c00006010  offset=8 


CHERI:CHERI-O2-uintcap-addr-exact-equals Addresses: p=0x7c00006010 q=0x7c00006010  offset=8 


CHERI:CHERI-O2-no-strict-aliasing-uintcap-addr-exact-equals Addresses: p=0x7c00006010 q=0x7c00006010  offset=8 


CHERI:CHERI-O0-uintcap-offset-exact-equals Addresses: p=0x7c00006010 q=0x7c00006010  offset=8 


CHERI:CHERI-O2-uintcap-offset-exact-equals Addresses: p=0x7c00006010 q=0x7c00006010  offset=8 


CHERI:CHERI-O2-no-strict-aliasing-uintcap-offset-exact-equals Addresses: p=0x7c00006010 q=0x7c00006010  offset=8 


CHERI:CHERI-O0-uintcap-addr Addresses: p=0x7c00006010 q=0x7c00006010  offset=8 


CHERI:CHERI-O2-uintcap-addr Addresses: p=0x7c00006010 q=0x7c00006010  offset=8 


CHERI:CHERI-O2-no-strict-aliasing-uintcap-addr Addresses: p=0x7c00006010 q=0x7c00006010  offset=8 


CHERI:CHERI-O0-uintcap-offset Addresses: p=0x7c00006010 q=0x7c00006010  offset=8 


CHERI:CHERI-O2-uintcap-offset Addresses: p=0x7c00006010 q=0x7c00006010  offset=8 


CHERI:CHERI-O2-no-strict-aliasing-uintcap-offset Addresses: p=0x7c00006010 q=0x7c00006010  offset=8 


RV-Match exit codes: compile 0 / execute 1


ch2o In file included from /usr/local/Cellar/gcc/7.3.0_1/lib/gcc/7/gcc/x86_64-apple-darwin17.3.0/7.3.0/include/stdint.h:9:0,
                 from pointer_offset_from_subtraction_1_malloc.c:3:
/usr/local/Cellar/gcc/7.3.0_1/lib/gcc/7/gcc/x86_64-apple-darwin17.3.0/7.3.0/include-fixed/stdint.h:27:10: fatal error: sys/_types/_int8_t.h: No such file or directory
 #include <sys/_types/_int8_t.h>
          ^~~~~~~~~~~~~~~~~~~~~~
compilation terminated.


compcert-3.2 Addresses: p=0x15ed030 q=0x15ed030  offset=32 
*xp=1 *yp=11 *p=11 *q=11


compcert-3.2-O Addresses: p=0x195c030 q=0x195c030  offset=32 
*xp=1 *yp=11 *p=11 *q=11


compcert-3.2-interp Time 0: calling main()
--[step_internal_function]-->
Time 1: in function main, statement
  xp = malloc(sizeof(int));
  yp = malloc(sizeof(int));
  *((int *) xp) = 1;
  *((int *) yp) = 2;
  offset = (unsigned char *) yp - (unsigned char *) xp;
  p1 = (unsigned char *) xp;
  p2 = p1 + offset;
  p = (int *) p2;
  q = (int *) yp;
  printf(__stringlit_1, (void *) p, (void *) q, offset);
  if (memcmp(&p, &q, sizeof(int *)) == 0) {
    *p = 11;
    printf(__stringlit_2, *((int *) .), 
           *((int *) .), *((int *) .), 
           *((int *) .));
  }
  return 0;
  return 0;
--[step_seq]-->
Time 2: in function main, statement
  xp = malloc(sizeof(int));
  yp = malloc(sizeof(int));
  *((int *) xp) = 1;
  *((int *) yp) = 2;
  offset = (unsigned char *) yp - (unsigned char *) xp;
  p1 = (unsigned char *) xp;
  p2 = p1 + offset;
  p = (int *) p2;
  q = (int *) yp;
  printf(__stringlit_1, (void *) p, (void *) q, offset);
  if (memcmp(&p, &q, sizeof(int *)) == 0) {
    *p = 11;
    printf(__stringlit_2, *((int *) .), 
           *((int *) .), *((int *) .), 
           *((int *) .));
  }
  return 0;
--[step_seq]-->
Time 3: in function main, statement xp = malloc(sizeof(int));
--[step_do_1]-->
Time 4: in function main, expression xp = malloc(sizeof(int))
--[red_var_local]-->
Time 5: in function main, expression <loc xp> = malloc(sizeof(int))
--[red_var_global]-->
Time 6: in function main, expression <loc xp> = <loc malloc>(sizeof(int))
--[red_rvalof]-->
Time 7: in function main, expression <loc xp> = <ptr malloc>(sizeof(int))
--[red_sizeof]-->
Time 8: in function main, expression <loc xp> = <ptr malloc>(4U)
--[red_call]-->
Time 9: calling malloc(4)
--[step_external_function]-->
Time 10: returning <ptr>
--[step_returnstate]-->
Time 11: in function main, expression <loc xp> = <ptr>
--[red_assign]-->
Time 12: in function main, expression <ptr>
--[step_do_2]-->
Time 13: in function main, statement /*skip*/;
--[step_skip_seq]-->
Time 14: in function main, statement
  yp = malloc(sizeof(int));
  *((int *) xp) = 1;
  *((int *) yp) = 2;
  offset = (unsigned char *) yp - (unsigned char *) xp;
  p1 = (unsigned char *) xp;
  p2 = p1 + offset;
  p = (int *) p2;
  q = (int *) yp;
  printf(__stringlit_1, (void *) p, (void *) q, offset);
  if (memcmp(&p, &q, sizeof(int *)) == 0) {
    *p = 11;
    printf(__stringlit_2, *((int *) .), 
           *((int *) .), *((int *) .), 
           *((int *) .));
  }
  return 0;
--[step_seq]-->
Time 15: in function main, statement yp = malloc(sizeof(int));
--[step_do_1]-->
Time 16: in function main, expression yp = malloc(sizeof(int))
--[red_var_local]-->
Time 17: in function main, expression <loc yp> = malloc(sizeof(int))
--[red_var_global]-->
Time 18: in function main, expression <loc yp> = <loc malloc>(sizeof(int))
--[red_rvalof]-->
Time 19: in function main, expression <loc yp> = <ptr malloc>(sizeof(int))
--[red_sizeof]-->
Time 20: in function main, expression <loc yp> = <ptr malloc>(4U)
--[red_call]-->
Time 21: calling malloc(4)
--[step_external_function]-->
Time 22: returning <ptr>
--[step_returnstate]-->
Time 23: in function main, expression <loc yp> = <ptr>
--[red_assign]-->
Time 24: in function main, expression <ptr>
--[step_do_2]-->
Time 25: in function main, statement /*skip*/;
--[step_skip_seq]-->
Time 26: in function main, statement
  *((int *) xp) = 1;
  *((int *) yp) = 2;
  offset = (unsigned char *) yp - (unsigned char *) xp;
  p1 = (unsigned char *) xp;
  p2 = p1 + offset;
  p = (int *) p2;
  q = (int *) yp;
  printf(__stringlit_1, (void *) p, (void *) q, offset);
  if (memcmp(&p, &q, sizeof(int *)) == 0) {
    *p = 11;
    printf(__stringlit_2, *((int *) .), 
           *((int *) .), *((int *) .), 
           *((int *) .));
  }
  return 0;
--[step_seq]-->
Time 27: in function main, statement *((int *) xp) = 1;
--[step_do_1]-->
Time 28: in function main, expression *((int *) xp) = 1
--[red_var_local]-->
Time 29: in function main, expression *((int *) <loc xp>) = 1
--[red_rvalof]-->
Time 30: in function main, expression *((int *) <ptr>) = 1
--[red_cast]-->
Time 31: in function main, expression *<ptr> = 1
--[red_deref]-->
Time 32: in function main, expression <loc> = 1
--[red_assign]-->
Time 33: in function main, expression 1
--[step_do_2]-->
Time 34: in function main, statement /*skip*/;
--[step_skip_seq]-->
Time 35: in function main, statement
  *((int *) yp) = 2;
  offset = (unsigned char *) yp - (unsigned char *) xp;
  p1 = (unsigned char *) xp;
  p2 = p1 + offset;
  p = (int *) p2;
  q = (int *) yp;
  printf(__stringlit_1, (void *) p, (void *) q, offset);
  if (memcmp(&p, &q, sizeof(int *)) == 0) {
    *p = 11;
    printf(__stringlit_2, *((int *) .), 
           *((int *) .), *((int *) .), 
           *((int *) .));
  }
  return 0;
--[step_seq]-->
Time 36: in function main, statement *((int *) yp) = 2;
--[step_do_1]-->
Time 37: in function main, expression *((int *) yp) = 2
--[red_var_local]-->
Time 38: in function main, expression *((int *) <loc yp>) = 2
--[red_rvalof]-->
Time 39: in function main, expression *((int *) <ptr>) = 2
--[red_cast]-->
Time 40: in function main, expression *<ptr> = 2
--[red_deref]-->
Time 41: in function main, expression <loc> = 2
--[red_assign]-->
Time 42: in function main, expression 2
--[step_do_2]-->
Time 43: in function main, statement /*skip*/;
--[step_skip_seq]-->
Time 44: in function main, statement
  offset = (unsigned char *) yp - (unsigned char *) xp;
  p1 = (unsigned char *) xp;
  p2 = p1 + offset;
  p = (int *) p2;
  q = (int *) yp;
  printf(__stringlit_1, (void *) p, (void *) q, offset);
  if (memcmp(&p, &q, sizeof(int *)) == 0) {
    *p = 11;
    printf(__stringlit_2, *((int *) .), 
           *((int *) .), *((int *) .), 
           *((int *) .));
  }
  return 0;
--[step_seq]-->
Time 45: in function main, statement
  offset = (unsigned char *) yp - (unsigned char *) xp;
--[step_do_1]-->
Time 46: in function main, expression
  offset = (unsigned char *) yp - (unsigned char *) xp
--[red_var_local]-->
Time 47: in function main, expression
  <loc offset> = (unsigned char *) yp - (unsigned char *) xp
--[red_var_local]-->
Time 48: in function main, expression
  <loc offset> = (unsigned char *) <loc yp> - (unsigned char *) xp
--[red_rvalof]-->
Time 49: in function main, expression
  <loc offset> = (unsigned char *) <ptr> - (unsigned char *) xp
--[red_cast]-->
Time 50: in function main, expression
  <loc offset> = <ptr> - (unsigned char *) xp
--[red_var_local]-->
Time 51: in function main, expression
  <loc offset> = <ptr> - (unsigned char *) <loc xp>
--[red_rvalof]-->
Time 52: in function main, expression
  <loc offset> = <ptr> - (unsigned char *) <ptr>
--[red_cast]-->
Time 53: in function main, expression <loc offset> = <ptr> - <ptr>
Stuck state: in function main, expression <loc offset> = <ptr> - <ptr>
Stuck subexpression: <ptr> - <ptr>
ERROR: Undefined behavior
In file included from pointer_offset_from_subtraction_1_malloc.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.