rely/guarantee for external library functions

.gitignore

@@ -17,6 +17,8 @@ src/main/antlr4/.antlr
 *.dot
 *.il
 *.txt
+*.o
+*.so
 examplesold/
 src/test/scala/dump/
 src/test/analysis/dump/

examples/secret_write_librg/secret.c

@@ -0,0 +1,4 @@
+
+void secret(int* x) {
+  *x = -1;
+}

examples/secret_write_librg/secret_write_librg.bir

@@ -0,0 +1,267 @@
+00000661: program
+0000064a: sub __cxa_finalize(__cxa_finalize_result)
+00000662: __cxa_finalize_result :: out u32 = low:32[R0]
+
+00000414:
+0000051c: R16 := 0x10000
+00000523: R17 := mem[R16 + 0xFB0, el]:u64
+00000529: R16 := R16 + 0xFB0
+0000052e: call R17 with noreturn
+
+0000064b: sub __do_global_dtors_aux(__do_global_dtors_aux_result)
+00000663: __do_global_dtors_aux_result :: out u32 = low:32[R0]
+
+000002be:
+000002c2: #3 := R31 - 0x20
+000002c8: mem := mem with [#3, el]:u64 <- R29
+000002ce: mem := mem with [#3 + 8, el]:u64 <- R30
+000002d2: R31 := #3
+000002d8: R29 := R31
+000002e0: mem := mem with [R31 + 0x10, el]:u64 <- R19
+000002e5: R19 := 0x11000
+000002ec: R0 := pad:64[mem[R19 + 0x10]]
+000002f3: when 31:0[R0] <> 0 goto %000002f1
+0000064c: goto %000003dd
+
+000003dd:
+000003e0: R0 := 0x10000
+000003e7: R0 := mem[R0 + 0xFE0, el]:u64
+000003ed: when R0 = 0 goto %000003eb
+0000064d: goto %00000404
+
+00000404:
+00000407: R0 := 0x11000
+0000040e: R0 := mem[R0 + 8, el]:u64
+00000413: R30 := 0x770
+00000416: call @__cxa_finalize with return %000003eb
+
+000003eb:
+000003f3: R30 := 0x774
+000003f5: call @deregister_tm_clones with return %000003f7
+
+000003f7:
+000003fa: R0 := 1
+00000402: mem := mem with [R19 + 0x10] <- 7:0[R0]
+0000064e: goto %000002f1
+
+000002f1:
+000002fb: R19 := mem[R31 + 0x10, el]:u64
+00000302: R29 := mem[R31, el]:u64
+00000307: R30 := mem[R31 + 8, el]:u64
+0000030b: R31 := R31 + 0x20
+00000310: call R30 with noreturn
+
+0000064f: sub __libc_start_main(__libc_start_main_main, __libc_start_main_arg2, __libc_start_main_arg3, __libc_start_main_auxv, __libc_start_main_result)
+00000664: __libc_start_main_main :: in u64 = R0
+00000665: __libc_start_main_arg2 :: in u32 = low:32[R1]
+00000666: __libc_start_main_arg3 :: in out u64 = R2
+00000667: __libc_start_main_auxv :: in out u64 = R3
+00000668: __libc_start_main_result :: out u32 = low:32[R0]
+
+00000217:
+00000506: R16 := 0x10000
+0000050d: R17 := mem[R16 + 0xFA8, el]:u64
+00000513: R16 := R16 + 0xFA8
+00000518: call R17 with noreturn
+
+00000650: sub _fini(_fini_result)
+00000669: _fini_result :: out u32 = low:32[R0]
+
+0000001f:
+00000025: #0 := R31 - 0x10
+0000002b: mem := mem with [#0, el]:u64 <- R29
+00000031: mem := mem with [#0 + 8, el]:u64 <- R30
+00000035: R31 := #0
+0000003b: R29 := R31
+00000042: R29 := mem[R31, el]:u64
+00000047: R30 := mem[R31 + 8, el]:u64
+0000004b: R31 := R31 + 0x10
+00000050: call R30 with noreturn
+
+00000651: sub _init(_init_result)
+0000066a: _init_result :: out u32 = low:32[R0]
+
+0000058c:
+00000592: #6 := R31 - 0x10
+00000598: mem := mem with [#6, el]:u64 <- R29
+0000059e: mem := mem with [#6 + 8, el]:u64 <- R30
+000005a2: R31 := #6
+000005a8: R29 := R31
+000005ad: R30 := 0x5D8
+000005af: call @call_weak_fn with return %000005b1
+
+000005b1:
+000005b6: R29 := mem[R31, el]:u64
+000005bb: R30 := mem[R31 + 8, el]:u64
+000005bf: R31 := R31 + 0x10
+000005c4: call R30 with noreturn
+
+00000652: sub _start(_start_result)
+0000066b: _start_result :: out u32 = low:32[R0]
+
+000001d8:
+000001dd: R29 := 0
+000001e2: R30 := 0
+000001e8: R5 := R0
+000001ef: R1 := mem[R31, el]:u64
+000001f5: R2 := R31 + 8
+000001fb: R6 := R31
+00000200: R0 := 0x10000
+00000207: R0 := mem[R0 + 0xFF0, el]:u64
+0000020c: R3 := 0
+00000211: R4 := 0
+00000216: R30 := 0x6B0
+00000219: call @__libc_start_main with return %0000021b
+
+0000021b:
+0000021e: R30 := 0x6B4
+00000221: call @abort with return %00000653
+
+00000653:
+00000654: call @call_weak_fn with noreturn
+
+00000655: sub abort()
+
+
+0000021f:
+00000548: R16 := 0x10000
+0000054f: R17 := mem[R16 + 0xFC0, el]:u64
+00000555: R16 := R16 + 0xFC0
+0000055a: call R17 with noreturn
+
+00000656: sub call_weak_fn(call_weak_fn_result)
+0000066c: call_weak_fn_result :: out u32 = low:32[R0]
+
+00000223:
+00000226: R0 := 0x10000
+0000022d: R0 := mem[R0 + 0xFE8, el]:u64
+00000233: when R0 = 0 goto %00000231
+00000657: goto %00000454
+
+00000231:
+00000239: call R30 with noreturn
+
+00000454:
+00000457: goto @__gmon_start__
+
+00000455:
+00000532: R16 := 0x10000
+00000539: R17 := mem[R16 + 0xFB8, el]:u64
+0000053f: R16 := R16 + 0xFB8
+00000544: call R17 with noreturn
+
+00000658: sub deregister_tm_clones(deregister_tm_clones_result)
+0000066d: deregister_tm_clones_result :: out u32 = low:32[R0]
+
+0000023f:
+00000242: R0 := 0x11000
+00000248: R0 := R0 + 0x10
+0000024d: R1 := 0x11000
+00000253: R1 := R1 + 0x10
+00000259: #1 := ~R0
+0000025e: #2 := R1 + ~R0
+00000264: VF := extend:65[#2 + 1] <> extend:65[R1] + extend:65[#1] + 1
+0000026a: CF := pad:65[#2 + 1] <> pad:65[R1] + pad:65[#1] + 1
+0000026e: ZF := #2 + 1 = 0
+00000272: NF := 63:63[#2 + 1]
+00000278: when ZF goto %00000276
+00000659: goto %00000436
+
+00000436:
+00000439: R1 := 0x10000
+00000440: R1 := mem[R1 + 0xFD8, el]:u64
+00000445: when R1 = 0 goto %00000276
+0000065a: goto %00000449
+
+00000276:
+0000027e: call R30 with noreturn
+
+00000449:
+0000044d: R16 := R1
+00000452: call R16 with noreturn
+
+0000065b: sub frame_dummy(frame_dummy_result)
+0000066e: frame_dummy_result :: out u32 = low:32[R0]
+
+00000316:
+00000318: call @register_tm_clones with noreturn
+
+0000065c: sub main(main_argc, main_argv, main_result)
+0000066f: main_argc :: in u32 = low:32[R0]
+00000670: main_argv :: in out u64 = R1
+00000671: main_result :: out u32 = low:32[R0]
+
+0000031a:
+0000031e: #4 := R31 - 0x10
+00000324: mem := mem with [#4, el]:u64 <- R29
+0000032a: mem := mem with [#4 + 8, el]:u64 <- R30
+0000032e: R31 := #4
+00000334: R29 := R31
+00000339: R0 := 0x11000
+0000033f: R0 := R0 + 0x14
+00000346: mem := mem with [R0, el]:u32 <- 0
+0000034b: R0 := 0x11000
+00000351: R0 := R0 + 0x14
+00000358: R0 := pad:64[mem[R0, el]:u32]
+0000035e: R1 := pad:64[31:0[R0] + 1]
+00000363: R0 := 0x11000
+00000369: R0 := R0 + 0x14
+00000371: mem := mem with [R0, el]:u32 <- 31:0[R1]
+00000376: R0 := 0x11000
+0000037c: R0 := R0 + 0x18
+00000381: R30 := 0x7D0
+00000384: call @secret with return %00000386
+
+00000386:
+00000389: R0 := 0x11000
+0000038f: R0 := R0 + 0x18
+00000396: mem := mem with [R0, el]:u32 <- 0
+0000039b: R0 := 0x11000
+000003a1: R0 := R0 + 0x14
+000003a8: R0 := pad:64[mem[R0, el]:u32]
+000003ae: R1 := pad:64[31:0[R0] + 1]
+000003b3: R0 := 0x11000
+000003b9: R0 := R0 + 0x14
+000003c1: mem := mem with [R0, el]:u32 <- 31:0[R1]
+000003c6: R0 := 0
+000003cd: R29 := mem[R31, el]:u64
+000003d2: R30 := mem[R31 + 8, el]:u64
+000003d6: R31 := R31 + 0x10
+000003db: call R30 with noreturn
+
+0000065d: sub register_tm_clones(register_tm_clones_result)
+00000672: register_tm_clones_result :: out u32 = low:32[R0]
+
+00000280:
+00000283: R0 := 0x11000
+00000289: R0 := R0 + 0x10
+0000028e: R1 := 0x11000
+00000294: R1 := R1 + 0x10
+0000029b: R1 := R1 + ~R0 + 1
+000002a1: R2 := 0.63:63[R1]
+000002a8: R1 := R2 + (R1 ~>> 3)
+000002ae: R1 := extend:64[63:1[R1]]
+000002b4: when R1 = 0 goto %000002b2
+0000065e: goto %00000418
+
+00000418:
+0000041b: R2 := 0x10000
+00000422: R2 := mem[R2 + 0xFF8, el]:u64
+00000427: when R2 = 0 goto %000002b2
+0000065f: goto %0000042b
+
+000002b2:
+000002ba: call R30 with noreturn
+
+0000042b:
+0000042f: R16 := R2
+00000434: call R16 with noreturn
+
+00000660: sub secret(secret_result)
+00000673: secret_result :: out u32 = low:32[R0]
+
+00000382:
+0000055e: R16 := 0x10000
+00000565: R17 := mem[R16 + 0xFC8, el]:u64
+0000056b: R16 := R16 + 0xFC8
+00000570: call R17 with noreturn

examples/secret_write_librg/secret_write_librg.c

@@ -0,0 +1,12 @@
+void secret(int* y);
+
+int z;
+int x;
+
+int main(void) {
+  z = 0;
+  z = z + 1;
+  secret(&x);
+  x = 0;
+  z = z + 1;
+}