Skip to content

Commit

Permalink
Modify tests to fail without analysis
Browse files Browse the repository at this point in the history
  • Loading branch information
@b-paul
b-paul committed Jul 17, 2024
1 parent 16618e1 commit b105491
Show file tree
Hide file tree
Showing 33 changed files with 687 additions and 4,513 deletions.
2 changes: 1 addition & 1 deletion src/test/correct-analysis/function_summary/function_summary.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,6 @@ int main() {
y = get_two();
}

int get_two() {
__attribute((noinline)) int get_two() {
return 2;
}
2 changes: 2 additions & 0 deletions src/test/correct-analysis/function_summary/function_summary.spec
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,8 @@ Globals:
x: int
y: int

L: y -> true

Subroutine: main
Requires: Gamma_x == true
Requires: Gamma_y == true
Expand Down
60 changes: 30 additions & 30 deletions src/test/correct-analysis/function_summary/gcc/function_summary.adt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -67,10 +67,10 @@ Annotation(Region(0x1FFB8,0x1FFE7), Attr("section","\".got\"")),
Annotation(Region(0x1FFE8,0x2001F), Attr("section","\".got.plt\"")),
Annotation(Region(0x20020,0x2002F), Attr("section","\".data\"")),
Annotation(Region(0x1FDC8,0x1FDCF), Attr("section","\".init_array\""))]),
Program(Tid(1_580, "%0000062c"), Attrs([]),
Program(Tid(1_609, "%00000649"), Attrs([]),
Subs([Sub(Tid(1_557, "@__cxa_finalize"),
Attrs([Attr("c.proto","signed (*)(void)"), Attr("address","0x5D0"),
Attr("stub","()")]), "__cxa_finalize", Args([Arg(Tid(1_581, "%0000062d"),
Attr("stub","()")]), "__cxa_finalize", Args([Arg(Tid(1_610, "%0000064a"),
Attrs([Attr("c.layout","[signed : 32]"), Attr("c.data","Top:u32"),
Attr("c.type","signed")]), Var("__cxa_finalize_result",Imm(32)),
LOW(32,Var("R0",Imm(64))), Out())]), Blks([Blk(Tid(945, "@__cxa_finalize"),
Expand All @@ -87,7 +87,7 @@ PLUS(Var("R16",Imm(64)),Int(8,64)))]), Jmps([Call(Tid(1_211, "%000004bb"),
(Indirect(Var("R17",Imm(64))),))]))])),
Sub(Tid(1_558, "@__do_global_dtors_aux"),
Attrs([Attr("c.proto","signed (*)(void)"), Attr("address","0x6CC")]),
"__do_global_dtors_aux", Args([Arg(Tid(1_582, "%0000062e"),
"__do_global_dtors_aux", Args([Arg(Tid(1_611, "%0000064b"),
Attrs([Attr("c.layout","[signed : 32]"), Attr("c.data","Top:u32"),
Attr("c.type","signed")]), Var("__do_global_dtors_aux_result",Imm(32)),
LOW(32,Var("R0",Imm(64))), Out())]),
Expand Down Expand Up @@ -118,7 +118,7 @@ UNSIGNED(64,Load(Var("mem",Mem(64,8)),PLUS(Var("R19",Imm(64)),Int(48,64)),Little
Jmps([Goto(Tid(729, "%000002d9"), Attrs([Attr("address","0x6E0"),
Attr("insn","tbnz w0, #0x0, #0x28")]),
EQ(Extract(0,0,Var("R0",Imm(64))),Int(1,1)), Direct(Tid(727, "%000002d7"))),
Goto(Tid(1_559, "%00000617"), Attrs([]), Int(1,1),
Goto(Tid(1_599, "%0000063f"), Attrs([]), Int(1,1),
Direct(Tid(890, "%0000037a")))])), Blk(Tid(890, "%0000037a"),
Attrs([Attr("address","0x6E4")]), Phis([]), Defs([Def(Tid(893, "%0000037d"),
Attrs([Attr("address","0x6E4"), Attr("insn","adrp x0, #126976")]),
Expand All @@ -128,7 +128,7 @@ Direct(Tid(890, "%0000037a")))])), Blk(Tid(890, "%0000037a"),
Load(Var("mem",Mem(64,8)),PLUS(Var("R0",Imm(64)),Int(4040,64)),LittleEndian(),64))]),
Jmps([Goto(Tid(906, "%0000038a"), Attrs([Attr("address","0x6EC"),
Attr("insn","cbz x0, #0x10")]), EQ(Var("R0",Imm(64)),Int(0,64)),
Direct(Tid(904, "%00000388"))), Goto(Tid(1_560, "%00000618"), Attrs([]),
Direct(Tid(904, "%00000388"))), Goto(Tid(1_600, "%00000640"), Attrs([]),
Int(1,1), Direct(Tid(929, "%000003a1")))])), Blk(Tid(929, "%000003a1"),
Attrs([Attr("address","0x6F0")]), Phis([]), Defs([Def(Tid(932, "%000003a4"),
Attrs([Attr("address","0x6F0"), Attr("insn","adrp x0, #131072")]),
Expand All @@ -153,7 +153,7 @@ Attr("insn","mov w0, #0x1")]), Var("R0",Imm(64)), Int(1,64)),
Def(Tid(927, "%0000039f"), Attrs([Attr("address","0x704"),
Attr("insn","strb w0, [x19, #0x30]")]), Var("mem",Mem(64,8)),
Store(Var("mem",Mem(64,8)),PLUS(Var("R19",Imm(64)),Int(48,64)),Extract(7,0,Var("R0",Imm(64))),LittleEndian(),8))]),
Jmps([Goto(Tid(1_561, "%00000619"), Attrs([]), Int(1,1),
Jmps([Goto(Tid(1_601, "%00000641"), Attrs([]), Int(1,1),
Direct(Tid(727, "%000002d7")))])), Blk(Tid(727, "%000002d7"),
Attrs([Attr("address","0x708")]), Phis([]), Defs([Def(Tid(737, "%000002e1"),
Attrs([Attr("address","0x708"), Attr("insn","ldr x19, [sp, #0x10]")]),
Expand All @@ -172,21 +172,21 @@ PLUS(Var("R31",Imm(64)),Int(32,64)))]), Jmps([Call(Tid(758, "%000002f6"),
(Indirect(Var("R30",Imm(64))),))]))])), Sub(Tid(1_562, "@__libc_start_main"),
Attrs([Attr("c.proto","signed (*)(signed (*)(signed , char** , char** );* main, signed , char** , \nvoid* auxv)"),
Attr("address","0x5C0"), Attr("stub","()")]), "__libc_start_main",
Args([Arg(Tid(1_583, "%0000062f"),
Args([Arg(Tid(1_612, "%0000064c"),
Attrs([Attr("c.layout","**[<undef> : 64]"),
Attr("c.data","Top:u64 ptr ptr"),
Attr("c.type","signed (*)(signed , char** , char** );*")]),
Var("__libc_start_main_main",Imm(64)), Var("R0",Imm(64)), In()),
Arg(Tid(1_584, "%00000630"), Attrs([Attr("c.layout","[signed : 32]"),
Arg(Tid(1_613, "%0000064d"), Attrs([Attr("c.layout","[signed : 32]"),
Attr("c.data","Top:u32"), Attr("c.type","signed")]),
Var("__libc_start_main_arg2",Imm(32)), LOW(32,Var("R1",Imm(64))), In()),
Arg(Tid(1_585, "%00000631"), Attrs([Attr("c.layout","**[char : 8]"),
Arg(Tid(1_614, "%0000064e"), Attrs([Attr("c.layout","**[char : 8]"),
Attr("c.data","Top:u8 ptr ptr"), Attr("c.type","char**")]),
Var("__libc_start_main_arg3",Imm(64)), Var("R2",Imm(64)), Both()),
Arg(Tid(1_586, "%00000632"), Attrs([Attr("c.layout","*[<undef> : 8]"),
Arg(Tid(1_615, "%0000064f"), Attrs([Attr("c.layout","*[<undef> : 8]"),
Attr("c.data","{} ptr"), Attr("c.type","void*")]),
Var("__libc_start_main_auxv",Imm(64)), Var("R3",Imm(64)), Both()),
Arg(Tid(1_587, "%00000633"), Attrs([Attr("c.layout","[signed : 32]"),
Arg(Tid(1_616, "%00000650"), Attrs([Attr("c.layout","[signed : 32]"),
Attr("c.data","Top:u32"), Attr("c.type","signed")]),
Var("__libc_start_main_result",Imm(32)), LOW(32,Var("R0",Imm(64))),
Out())]), Blks([Blk(Tid(504, "@__libc_start_main"),
Expand All @@ -202,7 +202,7 @@ Var("R16",Imm(64)))]), Jmps([Call(Tid(1_189, "%000004a5"),
Attrs([Attr("address","0x5CC"), Attr("insn","br x17")]), Int(1,1),
(Indirect(Var("R17",Imm(64))),))]))])), Sub(Tid(1_563, "@_fini"),
Attrs([Attr("c.proto","signed (*)(void)"), Attr("address","0x764")]),
"_fini", Args([Arg(Tid(1_588, "%00000634"),
"_fini", Args([Arg(Tid(1_617, "%00000651"),
Attrs([Attr("c.layout","[signed : 32]"), Attr("c.data","Top:u32"),
Attr("c.type","signed")]), Var("_fini_result",Imm(32)),
LOW(32,Var("R0",Imm(64))), Out())]), Blks([Blk(Tid(32, "@_fini"),
Expand Down Expand Up @@ -232,7 +232,7 @@ PLUS(Var("R31",Imm(64)),Int(16,64)))]), Jmps([Call(Tid(81, "%00000051"),
Attrs([Attr("address","0x774"), Attr("insn","ret")]), Int(1,1),
(Indirect(Var("R30",Imm(64))),))]))])), Sub(Tid(1_564, "@_init"),
Attrs([Attr("c.proto","signed (*)(void)"), Attr("address","0x580")]),
"_init", Args([Arg(Tid(1_589, "%00000635"),
"_init", Args([Arg(Tid(1_618, "%00000652"),
Attrs([Attr("c.layout","[signed : 32]"), Attr("c.data","Top:u32"),
Attr("c.type","signed")]), Var("_init_result",Imm(32)),
LOW(32,Var("R0",Imm(64))), Out())]), Blks([Blk(Tid(1_379, "@_init"),
Expand Down Expand Up @@ -269,7 +269,7 @@ PLUS(Var("R31",Imm(64)),Int(16,64)))]), Jmps([Call(Tid(1_435, "%0000059b"),
(Indirect(Var("R30",Imm(64))),))]))])), Sub(Tid(1_565, "@_start"),
Attrs([Attr("c.proto","signed (*)(void)"), Attr("address","0x600"),
Attr("stub","()"), Attr("entry-point","()")]), "_start",
Args([Arg(Tid(1_590, "%00000636"), Attrs([Attr("c.layout","[signed : 32]"),
Args([Arg(Tid(1_619, "%00000653"), Attrs([Attr("c.layout","[signed : 32]"),
Attr("c.data","Top:u32"), Attr("c.type","signed")]),
Var("_start_result",Imm(32)), LOW(32,Var("R0",Imm(64))), Out())]),
Blks([Blk(Tid(441, "@_start"), Attrs([Attr("address","0x600")]), Phis([]),
Expand Down Expand Up @@ -306,9 +306,9 @@ Defs([Def(Tid(511, "%000001ff"), Attrs([Attr("address","0x630"),
Attr("insn","bl #-0x40")]), Var("R30",Imm(64)), Int(1588,64))]),
Jmps([Call(Tid(514, "%00000202"), Attrs([Attr("address","0x630"),
Attr("insn","bl #-0x40")]), Int(1,1),
(Direct(Tid(1_568, "@abort")),Direct(Tid(1_566, "%0000061e"))))])),
Blk(Tid(1_566, "%0000061e"), Attrs([]), Phis([]), Defs([]),
Jmps([Call(Tid(1_567, "%0000061f"), Attrs([]), Int(1,1),
(Direct(Tid(1_568, "@abort")),Direct(Tid(1_602, "%00000642"))))])),
Blk(Tid(1_602, "%00000642"), Attrs([]), Phis([]), Defs([]),
Jmps([Call(Tid(1_603, "%00000643"), Attrs([]), Int(1,1),
(Direct(Tid(1_569, "@call_weak_fn")),))]))])), Sub(Tid(1_568, "@abort"),
Attrs([Attr("noreturn","()"), Attr("c.proto","void (*)(void)"),
Attr("address","0x5F0"), Attr("stub","()")]), "abort", Args([]),
Expand All @@ -324,7 +324,7 @@ PLUS(Var("R16",Imm(64)),Int(24,64)))]), Jmps([Call(Tid(1_255, "%000004e7"),
Attrs([Attr("address","0x5FC"), Attr("insn","br x17")]), Int(1,1),
(Indirect(Var("R17",Imm(64))),))]))])), Sub(Tid(1_569, "@call_weak_fn"),
Attrs([Attr("c.proto","signed (*)(void)"), Attr("address","0x634")]),
"call_weak_fn", Args([Arg(Tid(1_591, "%00000637"),
"call_weak_fn", Args([Arg(Tid(1_620, "%00000654"),
Attrs([Attr("c.layout","[signed : 32]"), Attr("c.data","Top:u32"),
Attr("c.type","signed")]), Var("call_weak_fn_result",Imm(32)),
LOW(32,Var("R0",Imm(64))), Out())]), Blks([Blk(Tid(516, "@call_weak_fn"),
Expand All @@ -336,7 +336,7 @@ LOW(32,Var("R0",Imm(64))), Out())]), Blks([Blk(Tid(516, "@call_weak_fn"),
Load(Var("mem",Mem(64,8)),PLUS(Var("R0",Imm(64)),Int(4048,64)),LittleEndian(),64))]),
Jmps([Goto(Tid(532, "%00000214"), Attrs([Attr("address","0x63C"),
Attr("insn","cbz x0, #0x8")]), EQ(Var("R0",Imm(64)),Int(0,64)),
Direct(Tid(530, "%00000212"))), Goto(Tid(1_570, "%00000622"), Attrs([]),
Direct(Tid(530, "%00000212"))), Goto(Tid(1_604, "%00000644"), Attrs([]),
Int(1,1), Direct(Tid(1_009, "%000003f1")))])), Blk(Tid(530, "%00000212"),
Attrs([Attr("address","0x644")]), Phis([]), Defs([]),
Jmps([Call(Tid(538, "%0000021a"), Attrs([Attr("address","0x644"),
Expand All @@ -358,7 +358,7 @@ PLUS(Var("R16",Imm(64)),Int(16,64)))]), Jmps([Call(Tid(1_233, "%000004d1"),
(Indirect(Var("R17",Imm(64))),))]))])),
Sub(Tid(1_571, "@deregister_tm_clones"),
Attrs([Attr("c.proto","signed (*)(void)"), Attr("address","0x660")]),
"deregister_tm_clones", Args([Arg(Tid(1_592, "%00000638"),
"deregister_tm_clones", Args([Arg(Tid(1_621, "%00000655"),
Attrs([Attr("c.layout","[signed : 32]"), Attr("c.data","Top:u32"),
Attr("c.type","signed")]), Var("deregister_tm_clones_result",Imm(32)),
LOW(32,Var("R0",Imm(64))), Out())]),
Expand Down Expand Up @@ -390,7 +390,7 @@ EQ(PLUS(Var("#2",Imm(64)),Int(1,64)),Int(0,64))), Def(Tid(603, "%0000025b"),
Var("NF",Imm(1)), Extract(63,63,PLUS(Var("#2",Imm(64)),Int(1,64))))]),
Jmps([Goto(Tid(609, "%00000261"), Attrs([Attr("address","0x674"),
Attr("insn","b.eq #0x18")]), EQ(Var("ZF",Imm(1)),Int(1,1)),
Direct(Tid(607, "%0000025f"))), Goto(Tid(1_572, "%00000624"), Attrs([]),
Direct(Tid(607, "%0000025f"))), Goto(Tid(1_605, "%00000645"), Attrs([]),
Int(1,1), Direct(Tid(979, "%000003d3")))])), Blk(Tid(979, "%000003d3"),
Attrs([Attr("address","0x678")]), Phis([]), Defs([Def(Tid(982, "%000003d6"),
Attrs([Attr("address","0x678"), Attr("insn","adrp x1, #126976")]),
Expand All @@ -400,7 +400,7 @@ Direct(Tid(607, "%0000025f"))), Goto(Tid(1_572, "%00000624"), Attrs([]),
Load(Var("mem",Mem(64,8)),PLUS(Var("R1",Imm(64)),Int(4032,64)),LittleEndian(),64))]),
Jmps([Goto(Tid(994, "%000003e2"), Attrs([Attr("address","0x680"),
Attr("insn","cbz x1, #0xc")]), EQ(Var("R1",Imm(64)),Int(0,64)),
Direct(Tid(607, "%0000025f"))), Goto(Tid(1_573, "%00000625"), Attrs([]),
Direct(Tid(607, "%0000025f"))), Goto(Tid(1_606, "%00000646"), Attrs([]),
Int(1,1), Direct(Tid(998, "%000003e6")))])), Blk(Tid(607, "%0000025f"),
Attrs([Attr("address","0x68C")]), Phis([]), Defs([]),
Jmps([Call(Tid(615, "%00000267"), Attrs([Attr("address","0x68C"),
Expand All @@ -411,7 +411,7 @@ Attr("insn","mov x16, x1")]), Var("R16",Imm(64)), Var("R1",Imm(64)))]),
Jmps([Call(Tid(1_007, "%000003ef"), Attrs([Attr("address","0x688"),
Attr("insn","br x16")]), Int(1,1), (Indirect(Var("R16",Imm(64))),))]))])),
Sub(Tid(1_574, "@frame_dummy"), Attrs([Attr("c.proto","signed (*)(void)"),
Attr("address","0x720")]), "frame_dummy", Args([Arg(Tid(1_593, "%00000639"),
Attr("address","0x720")]), "frame_dummy", Args([Arg(Tid(1_622, "%00000656"),
Attrs([Attr("c.layout","[signed : 32]"), Attr("c.data","Top:u32"),
Attr("c.type","signed")]), Var("frame_dummy_result",Imm(32)),
LOW(32,Var("R0",Imm(64))), Out())]), Blks([Blk(Tid(766, "@frame_dummy"),
Expand All @@ -420,7 +420,7 @@ Jmps([Call(Tid(768, "%00000300"), Attrs([Attr("address","0x720"),
Attr("insn","b #-0x90")]), Int(1,1),
(Direct(Tid(1_577, "@register_tm_clones")),))]))])),
Sub(Tid(1_575, "@get_two"), Attrs([Attr("c.proto","signed (*)(void)"),
Attr("address","0x75C")]), "get_two", Args([Arg(Tid(1_594, "%0000063a"),
Attr("address","0x75C")]), "get_two", Args([Arg(Tid(1_623, "%00000657"),
Attrs([Attr("c.layout","[signed : 32]"), Attr("c.data","Top:u32"),
Attr("c.type","signed")]), Var("get_two_result",Imm(32)),
LOW(32,Var("R0",Imm(64))), Out())]), Blks([Blk(Tid(826, "@get_two"),
Expand All @@ -430,13 +430,13 @@ LOW(32,Var("R0",Imm(64))), Out())]), Blks([Blk(Tid(826, "@get_two"),
Attrs([Attr("address","0x760"), Attr("insn","ret")]), Int(1,1),
(Indirect(Var("R30",Imm(64))),))]))])), Sub(Tid(1_576, "@main"),
Attrs([Attr("c.proto","signed (*)(signed argc, const char** argv)"),
Attr("address","0x724")]), "main", Args([Arg(Tid(1_595, "%0000063b"),
Attr("address","0x724")]), "main", Args([Arg(Tid(1_624, "%00000658"),
Attrs([Attr("c.layout","[signed : 32]"), Attr("c.data","Top:u32"),
Attr("c.type","signed")]), Var("main_argc",Imm(32)),
LOW(32,Var("R0",Imm(64))), In()), Arg(Tid(1_596, "%0000063c"),
LOW(32,Var("R0",Imm(64))), In()), Arg(Tid(1_625, "%00000659"),
Attrs([Attr("c.layout","**[char : 8]"), Attr("c.data","Top:u8 ptr ptr"),
Attr("c.type"," const char**")]), Var("main_argv",Imm(64)),
Var("R1",Imm(64)), Both()), Arg(Tid(1_597, "%0000063d"),
Var("R1",Imm(64)), Both()), Arg(Tid(1_626, "%0000065a"),
Attrs([Attr("c.layout","[signed : 32]"), Attr("c.data","Top:u32"),
Attr("c.type","signed")]), Var("main_result",Imm(32)),
LOW(32,Var("R0",Imm(64))), Out())]), Blks([Blk(Tid(770, "@main"),
Expand Down Expand Up @@ -495,7 +495,7 @@ PLUS(Var("R31",Imm(64)),Int(16,64)))]), Jmps([Call(Tid(888, "%00000378"),
(Indirect(Var("R30",Imm(64))),))]))])),
Sub(Tid(1_577, "@register_tm_clones"),
Attrs([Attr("c.proto","signed (*)(void)"), Attr("address","0x690")]),
"register_tm_clones", Args([Arg(Tid(1_598, "%0000063e"),
"register_tm_clones", Args([Arg(Tid(1_627, "%0000065b"),
Attrs([Attr("c.layout","[signed : 32]"), Attr("c.data","Top:u32"),
Attr("c.type","signed")]), Var("register_tm_clones_result",Imm(32)),
LOW(32,Var("R0",Imm(64))), Out())]),
Expand Down Expand Up @@ -523,7 +523,7 @@ Attr("insn","asr x1, x1, #1")]), Var("R1",Imm(64)),
SIGNED(64,Extract(63,1,Var("R1",Imm(64)))))]),
Jmps([Goto(Tid(669, "%0000029d"), Attrs([Attr("address","0x6B0"),
Attr("insn","cbz x1, #0x18")]), EQ(Var("R1",Imm(64)),Int(0,64)),
Direct(Tid(667, "%0000029b"))), Goto(Tid(1_578, "%0000062a"), Attrs([]),
Direct(Tid(667, "%0000029b"))), Goto(Tid(1_607, "%00000647"), Attrs([]),
Int(1,1), Direct(Tid(949, "%000003b5")))])), Blk(Tid(949, "%000003b5"),
Attrs([Attr("address","0x6B4")]), Phis([]), Defs([Def(Tid(952, "%000003b8"),
Attrs([Attr("address","0x6B4"), Attr("insn","adrp x2, #126976")]),
Expand All @@ -533,7 +533,7 @@ Direct(Tid(667, "%0000029b"))), Goto(Tid(1_578, "%0000062a"), Attrs([]),
Load(Var("mem",Mem(64,8)),PLUS(Var("R2",Imm(64)),Int(4064,64)),LittleEndian(),64))]),
Jmps([Goto(Tid(964, "%000003c4"), Attrs([Attr("address","0x6BC"),
Attr("insn","cbz x2, #0xc")]), EQ(Var("R2",Imm(64)),Int(0,64)),
Direct(Tid(667, "%0000029b"))), Goto(Tid(1_579, "%0000062b"), Attrs([]),
Direct(Tid(667, "%0000029b"))), Goto(Tid(1_608, "%00000648"), Attrs([]),
Int(1,1), Direct(Tid(968, "%000003c8")))])), Blk(Tid(667, "%0000029b"),
Attrs([Attr("address","0x6C8")]), Phis([]), Defs([]),
Jmps([Call(Tid(675, "%000002a3"), Attrs([Attr("address","0x6C8"),
Expand Down
Loading

0 comments on commit b105491

Please sign in to comment.