diff --git a/examples/memory/malloc_free.il b/examples/memory/malloc_free.il new file mode 100644 index 00000000..fe65ed38 --- /dev/null +++ b/examples/memory/malloc_free.il @@ -0,0 +1,332 @@ +memory shared $mem : (bv64 -> bv8); +memory $stack : (bv64 -> bv8); +var $R0: bv64; +var $R1: bv64; +var $R16: bv64; +var $R17: bv64; +var $R29: bv64; +var $R30: bv64; +var $R31: bv64; + +let $magic (a:(bv64->bv8)), (b:(bv64->bv8)) : (bv64->bv8) = (a); + +prog entry @main; + +proc @main () -> () + { .name = "main"; .address = 0x8e4; .returnBlock = "main_basil_return_1" } +[ + block %main_entry {.address = 0x8e4; .originalLabel = "ZLfuz7OtTNOS9GLtqSI1gg=="} [ + var Cse0__5_23: bv64 := bvadd($R31:bv64, 0xffffffffffffffe0:bv64) { .label = "2276_0" }; + store le $stack Cse0__5_23:bv64 $R29:bv64 64 { .label = "2276_1" }; + store le $stack bvadd(Cse0__5_23:bv64, 0x8:bv64) $R30:bv64 64 { .label = "2276_2" }; + $R31: bv64 := Cse0__5_23:bv64 { .label = "2276_3" }; + $R29: bv64 := $R31:bv64 { .label = "2280_0" }; + $R0: bv64 := 0x11:bv64 { .label = "2284_0" }; + $R30: bv64 := 0x8f4:bv64 { .label = "2288_0" }; + goto(%FUN_770_entry_9); + ]; + block %main_3 {.address = 0x910; .originalLabel = "32fWxY7+R++JNJOFTmT+Sg=="} [ + $R0: bv64 := 0x0:bv64 { .label = "2320_0" }; + var Exp16__5_24: bv64 := load le $stack $R31:bv64 64 { .label = "2324_0$0" }; + var Exp18__5_25: bv64 := load le $stack bvadd($R31:bv64, 0x8:bv64) 64 { .label = "2324_1$0" }; + $R29: bv64 := Exp16__5_24:bv64 { .label = "2324_2" }; + $R30: bv64 := Exp18__5_25:bv64 { .label = "2324_3" }; + $R31: bv64 := bvadd($R31:bv64, 0x20:bv64) { .label = "2324_4" }; + goto(%main_basil_return_1); + ]; + block %main_5 {.address = 0x8f4; .originalLabel = "HVqN0/3+RWiLPKsHRvUqeg=="} [ + store le $stack bvadd($R31:bv64, 0x18:bv64) $R0:bv64 64 { .label = "2292_0" }; + var Exp14__5_21: bv64 := load le $stack bvadd($R31:bv64, 0x18:bv64) 64 { .label = "2296_0$0" }; + $R0: bv64 := Exp14__5_21:bv64 { .label = "2296_1" }; + $R0: bv64 := bvadd($R0:bv64, 0x0:bv64) { .label = "2300_0" }; + $R1: bv64 := 0x79:bv64 { .label = "2304_0" }; + store le $mem $R0:bv64 extract(8, 0, $R1:bv64) 8 { .label = "2308_0" }; + var Exp14__5_22: bv64 := load le $stack bvadd($R31:bv64, 0x18:bv64) 64 { .label = "2312_0$0" }; + $R0: bv64 := Exp14__5_22:bv64 { .label = "2312_1" }; + $R30: bv64 := 0x910:bv64 { .label = "2316_0" }; + goto(%FUN_7a0_entry_7); + ]; + block %_inlineret_3 {.originalLabel = "HVqN0/3+RWiLPKsHRvUqeg=="} [ + goto(%main_3); + ]; + block %FUN_7a0_entry_7 {.address = 0x7a0} [ + var R30_begin_FUN_7a0_1952: bv64 := $R30:bv64; + $R16: bv64 := 0x20000:bv64 { .label = "1952_0" }; + var Exp14__5_1: bv64 := load le $mem bvadd($R16:bv64, 0x28:bv64) 64 { .label = "1956_0$0" }; + $R17: bv64 := Exp14__5_1:bv64 { .label = "1956_1" }; + $R16: bv64 := bvadd($R16:bv64, 0x28:bv64) { .label = "1960_0" }; + assert eq($R30:bv64, R30_begin_FUN_7a0_1952:bv64) { .comment = "R30 = R30_in" }; + call @free () { .label = "1964_2" }; + goto(%FUN_7a0_basil_return_1_8); + ]; + block %FUN_7a0_basil_return_1_8 [ + goto(%_inlineret_3); + ]; + block %_inlineret_4 {.originalLabel = "ZLfuz7OtTNOS9GLtqSI1gg=="} [ + goto(%main_5); + ]; + block %FUN_770_entry_9 {.address = 0x770} [ + var R30_begin_FUN_770_1904: bv64 := $R30:bv64; + $R16: bv64 := 0x20000:bv64 { .label = "1904_0" }; + var Exp14__5_2: bv64 := load le $mem bvadd($R16:bv64, 0x10:bv64) 64 { .label = "1908_0$0" }; + $R17: bv64 := Exp14__5_2:bv64 { .label = "1908_1" }; + $R16: bv64 := bvadd($R16:bv64, 0x10:bv64) { .label = "1912_0" }; + assert eq($R30:bv64, R30_begin_FUN_770_1904:bv64) { .comment = "R30 = R30_in" }; + $R0: bv64 := 0x1:bv64; + call @malloc () { .label = "1916_2" }; + goto(%FUN_770_basil_return_1_10); + ]; + block %FUN_770_basil_return_1_10 [ + goto(%_inlineret_4); + ]; + block %main_basil_return_1 [ + return (); + ] +]; + + +proc @malloc () -> () + { .name = "malloc" }; + + +proc @free () -> () + { .name = "free" }; + + + + +prog entry @main { + .symbols = { + .externalFunctions = [ + { .name = "_ITM_deregisterTMCloneTable"; .offset = 0x1ffc0 }; + { .name = "_ITM_registerTMCloneTable"; .offset = 0x1ffe0 }; + { .name = "__cxa_finalize"; .offset = 0x1ffc8 }; + { .name = "__cxa_finalize"; .offset = 0x20008 }; + { .name = "__gmon_start__"; .offset = 0x1ffd0 }; + { .name = "__gmon_start__"; .offset = 0x20018 }; + { .name = "__libc_start_main"; .offset = 0x20000 }; + { .name = "abort"; .offset = 0x20020 }; + { .name = "free"; .offset = 0x20028 }; + { .name = "malloc"; .offset = 0x20010 } + ]; + .globals = [ + { .name = "_DYNAMIC"; .address = 0x1fdb8; .size = 0x0 }; + { .name = "_GLOBAL_OFFSET_TABLE_"; .address = 0x1ffb8; .size = 0x0 }; + { .name = "_IO_stdin_used"; .address = 0x930; .size = 0x20 }; + { .name = "__FRAME_END__"; .address = 0xa18; .size = 0x0 }; + { .name = "__abi_tag"; .address = 0xa1c; .size = 0x100 }; + { .name = "__do_global_dtors_aux_fini_array_entry"; .address = 0x1fdb0; .size = 0x0 }; + { .name = "__frame_dummy_init_array_entry"; .address = 0x1fda8; .size = 0x0 }; + { .name = "completed.0"; .address = 0x20040; .size = 0x8 } + ]; + .funcEntries = [ + { .name = "_start"; .address = 0x7c0; .size = 0x1a0 }; + { .name = "main"; .address = 0x8e4; .size = 0x1c0 } + ]; + .globalOffsets = [ [ 0x1fda8; 0x8e0 ]; [ 0x1fdb0; 0x88c ]; [ 0x1ffd8; 0x8e4 ]; [ 0x20038; 0x20038 ] ] + }; + .initial_memory = [ + { + .name = ".interp"; + .address = 0x238; + .size = 0x6e; + .readOnly = false; + .bytes = [ + "H4sIAAAAAAAA/y3KSQ7DIAwAwH7IuI0sJJ5j0pKaxQhSVPL75JDzDKpM3H+1f7DFRSg15sIhWiehHMk7T4lKOdxssGXxKzD3"; + "9WsJhiatf4UsOiZsOmAx9ARr8WqY3zfc3ezVvB4nF5QsKG4AAAA=" + ] + }; + { + .name = ".hash"; + .address = 0x2a8; + .size = 0x40; + .readOnly = false; + .bytes = [ "H4sIAAAAAAAA/2NmYGDgBmJ2IOYCYg4GTMAMpVmhNBsQswAxJxADAPnRrSlAAAAA" ] + }; + { + .name = ".gnu.hash"; + .address = 0x2e8; + .size = 0x1c; + .readOnly = false; + .bytes = [ "H4sIAAAAAAAA/2NkYGBghGJ0AACV1IdlHAAAAA==" ] + }; + { + .name = ".dynsym"; + .address = 0x308; + .size = 0x108; + .readOnly = false; + .bytes = [ + "H4sIAAAAAAAA/2NgwA2YGbgYBNixiYszGDAwoYjxArEQFjPkGRkYFLCJA7ESFnE2HOZY4zBHD4d6RhziXjjMAQAVCkG3CAEA"; + "AA==" + ] + }; + { + .name = ".dynstr"; + .address = 0x410; + .size = 0x164; + .readOnly = false; + .bytes = [ + "H4sIAAAAAAAA/32Qy26DMBRE/UM2jzoOdNksqkjNjr11bQwx2NfCQAN8fUGtqi7a7kajozPSkCYaQzw4FzSR0lml5ThBnKQH"; + "i3ujF5CNRXB2MwRUiBM5IDYGJsjr2/XlInOWnb/jEycJ2iUZpxBNMnS55f0A4KHpRGkbv/aqVLzn3q/lMtD2kFGAqO+C0xl7"; + "DA+kzuK80BZnmjOeUiGSHXv+4b1zyIr3TW9rrWv3OBX33ndagC/wvA0+/cfYak2zE8tZupcq+RM8Jom8VjdZm2haO04mVreL"; + "C2gqUM7s37Q+4Ndb8hP9FfwAfvdaCWQBAAA=" + ] + }; + { + .name = ".gnu.version"; + .address = 0x574; + .size = 0x16; + .readOnly = false; + .bytes = [ "H4sIAAAAAAAA/2NgAAEmBkYGZiCEkQCZ8L9vFgAAAA==" ] + }; + { + .name = ".gnu.version_r"; + .address = 0x590; + .size = 0x30; + .readOnly = false; + .bytes = [ "H4sIAAAAAAAA/2NkYGIwYWBgEGCAgOkTp7ExMDAz2EHFtoD5TAyeUHkA0/tYujAAAAA=" ] + }; + { + .name = ".rela.dyn"; + .address = 0x5c0; + .size = 0xc0; + .readOnly = false; + .bytes = [ + "H4sIAAAAAAAA/1vxl5EBBJhZwBTDAw4IvQFNvAcqfuM/qvgTqLgFAxOKOIx/AKqeESgOlQKDE0jirEjiF5DE2ZHEHyCJcyGJ"; + "AwCxyMi5wAAAAA==" + ] + }; + { + .name = ".rela.plt"; + .address = 0x680; + .size = 0x90; + .readOnly = false; + .bytes = [ + "H4sIAAAAAAAA/03IKQ4AIBDAwGa5HRKJ5P8vJCg6ciB4IkPi6/qin/qqX/qm3/quP/qhv/tWWaiQAAAA" + ] + }; + { + .name = ".init"; + .address = 0x710; + .size = 0x18; + .readOnly = false; + .bytes = [ "H4sIAAAAAAAA/5NXYL76t3r/yr/MDBPNGBim/K0+uOIAc/w1AEDwxBIYAAAA" ] + }; + { + .name = ".plt"; + .address = 0x730; + .size = 0x80; + .readOnly = false; + .bytes = [ + "H4sIAAAAAAAA//tQvX/lBwaGD4L/3H8KPLKfqMAkf01egfkqDAswMkwQZHL4KcDEAJYD89mAfCUkPheQ74TE5wPyk5D4QkB+"; + "ExJfDMhfBOEDADC+jJiAAAAA" + ] + }; + { + .name = ".text"; + .address = 0x7c0; + .size = 0x15c; + .readOnly = false; + .bytes = [ + "H4sIAAAAAAAA/22PMUvDUBSFz8tzq5DBwaU1ffZHSCZfXN5e3Fv9Gx2Ms0uDg6uLoJmdpbq6VSwIDmmpUtAh0OlCQ3oSqENx"; + "OFzeu+d83BO09XsL8fiA+tJIp9rKrIPkWyPJgBy/TjR3O9RHWd4sqPp/4cQCj1lZ7o90bxKQ85+gMARUojgN5zHwMwJOp2SY"; + "zMkZGblWKbxgUnG2/QZ4PVxdvEW7l1dmFV0/0z9j9iR3cl5nvb9sMXh6KHj3sgHZY77vRaFVOKrvnTuJ6a/5TSspe1R92oi7"; + "fU+Fy4aVYvByv93lk/02XHrHt1V/H5L5VtBEYvy4q4Cwet9xB/I2nDUFlHDbXAEAAA==" + ] + }; + { + .name = ".fini"; + .address = 0x91c; + .size = 0x14; + .readOnly = false; + .bytes = [ "H4sIAAAAAAAA/5NXYL76t3r/yr/MDBP/Vh9ccYA5/hoA8Q4mSxQAAAA=" ] + }; + { + .name = ".rodata"; + .address = 0x930; + .size = 0x4; + .readOnly = true; + .bytes = [ "H4sIAAAAAAAA/2NkYGIAAPvazqsEAAAA" ] + }; + { + .name = ".eh_frame_hdr"; + .address = 0x934; + .size = 0x3c; + .readOnly = false; + .bytes = [ + "H4sIAAAAAAAA/2OUZra2YGBgYAPinn///wcA6TdAOgVIy/z//78CSEcA6R4gvQZIbwDSG4D0ESANAFvEJ7I8AAAA" + ] + }; + { + .name = ".eh_frame"; + .address = 0x970; + .size = 0xac; + .readOnly = false; + .bytes = [ + "H4sIAAAAAAAA/xNggADGqiAGlgo5RmkeeQYBIF8CiE3+/f9vApJ0ZJcDiekAcQNQzACqByTmAMRzgGI2UDEFIA4B4iNAMQ+w"; + "Xj6FuSzzmJ0mM/ndu3uZD6avAoi/ANWwQPXJAHEPED8Bilkg6fO5d5cPqoQBAHnEQFesAAAA" + ] + }; + { + .name = ".note.ABI-tag"; + .address = 0xa1c; + .size = 0x20; + .readOnly = false; + .bytes = [ "H4sIAAAAAAAA/2NhYGAQAGJGIHb3C2UAAWYg5mKAAADshLlpIAAAAA==" ] + }; + { + .name = ".init_array"; + .address = 0x1fda8; + .size = 0x8; + .readOnly = false; + .bytes = [ "H4sIAAAAAAAA/3vAwQAGAG+0HdUIAAAA" ] + }; + { + .name = ".fini_array"; + .address = 0x1fdb0; + .size = 0x8; + .readOnly = false; + .bytes = [ "H4sIAAAAAAAA/+vhYAADAJsBWVIIAAAA" ] + }; + { + .name = ".dynamic"; + .address = 0x1fdb8; + .size = 0x200; + .readOnly = false; + .bytes = [ + "H4sIAAAAAAAA/62QvRGCQBBG91TQ82fGQAd/sAtLsQRzEwuwBMogtATKITQxYBw5B/ZtcMRu8uax97G350TrDE/wApdwPVWu"; + "8Nwr93j5dT2P+Awe4JN+PuhPLD9Svttw61jjic3nYGr5sXKOX/X3ssB3cCtxEZM6aIAxUsANZF3J4CONv1dJvEcF/WD+J+g+"; + "drTFC/IB5/rywu/0G9ze6d/1AxafZfIAAgAA" + ] + }; + { + .name = ".got"; + .address = 0x1ffb8; + .size = 0x30; + .readOnly = true; + .bytes = [ "H4sIAAAAAAAA/9vxl5EBH3jCgcoHABiL2HUwAAAA" ] + }; + { + .name = ".got.plt"; + .address = 0x1ffe8; + .size = 0x48; + .readOnly = false; + .bytes = [ "H4sIAAAAAAAA/2NgwA4M2EmjAVzvZFpIAAAA" ] + }; + { + .name = ".data"; + .address = 0x20030; + .size = 0x10; + .readOnly = false; + .bytes = [ "H4sIAAAAAAAA/2NggAALBiYwDQCWolv3EAAAAA==" ] + }; + { + .name = ".bss"; + .address = 0x20040; + .size = 0x8; + .readOnly = false; + .bytes = [ "H4sIAAAAAAAA/2NggAAAad8iZQgAAAA=" ] + } +] +} ; + diff --git a/examples/memory/malloc_free_oob.il b/examples/memory/malloc_free_oob.il new file mode 100644 index 00000000..9afb01f6 --- /dev/null +++ b/examples/memory/malloc_free_oob.il @@ -0,0 +1,332 @@ +memory shared $mem : (bv64 -> bv8); +memory $stack : (bv64 -> bv8); +var $R0: bv64; +var $R1: bv64; +var $R16: bv64; +var $R17: bv64; +var $R29: bv64; +var $R30: bv64; +var $R31: bv64; + +let $magic (a:(bv64->bv8)), (b:(bv64->bv8)) : (bv64->bv8) = (a); + +prog entry @main; + +proc @main () -> () + { .name = "main"; .address = 0x8e4; .returnBlock = "main_basil_return_1" } +[ + block %main_entry {.address = 0x8e4; .originalLabel = "ZLfuz7OtTNOS9GLtqSI1gg=="} [ + var Cse0__5_23: bv64 := bvadd($R31:bv64, 0xffffffffffffffe0:bv64) { .label = "2276_0" }; + store le $stack Cse0__5_23:bv64 $R29:bv64 64 { .label = "2276_1" }; + store le $stack bvadd(Cse0__5_23:bv64, 0x8:bv64) $R30:bv64 64 { .label = "2276_2" }; + $R31: bv64 := Cse0__5_23:bv64 { .label = "2276_3" }; + $R29: bv64 := $R31:bv64 { .label = "2280_0" }; + $R0: bv64 := 0x11:bv64 { .label = "2284_0" }; + $R30: bv64 := 0x8f4:bv64 { .label = "2288_0" }; + goto(%FUN_770_entry_9); + ]; + block %main_3 {.address = 0x910; .originalLabel = "32fWxY7+R++JNJOFTmT+Sg=="} [ + $R0: bv64 := 0x0:bv64 { .label = "2320_0" }; + var Exp16__5_24: bv64 := load le $stack $R31:bv64 64 { .label = "2324_0$0" }; + var Exp18__5_25: bv64 := load le $stack bvadd($R31:bv64, 0x8:bv64) 64 { .label = "2324_1$0" }; + $R29: bv64 := Exp16__5_24:bv64 { .label = "2324_2" }; + $R30: bv64 := Exp18__5_25:bv64 { .label = "2324_3" }; + $R31: bv64 := bvadd($R31:bv64, 0x20:bv64) { .label = "2324_4" }; + goto(%main_basil_return_1); + ]; + block %main_5 {.address = 0x8f4; .originalLabel = "HVqN0/3+RWiLPKsHRvUqeg=="} [ + store le $stack bvadd($R31:bv64, 0x18:bv64) $R0:bv64 64 { .label = "2292_0" }; + var Exp14__5_21: bv64 := load le $stack bvadd($R31:bv64, 0x18:bv64) 64 { .label = "2296_0$0" }; + $R0: bv64 := Exp14__5_21:bv64 { .label = "2296_1" }; + $R0: bv64 := bvadd($R0:bv64, 0x7:bv64) { .label = "2300_0" }; + $R1: bv64 := 0x79:bv64 { .label = "2304_0" }; + store le $mem $R0:bv64 extract(8, 0, $R1:bv64) 8 { .label = "2308_0" }; + var Exp14__5_22: bv64 := load le $stack bvadd($R31:bv64, 0x18:bv64) 64 { .label = "2312_0$0" }; + $R0: bv64 := Exp14__5_22:bv64 { .label = "2312_1" }; + $R30: bv64 := 0x910:bv64 { .label = "2316_0" }; + goto(%FUN_7a0_entry_7); + ]; + block %_inlineret_3 {.originalLabel = "HVqN0/3+RWiLPKsHRvUqeg=="} [ + goto(%main_3); + ]; + block %FUN_7a0_entry_7 {.address = 0x7a0} [ + var R30_begin_FUN_7a0_1952: bv64 := $R30:bv64; + $R16: bv64 := 0x20000:bv64 { .label = "1952_0" }; + var Exp14__5_1: bv64 := load le $mem bvadd($R16:bv64, 0x28:bv64) 64 { .label = "1956_0$0" }; + $R17: bv64 := Exp14__5_1:bv64 { .label = "1956_1" }; + $R16: bv64 := bvadd($R16:bv64, 0x28:bv64) { .label = "1960_0" }; + assert eq($R30:bv64, R30_begin_FUN_7a0_1952:bv64) { .comment = "R30 = R30_in" }; + call @free () { .label = "1964_2" }; + goto(%FUN_7a0_basil_return_1_8); + ]; + block %FUN_7a0_basil_return_1_8 [ + goto(%_inlineret_3); + ]; + block %_inlineret_4 {.originalLabel = "ZLfuz7OtTNOS9GLtqSI1gg=="} [ + goto(%main_5); + ]; + block %FUN_770_entry_9 {.address = 0x770} [ + var R30_begin_FUN_770_1904: bv64 := $R30:bv64; + $R16: bv64 := 0x20000:bv64 { .label = "1904_0" }; + var Exp14__5_2: bv64 := load le $mem bvadd($R16:bv64, 0x10:bv64) 64 { .label = "1908_0$0" }; + $R17: bv64 := Exp14__5_2:bv64 { .label = "1908_1" }; + $R16: bv64 := bvadd($R16:bv64, 0x10:bv64) { .label = "1912_0" }; + assert eq($R30:bv64, R30_begin_FUN_770_1904:bv64) { .comment = "R30 = R30_in" }; + $R0: bv64 := 0x1:bv64; + call @malloc () { .label = "1916_2" }; + goto(%FUN_770_basil_return_1_10); + ]; + block %FUN_770_basil_return_1_10 [ + goto(%_inlineret_4); + ]; + block %main_basil_return_1 [ + return (); + ] +]; + + +proc @malloc () -> () + { .name = "malloc" }; + + +proc @free () -> () + { .name = "free" }; + + + + +prog entry @main { + .symbols = { + .externalFunctions = [ + { .name = "_ITM_deregisterTMCloneTable"; .offset = 0x1ffc0 }; + { .name = "_ITM_registerTMCloneTable"; .offset = 0x1ffe0 }; + { .name = "__cxa_finalize"; .offset = 0x1ffc8 }; + { .name = "__cxa_finalize"; .offset = 0x20008 }; + { .name = "__gmon_start__"; .offset = 0x1ffd0 }; + { .name = "__gmon_start__"; .offset = 0x20018 }; + { .name = "__libc_start_main"; .offset = 0x20000 }; + { .name = "abort"; .offset = 0x20020 }; + { .name = "free"; .offset = 0x20028 }; + { .name = "malloc"; .offset = 0x20010 } + ]; + .globals = [ + { .name = "_DYNAMIC"; .address = 0x1fdb8; .size = 0x0 }; + { .name = "_GLOBAL_OFFSET_TABLE_"; .address = 0x1ffb8; .size = 0x0 }; + { .name = "_IO_stdin_used"; .address = 0x930; .size = 0x20 }; + { .name = "__FRAME_END__"; .address = 0xa18; .size = 0x0 }; + { .name = "__abi_tag"; .address = 0xa1c; .size = 0x100 }; + { .name = "__do_global_dtors_aux_fini_array_entry"; .address = 0x1fdb0; .size = 0x0 }; + { .name = "__frame_dummy_init_array_entry"; .address = 0x1fda8; .size = 0x0 }; + { .name = "completed.0"; .address = 0x20040; .size = 0x8 } + ]; + .funcEntries = [ + { .name = "_start"; .address = 0x7c0; .size = 0x1a0 }; + { .name = "main"; .address = 0x8e4; .size = 0x1c0 } + ]; + .globalOffsets = [ [ 0x1fda8; 0x8e0 ]; [ 0x1fdb0; 0x88c ]; [ 0x1ffd8; 0x8e4 ]; [ 0x20038; 0x20038 ] ] + }; + .initial_memory = [ + { + .name = ".interp"; + .address = 0x238; + .size = 0x6e; + .readOnly = false; + .bytes = [ + "H4sIAAAAAAAA/y3KSQ7DIAwAwH7IuI0sJJ5j0pKaxQhSVPL75JDzDKpM3H+1f7DFRSg15sIhWiehHMk7T4lKOdxssGXxKzD3"; + "9WsJhiatf4UsOiZsOmAx9ARr8WqY3zfc3ezVvB4nF5QsKG4AAAA=" + ] + }; + { + .name = ".hash"; + .address = 0x2a8; + .size = 0x40; + .readOnly = false; + .bytes = [ "H4sIAAAAAAAA/2NmYGDgBmJ2IOYCYg4GTMAMpVmhNBsQswAxJxADAPnRrSlAAAAA" ] + }; + { + .name = ".gnu.hash"; + .address = 0x2e8; + .size = 0x1c; + .readOnly = false; + .bytes = [ "H4sIAAAAAAAA/2NkYGBghGJ0AACV1IdlHAAAAA==" ] + }; + { + .name = ".dynsym"; + .address = 0x308; + .size = 0x108; + .readOnly = false; + .bytes = [ + "H4sIAAAAAAAA/2NgwA2YGbgYBNixiYszGDAwoYjxArEQFjPkGRkYFLCJA7ESFnE2HOZY4zBHD4d6RhziXjjMAQAVCkG3CAEA"; + "AA==" + ] + }; + { + .name = ".dynstr"; + .address = 0x410; + .size = 0x164; + .readOnly = false; + .bytes = [ + "H4sIAAAAAAAA/32Qy26DMBRE/UM2jzoOdNksqkjNjr11bQwx2NfCQAN8fUGtqi7a7kajozPSkCYaQzw4FzSR0lml5ThBnKQH"; + "i3ujF5CNRXB2MwRUiBM5IDYGJsjr2/XlInOWnb/jEycJ2iUZpxBNMnS55f0A4KHpRGkbv/aqVLzn3q/lMtD2kFGAqO+C0xl7"; + "DA+kzuK80BZnmjOeUiGSHXv+4b1zyIr3TW9rrWv3OBX33ndagC/wvA0+/cfYak2zE8tZupcq+RM8Jom8VjdZm2haO04mVreL"; + "C2gqUM7s37Q+4Ndb8hP9FfwAfvdaCWQBAAA=" + ] + }; + { + .name = ".gnu.version"; + .address = 0x574; + .size = 0x16; + .readOnly = false; + .bytes = [ "H4sIAAAAAAAA/2NgAAEmBkYGZiCEkQCZ8L9vFgAAAA==" ] + }; + { + .name = ".gnu.version_r"; + .address = 0x590; + .size = 0x30; + .readOnly = false; + .bytes = [ "H4sIAAAAAAAA/2NkYGIwYWBgEGCAgOkTp7ExMDAz2EHFtoD5TAyeUHkA0/tYujAAAAA=" ] + }; + { + .name = ".rela.dyn"; + .address = 0x5c0; + .size = 0xc0; + .readOnly = false; + .bytes = [ + "H4sIAAAAAAAA/1vxl5EBBJhZwBTDAw4IvQFNvAcqfuM/qvgTqLgFAxOKOIx/AKqeESgOlQKDE0jirEjiF5DE2ZHEHyCJcyGJ"; + "AwCxyMi5wAAAAA==" + ] + }; + { + .name = ".rela.plt"; + .address = 0x680; + .size = 0x90; + .readOnly = false; + .bytes = [ + "H4sIAAAAAAAA/03IKQ4AIBDAwGa5HRKJ5P8vJCg6ciB4IkPi6/qin/qqX/qm3/quP/qhv/tWWaiQAAAA" + ] + }; + { + .name = ".init"; + .address = 0x710; + .size = 0x18; + .readOnly = false; + .bytes = [ "H4sIAAAAAAAA/5NXYL76t3r/yr/MDBPNGBim/K0+uOIAc/w1AEDwxBIYAAAA" ] + }; + { + .name = ".plt"; + .address = 0x730; + .size = 0x80; + .readOnly = false; + .bytes = [ + "H4sIAAAAAAAA//tQvX/lBwaGD4L/3H8KPLKfqMAkf01egfkqDAswMkwQZHL4KcDEAJYD89mAfCUkPheQ74TE5wPyk5D4QkB+"; + "ExJfDMhfBOEDADC+jJiAAAAA" + ] + }; + { + .name = ".text"; + .address = 0x7c0; + .size = 0x15c; + .readOnly = false; + .bytes = [ + "H4sIAAAAAAAA/22PMUvDUBSFz8tzq5DBwaU1ffZHSCZfXN5e3Fv9Gx2Ms0uDg6uLoJmdpbq6VSwIDmmpUtAh0OlCQ3oSqENx"; + "OFzeu+d83BO09XsL8fiA+tJIp9rKrIPkWyPJgBy/TjR3O9RHWd4sqPp/4cQCj1lZ7o90bxKQ85+gMARUojgN5zHwMwJOp2SY"; + "zMkZGblWKbxgUnG2/QZ4PVxdvEW7l1dmFV0/0z9j9iR3cl5nvb9sMXh6KHj3sgHZY77vRaFVOKrvnTuJ6a/5TSspe1R92oi7"; + "fU+Fy4aVYvByv93lk/02XHrHt1V/H5L5VtBEYvy4q4Cwet9xB/I2nDUFlHDbXAEAAA==" + ] + }; + { + .name = ".fini"; + .address = 0x91c; + .size = 0x14; + .readOnly = false; + .bytes = [ "H4sIAAAAAAAA/5NXYL76t3r/yr/MDBP/Vh9ccYA5/hoA8Q4mSxQAAAA=" ] + }; + { + .name = ".rodata"; + .address = 0x930; + .size = 0x4; + .readOnly = true; + .bytes = [ "H4sIAAAAAAAA/2NkYGIAAPvazqsEAAAA" ] + }; + { + .name = ".eh_frame_hdr"; + .address = 0x934; + .size = 0x3c; + .readOnly = false; + .bytes = [ + "H4sIAAAAAAAA/2OUZra2YGBgYAPinn///wcA6TdAOgVIy/z//78CSEcA6R4gvQZIbwDSG4D0ESANAFvEJ7I8AAAA" + ] + }; + { + .name = ".eh_frame"; + .address = 0x970; + .size = 0xac; + .readOnly = false; + .bytes = [ + "H4sIAAAAAAAA/xNggADGqiAGlgo5RmkeeQYBIF8CiE3+/f9vApJ0ZJcDiekAcQNQzACqByTmAMRzgGI2UDEFIA4B4iNAMQ+w"; + "Xj6FuSzzmJ0mM/ndu3uZD6avAoi/ANWwQPXJAHEPED8Bilkg6fO5d5cPqoQBAHnEQFesAAAA" + ] + }; + { + .name = ".note.ABI-tag"; + .address = 0xa1c; + .size = 0x20; + .readOnly = false; + .bytes = [ "H4sIAAAAAAAA/2NhYGAQAGJGIHb3C2UAAWYg5mKAAADshLlpIAAAAA==" ] + }; + { + .name = ".init_array"; + .address = 0x1fda8; + .size = 0x8; + .readOnly = false; + .bytes = [ "H4sIAAAAAAAA/3vAwQAGAG+0HdUIAAAA" ] + }; + { + .name = ".fini_array"; + .address = 0x1fdb0; + .size = 0x8; + .readOnly = false; + .bytes = [ "H4sIAAAAAAAA/+vhYAADAJsBWVIIAAAA" ] + }; + { + .name = ".dynamic"; + .address = 0x1fdb8; + .size = 0x200; + .readOnly = false; + .bytes = [ + "H4sIAAAAAAAA/62QvRGCQBBG91TQ82fGQAd/sAtLsQRzEwuwBMogtATKITQxYBw5B/ZtcMRu8uax97G350TrDE/wApdwPVWu"; + "8Nwr93j5dT2P+Awe4JN+PuhPLD9Svttw61jjic3nYGr5sXKOX/X3ssB3cCtxEZM6aIAxUsANZF3J4CONv1dJvEcF/WD+J+g+"; + "drTFC/IB5/rywu/0G9ze6d/1AxafZfIAAgAA" + ] + }; + { + .name = ".got"; + .address = 0x1ffb8; + .size = 0x30; + .readOnly = true; + .bytes = [ "H4sIAAAAAAAA/9vxl5EBH3jCgcoHABiL2HUwAAAA" ] + }; + { + .name = ".got.plt"; + .address = 0x1ffe8; + .size = 0x48; + .readOnly = false; + .bytes = [ "H4sIAAAAAAAA/2NgwA4M2EmjAVzvZFpIAAAA" ] + }; + { + .name = ".data"; + .address = 0x20030; + .size = 0x10; + .readOnly = false; + .bytes = [ "H4sIAAAAAAAA/2NggAALBiYwDQCWolv3EAAAAA==" ] + }; + { + .name = ".bss"; + .address = 0x20040; + .size = 0x8; + .readOnly = false; + .bytes = [ "H4sIAAAAAAAA/2NggAAAad8iZQgAAAA=" ] + } +] +} ; + diff --git a/examples/memory/malloc_free_oob_simple.il b/examples/memory/malloc_free_oob_simple.il new file mode 100644 index 00000000..095a6ee4 --- /dev/null +++ b/examples/memory/malloc_free_oob_simple.il @@ -0,0 +1,284 @@ +memory shared $mem : (bv64 -> bv8); +memory $stack : (bv64 -> bv8); + +prog entry @main_2276; + +proc @main_2276 + (R0_in:bv64, R16_in:bv64, R17_in:bv64, R1_in:bv64, R29_in:bv64, R30_in:bv64, R31_in:bv64, _PC_in:bv64) + -> (R0_out:bv64, R17_out:bv64, R1_out:bv64, R29_out:bv64, R30_out:bv64) + { .name = "main"; .address = 0x8e4; .returnBlock = "main_return" } +[ + block %main_entry {.address = 0x8e4; .originalLabel = "ZLfuz7OtTNOS9GLtqSI1gg=="} [ + store le $stack bvadd(R31_in:bv64, 0xffffffffffffffe0:bv64) R29_in:bv64 64 { .label = "2276_1" }; + store le $stack bvadd(R31_in:bv64, 0xffffffffffffffe8:bv64) R30_in:bv64 64 { .label = "2276_2" }; + var Exp14__5_2_1: bv64 := load le $mem 0x20010:bv64 64 { .label = "1908_0$0" }; + assert true { .comment = "R30 = R30_in" }; + var (R0_3:bv64) := call @malloc (0x1:bv64) { .label = "1916_2" }; + goto(%phi_5); + ]; + block %phi_5 {.originalLabel = "HVqN0/3+RWiLPKsHRvUqeg==, ZLfuz7OtTNOS9GLtqSI1gg=="} [ + store le $stack bvadd(R31_in:bv64, 0xfffffffffffffff8:bv64) R0_3:bv64 64 { .label = "2292_0" }; + var Exp14__5_21_1: bv64 := load le $stack bvadd(R31_in:bv64, 0xfffffffffffffff8:bv64) 64 { .label = "2296_0$0" }; + store le $mem bvadd(Exp14__5_21_1:bv64, 0x7:bv64) 0x79:bv8 8 { .label = "2308_0" }; + var Exp14__5_22_1: bv64 := load le $stack bvadd(R31_in:bv64, 0xfffffffffffffff8:bv64) 64 { .label = "2312_0$0" }; + var Exp14__5_1_1: bv64 := load le $mem 0x20028:bv64 64 { .label = "1956_0$0" }; + assert true { .comment = "R30 = R30_in" }; + call @#free (Exp14__5_22_1:bv64) { .label = "1964_2" }; + goto(%phi_6); + ]; + block %phi_6 {.originalLabel = "32fWxY7+R++JNJOFTmT+Sg==, HVqN0/3+RWiLPKsHRvUqeg=="} [ + var Exp16__5_24_1: bv64 := load le $stack bvadd(R31_in:bv64, 0xffffffffffffffe0:bv64) 64 { .label = "2324_0$0" }; + var Exp18__5_25_1: bv64 := load le $stack bvadd(R31_in:bv64, 0xffffffffffffffe8:bv64) 64 { .label = "2324_1$0" }; + goto(%main_return); + ]; + block %main_return [ + return (0x0:bv64, Exp14__5_1_1:bv64, 0x79:bv64, Exp16__5_24_1:bv64, Exp18__5_25_1:bv64); + ] +]; + + +proc @malloc (R0_in:bv64) -> (R0_out:bv64) + { .name = "malloc" }; + + +proc @#free (R0_in:bv64) -> () + { .name = "#free" }; + + + + +prog entry @main_2276 { + .symbols = { + .externalFunctions = [ + { .name = "_ITM_deregisterTMCloneTable"; .offset = 0x1ffc0 }; + { .name = "_ITM_registerTMCloneTable"; .offset = 0x1ffe0 }; + { .name = "__cxa_finalize"; .offset = 0x1ffc8 }; + { .name = "__cxa_finalize"; .offset = 0x20008 }; + { .name = "__gmon_start__"; .offset = 0x1ffd0 }; + { .name = "__gmon_start__"; .offset = 0x20018 }; + { .name = "__libc_start_main"; .offset = 0x20000 }; + { .name = "abort"; .offset = 0x20020 }; + { .name = "free"; .offset = 0x20028 }; + { .name = "malloc"; .offset = 0x20010 } + ]; + .globals = [ + { .name = "_DYNAMIC"; .address = 0x1fdb8; .size = 0x0 }; + { .name = "_GLOBAL_OFFSET_TABLE_"; .address = 0x1ffb8; .size = 0x0 }; + { .name = "_IO_stdin_used"; .address = 0x930; .size = 0x20 }; + { .name = "__FRAME_END__"; .address = 0xa18; .size = 0x0 }; + { .name = "__abi_tag"; .address = 0xa1c; .size = 0x100 }; + { .name = "__do_global_dtors_aux_fini_array_entry"; .address = 0x1fdb0; .size = 0x0 }; + { .name = "__frame_dummy_init_array_entry"; .address = 0x1fda8; .size = 0x0 }; + { .name = "completed.0"; .address = 0x20040; .size = 0x8 } + ]; + .funcEntries = [ + { .name = "_start"; .address = 0x7c0; .size = 0x1a0 }; + { .name = "main"; .address = 0x8e4; .size = 0x1c0 } + ]; + .globalOffsets = [ [ 0x1fda8; 0x8e0 ]; [ 0x1fdb0; 0x88c ]; [ 0x1ffd8; 0x8e4 ]; [ 0x20038; 0x20038 ] ] + }; + .initial_memory = [ + { + .name = ".interp"; + .address = 0x238; + .size = 0x6e; + .readOnly = false; + .bytes = [ + "H4sIAAAAAAAA/y3KSQ7DIAwAwH7IuI0sJJ5j0pKaxQhSVPL75JDzDKpM3H+1f7DFRSg15sIhWiehHMk7T4lKOdxssGXxKzD3"; + "9WsJhiatf4UsOiZsOmAx9ARr8WqY3zfc3ezVvB4nF5QsKG4AAAA=" + ] + }; + { + .name = ".hash"; + .address = 0x2a8; + .size = 0x40; + .readOnly = false; + .bytes = [ "H4sIAAAAAAAA/2NmYGDgBmJ2IOYCYg4GTMAMpVmhNBsQswAxJxADAPnRrSlAAAAA" ] + }; + { + .name = ".gnu.hash"; + .address = 0x2e8; + .size = 0x1c; + .readOnly = false; + .bytes = [ "H4sIAAAAAAAA/2NkYGBghGJ0AACV1IdlHAAAAA==" ] + }; + { + .name = ".dynsym"; + .address = 0x308; + .size = 0x108; + .readOnly = false; + .bytes = [ + "H4sIAAAAAAAA/2NgwA2YGbgYBNixiYszGDAwoYjxArEQFjPkGRkYFLCJA7ESFnE2HOZY4zBHD4d6RhziXjjMAQAVCkG3CAEA"; + "AA==" + ] + }; + { + .name = ".dynstr"; + .address = 0x410; + .size = 0x164; + .readOnly = false; + .bytes = [ + "H4sIAAAAAAAA/32Qy26DMBRE/UM2jzoOdNksqkjNjr11bQwx2NfCQAN8fUGtqi7a7kajozPSkCYaQzw4FzSR0lml5ThBnKQH"; + "i3ujF5CNRXB2MwRUiBM5IDYGJsjr2/XlInOWnb/jEycJ2iUZpxBNMnS55f0A4KHpRGkbv/aqVLzn3q/lMtD2kFGAqO+C0xl7"; + "DA+kzuK80BZnmjOeUiGSHXv+4b1zyIr3TW9rrWv3OBX33ndagC/wvA0+/cfYak2zE8tZupcq+RM8Jom8VjdZm2haO04mVreL"; + "C2gqUM7s37Q+4Ndb8hP9FfwAfvdaCWQBAAA=" + ] + }; + { + .name = ".gnu.version"; + .address = 0x574; + .size = 0x16; + .readOnly = false; + .bytes = [ "H4sIAAAAAAAA/2NgAAEmBkYGZiCEkQCZ8L9vFgAAAA==" ] + }; + { + .name = ".gnu.version_r"; + .address = 0x590; + .size = 0x30; + .readOnly = false; + .bytes = [ "H4sIAAAAAAAA/2NkYGIwYWBgEGCAgOkTp7ExMDAz2EHFtoD5TAyeUHkA0/tYujAAAAA=" ] + }; + { + .name = ".rela.dyn"; + .address = 0x5c0; + .size = 0xc0; + .readOnly = false; + .bytes = [ + "H4sIAAAAAAAA/1vxl5EBBJhZwBTDAw4IvQFNvAcqfuM/qvgTqLgFAxOKOIx/AKqeESgOlQKDE0jirEjiF5DE2ZHEHyCJcyGJ"; + "AwCxyMi5wAAAAA==" + ] + }; + { + .name = ".rela.plt"; + .address = 0x680; + .size = 0x90; + .readOnly = false; + .bytes = [ + "H4sIAAAAAAAA/03IKQ4AIBDAwGa5HRKJ5P8vJCg6ciB4IkPi6/qin/qqX/qm3/quP/qhv/tWWaiQAAAA" + ] + }; + { + .name = ".init"; + .address = 0x710; + .size = 0x18; + .readOnly = false; + .bytes = [ "H4sIAAAAAAAA/5NXYL76t3r/yr/MDBPNGBim/K0+uOIAc/w1AEDwxBIYAAAA" ] + }; + { + .name = ".plt"; + .address = 0x730; + .size = 0x80; + .readOnly = false; + .bytes = [ + "H4sIAAAAAAAA//tQvX/lBwaGD4L/3H8KPLKfqMAkf01egfkqDAswMkwQZHL4KcDEAJYD89mAfCUkPheQ74TE5wPyk5D4QkB+"; + "ExJfDMhfBOEDADC+jJiAAAAA" + ] + }; + { + .name = ".text"; + .address = 0x7c0; + .size = 0x15c; + .readOnly = false; + .bytes = [ + "H4sIAAAAAAAA/22PMUvDUBSFz8tzq5DBwaU1ffZHSCZfXN5e3Fv9Gx2Ms0uDg6uLoJmdpbq6VSwIDmmpUtAh0OlCQ3oSqENx"; + "OFzeu+d83BO09XsL8fiA+tJIp9rKrIPkWyPJgBy/TjR3O9RHWd4sqPp/4cQCj1lZ7o90bxKQ85+gMARUojgN5zHwMwJOp2SY"; + "zMkZGblWKbxgUnG2/QZ4PVxdvEW7l1dmFV0/0z9j9iR3cl5nvb9sMXh6KHj3sgHZY77vRaFVOKrvnTuJ6a/5TSspe1R92oi7"; + "fU+Fy4aVYvByv93lk/02XHrHt1V/H5L5VtBEYvy4q4Cwet9xB/I2nDUFlHDbXAEAAA==" + ] + }; + { + .name = ".fini"; + .address = 0x91c; + .size = 0x14; + .readOnly = false; + .bytes = [ "H4sIAAAAAAAA/5NXYL76t3r/yr/MDBP/Vh9ccYA5/hoA8Q4mSxQAAAA=" ] + }; + { + .name = ".rodata"; + .address = 0x930; + .size = 0x4; + .readOnly = true; + .bytes = [ "H4sIAAAAAAAA/2NkYGIAAPvazqsEAAAA" ] + }; + { + .name = ".eh_frame_hdr"; + .address = 0x934; + .size = 0x3c; + .readOnly = false; + .bytes = [ + "H4sIAAAAAAAA/2OUZra2YGBgYAPinn///wcA6TdAOgVIy/z//78CSEcA6R4gvQZIbwDSG4D0ESANAFvEJ7I8AAAA" + ] + }; + { + .name = ".eh_frame"; + .address = 0x970; + .size = 0xac; + .readOnly = false; + .bytes = [ + "H4sIAAAAAAAA/xNggADGqiAGlgo5RmkeeQYBIF8CiE3+/f9vApJ0ZJcDiekAcQNQzACqByTmAMRzgGI2UDEFIA4B4iNAMQ+w"; + "Xj6FuSzzmJ0mM/ndu3uZD6avAoi/ANWwQPXJAHEPED8Bilkg6fO5d5cPqoQBAHnEQFesAAAA" + ] + }; + { + .name = ".note.ABI-tag"; + .address = 0xa1c; + .size = 0x20; + .readOnly = false; + .bytes = [ "H4sIAAAAAAAA/2NhYGAQAGJGIHb3C2UAAWYg5mKAAADshLlpIAAAAA==" ] + }; + { + .name = ".init_array"; + .address = 0x1fda8; + .size = 0x8; + .readOnly = false; + .bytes = [ "H4sIAAAAAAAA/3vAwQAGAG+0HdUIAAAA" ] + }; + { + .name = ".fini_array"; + .address = 0x1fdb0; + .size = 0x8; + .readOnly = false; + .bytes = [ "H4sIAAAAAAAA/+vhYAADAJsBWVIIAAAA" ] + }; + { + .name = ".dynamic"; + .address = 0x1fdb8; + .size = 0x200; + .readOnly = false; + .bytes = [ + "H4sIAAAAAAAA/62QvRGCQBBG91TQ82fGQAd/sAtLsQRzEwuwBMogtATKITQxYBw5B/ZtcMRu8uax97G350TrDE/wApdwPVWu"; + "8Nwr93j5dT2P+Awe4JN+PuhPLD9Svttw61jjic3nYGr5sXKOX/X3ssB3cCtxEZM6aIAxUsANZF3J4CONv1dJvEcF/WD+J+g+"; + "drTFC/IB5/rywu/0G9ze6d/1AxafZfIAAgAA" + ] + }; + { + .name = ".got"; + .address = 0x1ffb8; + .size = 0x30; + .readOnly = true; + .bytes = [ "H4sIAAAAAAAA/9vxl5EBH3jCgcoHABiL2HUwAAAA" ] + }; + { + .name = ".got.plt"; + .address = 0x1ffe8; + .size = 0x48; + .readOnly = false; + .bytes = [ "H4sIAAAAAAAA/2NgwA4M2EmjAVzvZFpIAAAA" ] + }; + { + .name = ".data"; + .address = 0x20030; + .size = 0x10; + .readOnly = false; + .bytes = [ "H4sIAAAAAAAA/2NggAALBiYwDQCWolv3EAAAAA==" ] + }; + { + .name = ".bss"; + .address = 0x20040; + .size = 0x8; + .readOnly = false; + .bytes = [ "H4sIAAAAAAAA/2NggAAAad8iZQgAAAA=" ] + } +] +} ; + diff --git a/examples/memory/malloc_free_simple.il b/examples/memory/malloc_free_simple.il new file mode 100644 index 00000000..ee282188 --- /dev/null +++ b/examples/memory/malloc_free_simple.il @@ -0,0 +1,284 @@ +memory shared $mem : (bv64 -> bv8); +memory $stack : (bv64 -> bv8); + +prog entry @main_2276; + +proc @main_2276 + (R0_in:bv64, R16_in:bv64, R17_in:bv64, R1_in:bv64, R29_in:bv64, R30_in:bv64, R31_in:bv64, _PC_in:bv64) + -> (R0_out:bv64, R17_out:bv64, R1_out:bv64, R29_out:bv64, R30_out:bv64) + { .name = "main"; .address = 0x8e4; .returnBlock = "main_return" } +[ + block %main_entry {.address = 0x8e4; .originalLabel = "ZLfuz7OtTNOS9GLtqSI1gg=="} [ + store le $stack bvadd(R31_in:bv64, 0xffffffffffffffe0:bv64) R29_in:bv64 64 { .label = "2276_1" }; + store le $stack bvadd(R31_in:bv64, 0xffffffffffffffe8:bv64) R30_in:bv64 64 { .label = "2276_2" }; + var Exp14__5_2_1: bv64 := load le $mem 0x20010:bv64 64 { .label = "1908_0$0" }; + assert true { .comment = "R30 = R30_in" }; + var (R0_3:bv64) := call @malloc (0x1:bv64) { .label = "1916_2" }; + goto(%phi_5); + ]; + block %phi_5 {.originalLabel = "HVqN0/3+RWiLPKsHRvUqeg==, ZLfuz7OtTNOS9GLtqSI1gg=="} [ + store le $stack bvadd(R31_in:bv64, 0xfffffffffffffff8:bv64) R0_3:bv64 64 { .label = "2292_0" }; + var Exp14__5_21_1: bv64 := load le $stack bvadd(R31_in:bv64, 0xfffffffffffffff8:bv64) 64 { .label = "2296_0$0" }; + store le $mem Exp14__5_21_1:bv64 0x79:bv8 8 { .label = "2304_0" }; + var Exp14__5_22_1: bv64 := load le $stack bvadd(R31_in:bv64, 0xfffffffffffffff8:bv64) 64 { .label = "2308_0$0" }; + var Exp14__5_1_1: bv64 := load le $mem 0x20028:bv64 64 { .label = "1956_0$0" }; + assert true { .comment = "R30 = R30_in" }; + call @#free (Exp14__5_22_1:bv64) { .label = "1964_2" }; + goto(%phi_6); + ]; + block %phi_6 {.originalLabel = "32fWxY7+R++JNJOFTmT+Sg==, HVqN0/3+RWiLPKsHRvUqeg=="} [ + var Exp16__5_24_1: bv64 := load le $stack bvadd(R31_in:bv64, 0xffffffffffffffe0:bv64) 64 { .label = "2320_0$0" }; + var Exp18__5_25_1: bv64 := load le $stack bvadd(R31_in:bv64, 0xffffffffffffffe8:bv64) 64 { .label = "2320_1$0" }; + goto(%main_return); + ]; + block %main_return [ + return (0x0:bv64, Exp14__5_1_1:bv64, 0x79:bv64, Exp16__5_24_1:bv64, Exp18__5_25_1:bv64); + ] +]; + + +proc @malloc (R0_in:bv64) -> (R0_out:bv64) + { .name = "malloc" }; + + +proc @#free (R0_in:bv64) -> () + { .name = "#free" }; + + + + +prog entry @main_2276 { + .symbols = { + .externalFunctions = [ + { .name = "_ITM_deregisterTMCloneTable"; .offset = 0x1ffc0 }; + { .name = "_ITM_registerTMCloneTable"; .offset = 0x1ffe0 }; + { .name = "__cxa_finalize"; .offset = 0x1ffc8 }; + { .name = "__cxa_finalize"; .offset = 0x20008 }; + { .name = "__gmon_start__"; .offset = 0x1ffd0 }; + { .name = "__gmon_start__"; .offset = 0x20018 }; + { .name = "__libc_start_main"; .offset = 0x20000 }; + { .name = "abort"; .offset = 0x20020 }; + { .name = "free"; .offset = 0x20028 }; + { .name = "malloc"; .offset = 0x20010 } + ]; + .globals = [ + { .name = "_DYNAMIC"; .address = 0x1fdb8; .size = 0x0 }; + { .name = "_GLOBAL_OFFSET_TABLE_"; .address = 0x1ffb8; .size = 0x0 }; + { .name = "_IO_stdin_used"; .address = 0x92c; .size = 0x20 }; + { .name = "__FRAME_END__"; .address = 0xa18; .size = 0x0 }; + { .name = "__abi_tag"; .address = 0xa1c; .size = 0x100 }; + { .name = "__do_global_dtors_aux_fini_array_entry"; .address = 0x1fdb0; .size = 0x0 }; + { .name = "__frame_dummy_init_array_entry"; .address = 0x1fda8; .size = 0x0 }; + { .name = "completed.0"; .address = 0x20040; .size = 0x8 } + ]; + .funcEntries = [ + { .name = "_start"; .address = 0x7c0; .size = 0x1a0 }; + { .name = "main"; .address = 0x8e4; .size = 0x1a0 } + ]; + .globalOffsets = [ [ 0x1fda8; 0x8e0 ]; [ 0x1fdb0; 0x88c ]; [ 0x1ffd8; 0x8e4 ]; [ 0x20038; 0x20038 ] ] + }; + .initial_memory = [ + { + .name = ".interp"; + .address = 0x238; + .size = 0x6e; + .readOnly = false; + .bytes = [ + "H4sIAAAAAAAA/y3KSQ7DIAwAwH7IuI0sJJ5j0pKaxQhSVPL75JDzDKpM3H+1f7DFRSg15sIhWiehHMk7T4lKOdxssGXxKzD3"; + "9WsJhiatf4UsOiZsOmAx9ARr8WqY3zfc3ezVvB4nF5QsKG4AAAA=" + ] + }; + { + .name = ".hash"; + .address = 0x2a8; + .size = 0x40; + .readOnly = false; + .bytes = [ "H4sIAAAAAAAA/2NmYGDgBmJ2IOYCYg4GTMAMpVmhNBsQswAxJxADAPnRrSlAAAAA" ] + }; + { + .name = ".gnu.hash"; + .address = 0x2e8; + .size = 0x1c; + .readOnly = false; + .bytes = [ "H4sIAAAAAAAA/2NkYGBghGJ0AACV1IdlHAAAAA==" ] + }; + { + .name = ".dynsym"; + .address = 0x308; + .size = 0x108; + .readOnly = false; + .bytes = [ + "H4sIAAAAAAAA/2NgwA2YGbgYBNixiYszGDAwoYjxArEQFjPkGRkYFLCJA7ESFnE2HOZY4zBHD4d6RhziXjjMAQAVCkG3CAEA"; + "AA==" + ] + }; + { + .name = ".dynstr"; + .address = 0x410; + .size = 0x164; + .readOnly = false; + .bytes = [ + "H4sIAAAAAAAA/32Qy26DMBRE/UM2jzoOdNksqkjNjr11bQwx2NfCQAN8fUGtqi7a7kajozPSkCYaQzw4FzSR0lml5ThBnKQH"; + "i3ujF5CNRXB2MwRUiBM5IDYGJsjr2/XlInOWnb/jEycJ2iUZpxBNMnS55f0A4KHpRGkbv/aqVLzn3q/lMtD2kFGAqO+C0xl7"; + "DA+kzuK80BZnmjOeUiGSHXv+4b1zyIr3TW9rrWv3OBX33ndagC/wvA0+/cfYak2zE8tZupcq+RM8Jom8VjdZm2haO04mVreL"; + "C2gqUM7s37Q+4Ndb8hP9FfwAfvdaCWQBAAA=" + ] + }; + { + .name = ".gnu.version"; + .address = 0x574; + .size = 0x16; + .readOnly = false; + .bytes = [ "H4sIAAAAAAAA/2NgAAEmBkYGZiCEkQCZ8L9vFgAAAA==" ] + }; + { + .name = ".gnu.version_r"; + .address = 0x590; + .size = 0x30; + .readOnly = false; + .bytes = [ "H4sIAAAAAAAA/2NkYGIwYWBgEGCAgOkTp7ExMDAz2EHFtoD5TAyeUHkA0/tYujAAAAA=" ] + }; + { + .name = ".rela.dyn"; + .address = 0x5c0; + .size = 0xc0; + .readOnly = false; + .bytes = [ + "H4sIAAAAAAAA/1vxl5EBBJhZwBTDAw4IvQFNvAcqfuM/qvgTqLgFAxOKOIx/AKqeESgOlQKDE0jirEjiF5DE2ZHEHyCJcyGJ"; + "AwCxyMi5wAAAAA==" + ] + }; + { + .name = ".rela.plt"; + .address = 0x680; + .size = 0x90; + .readOnly = false; + .bytes = [ + "H4sIAAAAAAAA/03IKQ4AIBDAwGa5HRKJ5P8vJCg6ciB4IkPi6/qin/qqX/qm3/quP/qhv/tWWaiQAAAA" + ] + }; + { + .name = ".init"; + .address = 0x710; + .size = 0x18; + .readOnly = false; + .bytes = [ "H4sIAAAAAAAA/5NXYL76t3r/yr/MDBPNGBim/K0+uOIAc/w1AEDwxBIYAAAA" ] + }; + { + .name = ".plt"; + .address = 0x730; + .size = 0x80; + .readOnly = false; + .bytes = [ + "H4sIAAAAAAAA//tQvX/lBwaGD4L/3H8KPLKfqMAkf01egfkqDAswMkwQZHL4KcDEAJYD89mAfCUkPheQ74TE5wPyk5D4QkB+"; + "ExJfDMhfBOEDADC+jJiAAAAA" + ] + }; + { + .name = ".text"; + .address = 0x7c0; + .size = 0x158; + .readOnly = false; + .bytes = [ + "H4sIAAAAAAAA/22PMUvDUBSFz8tzq5DBwcWaPv0RkskXl7cXd6t/o4Nx7tLg4OokmtlZqqtbSwuCQ1pUCnUIdLrQkJ4E6lAc"; + "Dvdx3zkf9wQtPW4iHh5S3xrpVFuZHSP50UgyIMevE82/HeqjLO/mVL2fO7HAc1aW+wN9MQnI+U9Q6AMqUZyG8xRYDIDzKRkm"; + "c3JJRq5VCi+YVJxtvwHej1bXo2j3pmdW0e0r/TNmz3InV3XW+8sW3ZengncvG5A95jteFFqFk/reLycx/TX/wErKHlWfFuJ2"; + "x1PhsmGl6L49bnf5ZL8Nl97hfdXfh2S+FePHbQWE1fuBe5C1YawB799ywFgBAAA=" + ] + }; + { + .name = ".fini"; + .address = 0x918; + .size = 0x14; + .readOnly = false; + .bytes = [ "H4sIAAAAAAAA/5NXYL76t3r/yr/MDBP/Vh9ccYA5/hoA8Q4mSxQAAAA=" ] + }; + { + .name = ".rodata"; + .address = 0x92c; + .size = 0x4; + .readOnly = true; + .bytes = [ "H4sIAAAAAAAA/2NkYGIAAPvazqsEAAAA" ] + }; + { + .name = ".eh_frame_hdr"; + .address = 0x930; + .size = 0x3c; + .readOnly = false; + .bytes = [ + "H4sIAAAAAAAA/2OUZra2YWBgYAPiCf/+/w8B0h+AdAaQVvj//38NkI4B0hOA9AYgvQVIbwHSJ4A0ALBWOLI8AAAA" + ] + }; + { + .name = ".eh_frame"; + .address = 0x970; + .size = 0xac; + .readOnly = false; + .bytes = [ + "H4sIAAAAAAAA/xNggADGqiAGlgo5RmkeeQYBIF8CiE3+/f9vApJ0ZJcDiekAcQNQzACqByTmAMRzgGI2UDEFIA4B4iNAMQ+w"; + "Xj6FuSzzmJ0mM/ndu3uZD6avAoi/ANWwQPXJAHEPED+B2wnR533vLh9UCQMAF4/TmKwAAAA=" + ] + }; + { + .name = ".note.ABI-tag"; + .address = 0xa1c; + .size = 0x20; + .readOnly = false; + .bytes = [ "H4sIAAAAAAAA/2NhYGAQAGJGIHb3C2UAAWYg5mKAAADshLlpIAAAAA==" ] + }; + { + .name = ".init_array"; + .address = 0x1fda8; + .size = 0x8; + .readOnly = false; + .bytes = [ "H4sIAAAAAAAA/3vAwQAGAG+0HdUIAAAA" ] + }; + { + .name = ".fini_array"; + .address = 0x1fdb0; + .size = 0x8; + .readOnly = false; + .bytes = [ "H4sIAAAAAAAA/+vhYAADAJsBWVIIAAAA" ] + }; + { + .name = ".dynamic"; + .address = 0x1fdb8; + .size = 0x200; + .readOnly = false; + .bytes = [ + "H4sIAAAAAAAA/62QvRGCQBBGF+VHEGcMdPylC0uhBHISC7AEyjC0BMohJDFwHDlH9m1wxG7y5rH33d4SiNYFFrCEOVwnyhW+"; + "T5UH/P4JRp7wBTzCB/3zpB9afqZ8Dq7+scMjm8/B2PJzZYZXer0s7X1wK34Rk85pgDHSwA1kXdnBW+x/byN/jxamk/lvp/vY"; + "0QFvyDuc50uPX+m/cPtP/64vQ0gXnAACAAA=" + ] + }; + { + .name = ".got"; + .address = 0x1ffb8; + .size = 0x30; + .readOnly = true; + .bytes = [ "H4sIAAAAAAAA/9vxl5EBH3jCgcoHABiL2HUwAAAA" ] + }; + { + .name = ".got.plt"; + .address = 0x1ffe8; + .size = 0x48; + .readOnly = false; + .bytes = [ "H4sIAAAAAAAA/2NgwA4M2EmjAVzvZFpIAAAA" ] + }; + { + .name = ".data"; + .address = 0x20030; + .size = 0x10; + .readOnly = false; + .bytes = [ "H4sIAAAAAAAA/2NggAALBiYwDQCWolv3EAAAAA==" ] + }; + { + .name = ".bss"; + .address = 0x20040; + .size = 0x8; + .readOnly = false; + .bytes = [ "H4sIAAAAAAAA/2NggAAAad8iZQgAAAA=" ] + } +] +} ; + diff --git a/lib/analysis/defuse_bool.ml b/lib/analysis/defuse_bool.ml index 2275f1e6..b75759f7 100644 --- a/lib/analysis/defuse_bool.ml +++ b/lib/analysis/defuse_bool.ml @@ -62,9 +62,9 @@ module IsZeroValueAbstraction = struct | `SignExtend _ -> ( match a with Zero -> Zero | _ -> Top) | `BVNOT -> ( match a with Zero -> NonZero | _ -> Top) | `ZeroExtend size -> a - | `Old -> Top - | `FACCESS offset -> ( match a with Zero -> Zero | _ -> Top) - | `Gamma | `Classification -> Top + | `Old | `Gamma | `Classification -> Top + (* NOTE: More effort would be needed to be able to say is this one field zero or not *) + | `ReadField offset -> ( match a with Zero -> Zero | _ -> Top) let eval_binop (op : Lang.Ops.AllOps.binary) a b = match (op, a, b) with @@ -110,10 +110,10 @@ module IsZeroValueAbstraction = struct | `INTSUB, _, _ -> Top | `BVSLT, Zero, Zero -> Zero | `BVSLT, _, _ -> Top - | `FSET _, Zero, Zero -> Zero - | `FSET _, _, NonZero -> NonZero + | `WriteField _, Zero, Zero -> Zero + | `WriteField _, _, NonZero -> NonZero (* Larger refactor would be needed to reason about individual fields *) - | `FSET _, _, _ -> Top + | `WriteField _, _, _ -> Top | #Lang.Ops.Spec.binary, _, _ -> Top let eval_intrin (op : Lang.Ops.AllOps.intrin) (args : t list) = diff --git a/lib/analysis/wp_dual.ml b/lib/analysis/wp_dual.ml index 70a78579..e8e23004 100644 --- a/lib/analysis/wp_dual.ml +++ b/lib/analysis/wp_dual.ml @@ -164,4 +164,4 @@ proc @main () -> () IntraAnalysis.A.M.find Procedure.Vert.Entry res |> IntraDomain.to_pred |> BasilExpr.to_string |> print_endline; [%expect - {| booland(eq(bvadd($x:bv64, a:bv64), 0), eq(bvadd(a:bv64, a:bv64), 0)) |}] + {| booland(eq(bvadd($x, a), 0), eq(bvadd(a, a), 0)) |}] diff --git a/lib/analysis/wrapped_intervals.ml b/lib/analysis/wrapped_intervals.ml index ae4f8e0b..8f24bffa 100644 --- a/lib/analysis/wrapped_intervals.ml +++ b/lib/analysis/wrapped_intervals.ml @@ -701,6 +701,7 @@ module WrappedIntervalsValueAbstraction = struct if size bv = 0 then top else interval bv bv (* NOTE: This kind of thing happens frequently, should I go through all of the fields and make a intervals out of those bvs?*) | `Record fields -> top + | `Sort _ -> top let eval_unop (op : Lang.Ops.AllOps.unary) (a, t) rt = match t with diff --git a/lib/backends/boogie.ml b/lib/backends/boogie.ml index e20fa36f..1e2e725c 100644 --- a/lib/backends/boogie.ml +++ b/lib/backends/boogie.ml @@ -38,6 +38,8 @@ let rec type_to_string (t : Types.t) = | Types.Bitvector i -> String.cat "bv" (Int.to_string i) | Types.Map (i, o) -> String.concat "" [ "["; type_to_string i; "]"; type_to_string o ] + | Types.Variable s -> s + | Types.Sort (s, vs) -> s | t -> raise (BoogieException (String.cat "Unsupported type" (Types.to_string t))) @@ -66,6 +68,7 @@ let pretty_const (c : Lang.Ops.AllOps.const) = | `Record _ -> raise (BoogieException "records unsupported by boogie backend") | `Pointer _ -> raise (BoogieException "pointers unsupported by boogie backend") + | `Sort _ -> raise (BoogieException "const sorts unsupported by boogie backend") let pretty_call_args_no_brackets (args : Containers_pp.t list) = let open Containers_pp in @@ -90,6 +93,8 @@ let pretty_binary_expr (op : Lang.Ops.AllOps.binary) (ty1, arg1) (ty2, arg2) let open Containers_pp in match op with | `MapAccess -> arg1 ^ bracket "[" arg2 "]" + | `WriteField s -> + arg1 ^ text "->" ^ bracket "(" (text s ^+ text ":=" ^+ arg2) ")" | _ -> ( match Transforms.Boogie_prepass.Builtins.name op [ ty1; ty2; t ] with | Function name -> text name ^ pretty_call_args [ arg1; arg2 ] @@ -165,7 +170,7 @@ and pretty_attribute_map (key : string) "}") |> append_sp -and pretty_triggers attrib = +and pretty_triggers (attrib : Lang.Program.e Lang.Attrib.t option) = let open Containers_pp in Lang.Attrib.find_opt ".triggers" attrib |> Option.map (fun attrib -> @@ -173,6 +178,7 @@ and pretty_triggers attrib = @@ List.map (fun b -> bracket "{" b "}") @@ pretty_attribute attrib) |> Option.get_or ~default:(text "") + (* Option.map (Lang.Attrib.attrib_pretty Lang.Expr.BasilExpr.pretty) attrib |> Option.get_or ~default:(text "MAGIC") *) and pretty_binding_expr ?(attrib : Lang.Program.e Lang.Attrib.t option) bound in_body = @@ -196,7 +202,7 @@ and pretty_expr_alg | `Exists -> "exists" | `Lambda -> "lambda" in - bracket "(" (op ^+ pretty_binding_expr bound_vars in_body) ")" + bracket "(" (op ^+ pretty_binding_expr ?attrib bound_vars in_body) ")" | UnaryExpr { op; arg } -> pretty_unary_expr op arg (type_of e) | BinaryExpr { op; arg1; arg2 } -> pretty_binary_expr op arg1 arg2 (type_of e) | ApplyIntrin { op; args } -> pretty_apply_intrinsic op args (type_of e) @@ -225,6 +231,26 @@ let pretty_function_body funcname (e : Lang.Program.e) = (Var.to_string funcname) (Lang.Expr.BasilExpr.to_string e))) +let pretty_variant_declaration (v : Types.variant) = + let open Containers_pp in + text v.variant + ^ bracket "(" + (append_l + ~sep:(text "," ^ sp) + (List.map + (fun (f : Types.field) -> + text f.field ^ text ":" ^+ text (type_to_string f.typ)) + v.fields)) + ")" + +let pretty_type_declaration (binding : string) (typ : Types.t) = + let open Containers_pp in + match typ with + | Types.Sort (s, vs) -> + text "datatype" ^+ text binding + ^+ bracket "{" (append_sp (List.map pretty_variant_declaration vs)) "}" + | _ -> raise (BoogieException "Unsupported type declaration") + let pretty_declaration (d : Lang.Program.declaration) = let open Containers_pp in let open Containers_pp.Infix in @@ -234,6 +260,11 @@ let pretty_declaration (d : Lang.Program.declaration) = | Lang.Program.Function { binding; attrib; definition = Function t } -> let func_body, return_type = pretty_function_body binding t in + (* Ideally use above return type + * but unfortunately curry will uncurry returned maps... :( *) + let return_type = Lang.Expr.BasilExpr.type_of t in + let return_type = text @@ type_to_string return_type in + text "function" ^+ pretty_attribute_map ".boogie" attrib ^+ (function_name @@ Var.name binding) @@ -258,9 +289,7 @@ let pretty_declaration (d : Lang.Program.declaration) = ")" ^ bracket " returns (" (text (type_to_string rt)) ")" ^ text ";" - | Lang.Program.Type _ -> - raise - (BoogieException "generation of boogie datatypes is unsupported for now") + | Lang.Program.Type { binding; typ } -> pretty_type_declaration binding typ let rec pretty_statement (s : Lang.Program.stmt) = let open Containers_pp in @@ -395,15 +424,13 @@ let pretty_procedure_impl (p : Lang.Program.proc) = let in_params = Lang.Procedure.formal_in_params p in let out_params = Lang.Procedure.formal_out_params p in let local_decls = - if StringMap.cardinal in_params + StringMap.cardinal out_params > 0 then - Lang.Procedure.local_decls p - |> Hashtbl.to_list - |> List.filter (fun (k, v) -> - (Option.is_none @@ StringMap.get k in_params) - && (Option.is_none @@ StringMap.get k out_params)) - |> List.map (fun (k, v) -> pretty_variable_declaration v) - |> join_lines_end - else text "" + Lang.Procedure.local_decls p + |> Hashtbl.to_list + |> List.filter (fun (k, v) -> + (Option.is_none @@ StringMap.get k in_params) + && (Option.is_none @@ StringMap.get k out_params)) + |> List.map (fun (k, v) -> pretty_variable_declaration v) + |> join_lines_end in let blocks = Lang.Procedure.iter_blocks_topo_fwd p diff --git a/lib/fe/AbsBasilIR.ml b/lib/fe/AbsBasilIR.ml index f7e61fe9..44ae0a30 100644 --- a/lib/fe/AbsBasilIR.ml +++ b/lib/fe/AbsBasilIR.ml @@ -224,11 +224,13 @@ and expr = | Expr_SignExtend of openParen * intVal * expr * closeParen | Expr_Extract of openParen * intVal * intVal * expr * closeParen | Expr_Concat of openParen * expr list * closeParen - | Expr_FSet of openParen * str * expr * expr * closeParen - | Expr_FAccess of openParen * str * expr * closeParen + | Expr_Ite of expr * expr * expr | Expr_Match of expr * openParen * case list * closeParen | Expr_Cases of openParen * case list * closeParen | Expr_Paren of openParen * expr * closeParen + | Expr_Field of expr * bIdent + | Expr_FieldSet of expr * localIdent * expr + | SortValRec of localIdent * beginRec * fieldAssign list * endRec and lambdaDef = LambdaDef1 of localVarParen list * lambdaSep * expr @@ -253,6 +255,9 @@ and case = CaseCase of expr * expr | CaseDefault of expr +and fieldAssign = + FieldAssign1 of localIdent * expr + and eqOp = EqOp_eq | EqOp_neq diff --git a/lib/fe/BasilIR.cf b/lib/fe/BasilIR.cf index 9948a3b7..69bdd16b 100644 --- a/lib/fe/BasilIR.cf +++ b/lib/fe/BasilIR.cf @@ -273,17 +273,27 @@ Expr_ZeroExtend . Expr2 ::= "zero_extend" OpenParen IntVal "," Expr CloseParen ; Expr_SignExtend . Expr2 ::= "sign_extend" OpenParen IntVal "," Expr CloseParen ; Expr_Extract . Expr2 ::= "extract" OpenParen IntVal "," IntVal "," Expr CloseParen ; Expr_Concat . Expr2 ::= "bvconcat" OpenParen [Expr] CloseParen ; -Expr_FSet . Expr2 ::= "fset" OpenParen Str "," Expr "," Expr CloseParen ; -Expr_FAccess . Expr2 ::= "faccess" OpenParen Str "," Expr CloseParen ; + CaseCase . Case ::= Expr "->" Expr ; CaseDefault . Case ::= "_" "->" Expr ; separator Case "|" ; +Expr_Ite . Expr2 ::= "if" Expr "then" Expr "else" Expr ; Expr_Match . Expr2 ::= "match" Expr "with" OpenParen [Case] CloseParen ; Expr_Cases . Expr2 ::= "cases" OpenParen [Case] CloseParen ; Expr_Paren . Expr2 ::= OpenParen Expr CloseParen ; + +Expr_Field . Expr ::= Expr2 BIdent; +Expr_FieldSet . Expr2 ::= Expr2 "with" LocalIdent "=" Expr ; + +rules FieldAssign ::= LocalIdent "=" Expr ; +separator FieldAssign ";"; + +SortValRec . Expr ::= LocalIdent BeginRec [FieldAssign] EndRec; + + -- operators rules EqOp ::= "eq" | "neq" ; diff --git a/lib/fe/LexBasilIR.mll b/lib/fe/LexBasilIR.mll index c89b95aa..cc8d0109 100644 --- a/lib/fe/LexBasilIR.mll +++ b/lib/fe/LexBasilIR.mll @@ -11,9 +11,9 @@ let symbol_table = Hashtbl.create 10 let _ = List.iter (fun (kwd, tok) -> Hashtbl.add symbol_table kwd tok) [(";", SYMB1);(",", SYMB2);("->", SYMB3);("::", SYMB4);(":", SYMB5);("=", SYMB6);("|", SYMB7);(":=", SYMB8);("mem:=", SYMB9);("_", SYMB10)] -let resword_table = Hashtbl.create 106 +let resword_table = Hashtbl.create 107 let _ = List.iter (fun (kwd, tok) -> Hashtbl.add resword_table kwd tok) - [("shared", KW_shared);("observable", KW_observable);("axiom", KW_axiom);("memory", KW_memory);("var", KW_var);("val", KW_val);("let", KW_let);("prog", KW_prog);("entry", KW_entry);("proc", KW_proc);("and", KW_and);("type", KW_type);("ptr", KW_ptr);("of", KW_of);("le", KW_le);("be", KW_be);("nop", KW_nop);("store", KW_store);("load", KW_load);("call", KW_call);("indirect", KW_indirect);("assume", KW_assume);("guard", KW_guard);("assert", KW_assert);("goto", KW_goto);("unreachable", KW_unreachable);("return", KW_return);("phi", KW_phi);("block", KW_block);("true", KW_true);("false", KW_false);("forall", KW_forall);("exists", KW_exists);("fun", KW_fun);("in", KW_in);("old", KW_old);("boolnot", KW_boolnot);("intneg", KW_intneg);("booltobv1", KW_booltobv1);("gamma", KW_gamma);("classification", KW_classification);("load_be", KW_load_be);("load_le", KW_load_le);("zero_extend", KW_zero_extend);("sign_extend", KW_sign_extend);("extract", KW_extract);("bvconcat", KW_bvconcat);("fset", KW_fset);("faccess", KW_faccess);("match", KW_match);("with", KW_with);("cases", KW_cases);("eq", KW_eq);("neq", KW_neq);("bvnot", KW_bvnot);("bvneg", KW_bvneg);("bvand", KW_bvand);("bvor", KW_bvor);("bvadd", KW_bvadd);("bvmul", KW_bvmul);("bvudiv", KW_bvudiv);("bvurem", KW_bvurem);("bvshl", KW_bvshl);("bvlshr", KW_bvlshr);("bvnand", KW_bvnand);("bvnor", KW_bvnor);("bvxor", KW_bvxor);("bvxnor", KW_bvxnor);("bvcomp", KW_bvcomp);("bvsub", KW_bvsub);("bvsdiv", KW_bvsdiv);("bvsrem", KW_bvsrem);("bvsmod", KW_bvsmod);("bvashr", KW_bvashr);("bvule", KW_bvule);("bvugt", KW_bvugt);("bvuge", KW_bvuge);("bvult", KW_bvult);("bvslt", KW_bvslt);("bvsle", KW_bvsle);("bvsgt", KW_bvsgt);("bvsge", KW_bvsge);("intadd", KW_intadd);("intmul", KW_intmul);("intsub", KW_intsub);("intdiv", KW_intdiv);("intmod", KW_intmod);("intlt", KW_intlt);("intle", KW_intle);("intgt", KW_intgt);("intge", KW_intge);("booland", KW_booland);("boolor", KW_boolor);("boolimplies", KW_boolimplies);("ptradd", KW_ptradd);("require", KW_require);("requires", KW_requires);("ensure", KW_ensure);("ensures", KW_ensures);("rely", KW_rely);("relies", KW_relies);("guarantee", KW_guarantee);("guarantees", KW_guarantees);("captures", KW_captures);("modifies", KW_modifies);("invariant", KW_invariant)] + [("shared", KW_shared);("observable", KW_observable);("axiom", KW_axiom);("memory", KW_memory);("var", KW_var);("val", KW_val);("let", KW_let);("prog", KW_prog);("entry", KW_entry);("proc", KW_proc);("and", KW_and);("type", KW_type);("ptr", KW_ptr);("of", KW_of);("le", KW_le);("be", KW_be);("nop", KW_nop);("store", KW_store);("load", KW_load);("call", KW_call);("indirect", KW_indirect);("assume", KW_assume);("guard", KW_guard);("assert", KW_assert);("goto", KW_goto);("unreachable", KW_unreachable);("return", KW_return);("phi", KW_phi);("block", KW_block);("true", KW_true);("false", KW_false);("forall", KW_forall);("exists", KW_exists);("fun", KW_fun);("in", KW_in);("old", KW_old);("boolnot", KW_boolnot);("intneg", KW_intneg);("booltobv1", KW_booltobv1);("gamma", KW_gamma);("classification", KW_classification);("load_be", KW_load_be);("load_le", KW_load_le);("zero_extend", KW_zero_extend);("sign_extend", KW_sign_extend);("extract", KW_extract);("bvconcat", KW_bvconcat);("if", KW_if);("then", KW_then);("else", KW_else);("match", KW_match);("with", KW_with);("cases", KW_cases);("eq", KW_eq);("neq", KW_neq);("bvnot", KW_bvnot);("bvneg", KW_bvneg);("bvand", KW_bvand);("bvor", KW_bvor);("bvadd", KW_bvadd);("bvmul", KW_bvmul);("bvudiv", KW_bvudiv);("bvurem", KW_bvurem);("bvshl", KW_bvshl);("bvlshr", KW_bvlshr);("bvnand", KW_bvnand);("bvnor", KW_bvnor);("bvxor", KW_bvxor);("bvxnor", KW_bvxnor);("bvcomp", KW_bvcomp);("bvsub", KW_bvsub);("bvsdiv", KW_bvsdiv);("bvsrem", KW_bvsrem);("bvsmod", KW_bvsmod);("bvashr", KW_bvashr);("bvule", KW_bvule);("bvugt", KW_bvugt);("bvuge", KW_bvuge);("bvult", KW_bvult);("bvslt", KW_bvslt);("bvsle", KW_bvsle);("bvsgt", KW_bvsgt);("bvsge", KW_bvsge);("intadd", KW_intadd);("intmul", KW_intmul);("intsub", KW_intsub);("intdiv", KW_intdiv);("intmod", KW_intmod);("intlt", KW_intlt);("intle", KW_intle);("intgt", KW_intgt);("intge", KW_intge);("booland", KW_booland);("boolor", KW_boolor);("boolimplies", KW_boolimplies);("ptradd", KW_ptradd);("require", KW_require);("requires", KW_requires);("ensure", KW_ensure);("ensures", KW_ensures);("rely", KW_rely);("relies", KW_relies);("guarantee", KW_guarantee);("guarantees", KW_guarantees);("captures", KW_captures);("modifies", KW_modifies);("invariant", KW_invariant)] let unescapeInitTail (s:string) : string = let rec unesc s = match s with diff --git a/lib/fe/ParBasilIR.mly b/lib/fe/ParBasilIR.mly index 106b75f2..6ad4658a 100644 --- a/lib/fe/ParBasilIR.mly +++ b/lib/fe/ParBasilIR.mly @@ -7,7 +7,7 @@ open AbsBasilIR open Lexing %} -%token KW_shared KW_observable KW_axiom KW_memory KW_var KW_val KW_let KW_prog KW_entry KW_proc KW_and KW_type KW_ptr KW_of KW_le KW_be KW_nop KW_store KW_load KW_call KW_indirect KW_assume KW_guard KW_assert KW_goto KW_unreachable KW_return KW_phi KW_block KW_true KW_false KW_forall KW_exists KW_fun KW_in KW_old KW_boolnot KW_intneg KW_booltobv1 KW_gamma KW_classification KW_load_be KW_load_le KW_zero_extend KW_sign_extend KW_extract KW_bvconcat KW_fset KW_faccess KW_match KW_with KW_cases KW_eq KW_neq KW_bvnot KW_bvneg KW_bvand KW_bvor KW_bvadd KW_bvmul KW_bvudiv KW_bvurem KW_bvshl KW_bvlshr KW_bvnand KW_bvnor KW_bvxor KW_bvxnor KW_bvcomp KW_bvsub KW_bvsdiv KW_bvsrem KW_bvsmod KW_bvashr KW_bvule KW_bvugt KW_bvuge KW_bvult KW_bvslt KW_bvsle KW_bvsgt KW_bvsge KW_intadd KW_intmul KW_intsub KW_intdiv KW_intmod KW_intlt KW_intle KW_intgt KW_intge KW_booland KW_boolor KW_boolimplies KW_ptradd KW_require KW_requires KW_ensure KW_ensures KW_rely KW_relies KW_guarantee KW_guarantees KW_captures KW_modifies KW_invariant +%token KW_shared KW_observable KW_axiom KW_memory KW_var KW_val KW_let KW_prog KW_entry KW_proc KW_and KW_type KW_ptr KW_of KW_le KW_be KW_nop KW_store KW_load KW_call KW_indirect KW_assume KW_guard KW_assert KW_goto KW_unreachable KW_return KW_phi KW_block KW_true KW_false KW_forall KW_exists KW_fun KW_in KW_old KW_boolnot KW_intneg KW_booltobv1 KW_gamma KW_classification KW_load_be KW_load_le KW_zero_extend KW_sign_extend KW_extract KW_bvconcat KW_if KW_then KW_else KW_match KW_with KW_cases KW_eq KW_neq KW_bvnot KW_bvneg KW_bvand KW_bvor KW_bvadd KW_bvmul KW_bvudiv KW_bvurem KW_bvshl KW_bvlshr KW_bvnand KW_bvnor KW_bvxor KW_bvxnor KW_bvcomp KW_bvsub KW_bvsdiv KW_bvsrem KW_bvsmod KW_bvashr KW_bvule KW_bvugt KW_bvuge KW_bvult KW_bvslt KW_bvsle KW_bvsgt KW_bvsge KW_intadd KW_intmul KW_intsub KW_intdiv KW_intmod KW_intlt KW_intle KW_intgt KW_intge KW_booland KW_boolor KW_boolimplies KW_ptradd KW_require KW_requires KW_ensure KW_ensures KW_rely KW_relies KW_guarantee KW_guarantees KW_captures KW_modifies KW_invariant %token SYMB1 /* ; */ %token SYMB2 /* , */ @@ -45,7 +45,7 @@ open Lexing %token <(int * int) * string> TOK_IntegerHex %token <(int * int) * string> TOK_IntegerDec -%start pModuleT pDecl_list pBlockIdent_list pLambdaSep pVarModifiers pVarModifiers_list pDecl pTypeT_list pTypeAssign pTypeAssign_list pProcDef pField_list pField pIntType pBoolType pRecordType pPointerType pBVType pMapType pRecordField pRecordField_list pSumCase pSumCase_list pType1 pTypeT pIntVal pBVVal pFieldVal_list pFieldVal pEndian pAssignment pStmt pAssignment_list pLocalVar pLocalVar_list pGlobalVar pGlobalVar_list pVar pLocalVarParen pGlobalVarParen pLocalVarParen_list pNamedCallReturn pNamedCallReturn_list pLVars pNamedCallArg pNamedCallArg_list pCallParams pJump pLVar pLVar_list pBlock_list pStmtWithAttrib pStmtWithAttrib_list pJumpWithAttrib pPhiExpr pPhiExpr_list pPhiAssign pPhiAssign_list pBlock pAttrKeyValue pAttrKeyValue_list pAttribSet pAttr_list pAttr pParams pParams_list pValue pExpr_list pExpr pExpr1 pExpr2 pLambdaDef pBinOp pUnOp pCase pCase_list pEqOp pBVUnOp pBVBinOp pBVLogicalBinOp pIntBinOp pIntLogicalBinOp pBoolBinOp pPointerBinOp pRequireTok pEnsureTok pRelyTok pGuarTok pFunSpec pVarSpec pProgSpec pFunSpec_list pProgSpec_list +%start pModuleT pDecl_list pBlockIdent_list pLambdaSep pVarModifiers pVarModifiers_list pDecl pTypeT_list pTypeAssign pTypeAssign_list pProcDef pField_list pField pIntType pBoolType pRecordType pPointerType pBVType pMapType pRecordField pRecordField_list pSumCase pSumCase_list pType1 pTypeT pIntVal pBVVal pFieldVal_list pFieldVal pEndian pAssignment pStmt pAssignment_list pLocalVar pLocalVar_list pGlobalVar pGlobalVar_list pVar pLocalVarParen pGlobalVarParen pLocalVarParen_list pNamedCallReturn pNamedCallReturn_list pLVars pNamedCallArg pNamedCallArg_list pCallParams pJump pLVar pLVar_list pBlock_list pStmtWithAttrib pStmtWithAttrib_list pJumpWithAttrib pPhiExpr pPhiExpr_list pPhiAssign pPhiAssign_list pBlock pAttrKeyValue pAttrKeyValue_list pAttribSet pAttr_list pAttr pParams pParams_list pValue pExpr_list pExpr pExpr1 pExpr2 pLambdaDef pBinOp pUnOp pCase pCase_list pFieldAssign pFieldAssign_list pEqOp pBVUnOp pBVBinOp pBVLogicalBinOp pIntBinOp pIntLogicalBinOp pBoolBinOp pPointerBinOp pRequireTok pEnsureTok pRelyTok pGuarTok pFunSpec pVarSpec pProgSpec pFunSpec_list pProgSpec_list %type pModuleT %type pDecl_list %type pBlockIdent_list @@ -122,6 +122,8 @@ open Lexing %type pUnOp %type pCase %type pCase_list +%type pFieldAssign +%type pFieldAssign_list %type pEqOp %type pBVUnOp %type pBVBinOp @@ -216,6 +218,8 @@ open Lexing %type unOp %type case %type case_list +%type fieldAssign +%type fieldAssign_list %type eqOp %type bVUnOp %type bVBinOp @@ -407,6 +411,10 @@ pCase : case TOK_EOF { $1 }; pCase_list : case_list TOK_EOF { $1 }; +pFieldAssign : fieldAssign TOK_EOF { $1 }; + +pFieldAssign_list : fieldAssign_list TOK_EOF { $1 }; + pEqOp : eqOp TOK_EOF { $1 }; pBVUnOp : bVUnOp TOK_EOF { $1 }; @@ -746,6 +754,8 @@ expr : expr1 { $1 } | KW_exists attribSet lambdaDef { Expr_Exists ($2, $3) } | KW_fun attribSet lambdaDef { Expr_Lambda ($2, $3) } | KW_let localIdent localVarParen_list SYMB5 typeT SYMB6 expr KW_in expr { Expr_Let ($2, $3, $5, $7, $9) } + | expr2 bIdent { Expr_Field ($1, $2) } + | localIdent beginRec fieldAssign_list endRec { SortValRec ($1, $2, $3, $4) } ; expr1 : expr2 { $1 } @@ -765,11 +775,11 @@ expr2 : value { Expr_Literal $1 } | KW_sign_extend openParen intVal SYMB2 expr closeParen { Expr_SignExtend ($2, $3, $5, $6) } | KW_extract openParen intVal SYMB2 intVal SYMB2 expr closeParen { Expr_Extract ($2, $3, $5, $7, $8) } | KW_bvconcat openParen expr_list closeParen { Expr_Concat ($2, $3, $4) } - | KW_fset openParen str SYMB2 expr SYMB2 expr closeParen { Expr_FSet ($2, $3, $5, $7, $8) } - | KW_faccess openParen str SYMB2 expr closeParen { Expr_FAccess ($2, $3, $5, $6) } + | KW_if expr KW_then expr KW_else expr { Expr_Ite ($2, $4, $6) } | KW_match expr KW_with openParen case_list closeParen { Expr_Match ($2, $4, $5, $6) } | KW_cases openParen case_list closeParen { Expr_Cases ($2, $3, $4) } | openParen expr closeParen { Expr_Paren ($1, $2, $3) } + | expr2 KW_with localIdent SYMB6 expr { Expr_FieldSet ($1, $3, $5) } ; lambdaDef : localVarParen_list lambdaSep expr { LambdaDef1 ($1, $2, $3) } @@ -800,6 +810,14 @@ case_list : /* empty */ { [] } | case SYMB7 case_list { (fun (x,xs) -> x::xs) ($1, $3) } ; +fieldAssign : localIdent SYMB6 expr { FieldAssign1 ($1, $3) } + ; + +fieldAssign_list : /* empty */ { [] } + | fieldAssign { (fun x -> [x]) $1 } + | fieldAssign SYMB1 fieldAssign_list { (fun (x,xs) -> x::xs) ($1, $3) } + ; + eqOp : KW_eq { EqOp_eq } | KW_neq { EqOp_neq } ; diff --git a/lib/fe/PrintBasilIR.ml b/lib/fe/PrintBasilIR.ml index 87f350dc..d0becc9a 100644 --- a/lib/fe/PrintBasilIR.ml +++ b/lib/fe/PrintBasilIR.ml @@ -451,11 +451,13 @@ and prtExpr (i:int) (e : AbsBasilIR.expr) : doc = match e with | AbsBasilIR.Expr_SignExtend (openparen, intval, expr, closeparen) -> prPrec i 2 (concatD [render "sign_extend" ; prtOpenParen 0 openparen ; prtIntVal 0 intval ; render "," ; prtExpr 0 expr ; prtCloseParen 0 closeparen]) | AbsBasilIR.Expr_Extract (openparen, intval1, intval2, expr, closeparen) -> prPrec i 2 (concatD [render "extract" ; prtOpenParen 0 openparen ; prtIntVal 0 intval1 ; render "," ; prtIntVal 0 intval2 ; render "," ; prtExpr 0 expr ; prtCloseParen 0 closeparen]) | AbsBasilIR.Expr_Concat (openparen, exprs, closeparen) -> prPrec i 2 (concatD [render "bvconcat" ; prtOpenParen 0 openparen ; prtExprListBNFC 0 exprs ; prtCloseParen 0 closeparen]) - | AbsBasilIR.Expr_FSet (openparen, str, expr1, expr2, closeparen) -> prPrec i 2 (concatD [render "fset" ; prtOpenParen 0 openparen ; prtStr 0 str ; render "," ; prtExpr 0 expr1 ; render "," ; prtExpr 0 expr2 ; prtCloseParen 0 closeparen]) - | AbsBasilIR.Expr_FAccess (openparen, str, expr, closeparen) -> prPrec i 2 (concatD [render "faccess" ; prtOpenParen 0 openparen ; prtStr 0 str ; render "," ; prtExpr 0 expr ; prtCloseParen 0 closeparen]) + | AbsBasilIR.Expr_Ite (expr1, expr2, expr3) -> prPrec i 2 (concatD [render "if" ; prtExpr 0 expr1 ; render "then" ; prtExpr 0 expr2 ; render "else" ; prtExpr 0 expr3]) | AbsBasilIR.Expr_Match (expr, openparen, cases, closeparen) -> prPrec i 2 (concatD [render "match" ; prtExpr 0 expr ; render "with" ; prtOpenParen 0 openparen ; prtCaseListBNFC 0 cases ; prtCloseParen 0 closeparen]) | AbsBasilIR.Expr_Cases (openparen, cases, closeparen) -> prPrec i 2 (concatD [render "cases" ; prtOpenParen 0 openparen ; prtCaseListBNFC 0 cases ; prtCloseParen 0 closeparen]) | AbsBasilIR.Expr_Paren (openparen, expr, closeparen) -> prPrec i 2 (concatD [prtOpenParen 0 openparen ; prtExpr 0 expr ; prtCloseParen 0 closeparen]) + | AbsBasilIR.Expr_Field (expr, bident) -> prPrec i 0 (concatD [prtExpr 2 expr ; prtBIdent 0 bident]) + | AbsBasilIR.Expr_FieldSet (expr1, localident, expr2) -> prPrec i 2 (concatD [prtExpr 2 expr1 ; render "with" ; prtLocalIdent 0 localident ; render "=" ; prtExpr 0 expr2]) + | AbsBasilIR.SortValRec (localident, beginrec, fieldassigns, endrec) -> prPrec i 0 (concatD [prtLocalIdent 0 localident ; prtBeginRec 0 beginrec ; prtFieldAssignListBNFC 0 fieldassigns ; prtEndRec 0 endrec]) and prtExprListBNFC i es : doc = match (i, es) with (_,[]) -> (concatD []) @@ -491,6 +493,13 @@ and prtCaseListBNFC i es : doc = match (i, es) with (_,[]) -> (concatD []) | (_,[x]) -> (concatD [prtCase 0 x]) | (_,x::xs) -> (concatD [prtCase 0 x ; render "|" ; prtCaseListBNFC 0 xs]) +and prtFieldAssign (i:int) (e : AbsBasilIR.fieldAssign) : doc = match e with + AbsBasilIR.FieldAssign1 (localident, expr) -> prPrec i 0 (concatD [prtLocalIdent 0 localident ; render "=" ; prtExpr 0 expr]) + +and prtFieldAssignListBNFC i es : doc = match (i, es) with + (_,[]) -> (concatD []) + | (_,[x]) -> (concatD [prtFieldAssign 0 x]) + | (_,x::xs) -> (concatD [prtFieldAssign 0 x ; render ";" ; prtFieldAssignListBNFC 0 xs]) and prtEqOp (i:int) (e : AbsBasilIR.eqOp) : doc = match e with AbsBasilIR.EqOp_eq -> prPrec i 0 (concatD [render "eq"]) | AbsBasilIR.EqOp_neq -> prPrec i 0 (concatD [render "neq"]) diff --git a/lib/fe/ShowBasilIR.ml b/lib/fe/ShowBasilIR.ml index afd2600c..db2e793e 100644 --- a/lib/fe/ShowBasilIR.ml +++ b/lib/fe/ShowBasilIR.ml @@ -306,11 +306,13 @@ and showExpr (e : AbsBasilIR.expr) : showable = match e with | AbsBasilIR.Expr_SignExtend (openparen, intval, expr, closeparen) -> s2s "Expr_SignExtend" >> c2s ' ' >> c2s '(' >> showOpenParen openparen >> s2s ", " >> showIntVal intval >> s2s ", " >> showExpr expr >> s2s ", " >> showCloseParen closeparen >> c2s ')' | AbsBasilIR.Expr_Extract (openparen, intval0, intval, expr, closeparen) -> s2s "Expr_Extract" >> c2s ' ' >> c2s '(' >> showOpenParen openparen >> s2s ", " >> showIntVal intval0 >> s2s ", " >> showIntVal intval >> s2s ", " >> showExpr expr >> s2s ", " >> showCloseParen closeparen >> c2s ')' | AbsBasilIR.Expr_Concat (openparen, exprs, closeparen) -> s2s "Expr_Concat" >> c2s ' ' >> c2s '(' >> showOpenParen openparen >> s2s ", " >> showList showExpr exprs >> s2s ", " >> showCloseParen closeparen >> c2s ')' - | AbsBasilIR.Expr_FSet (openparen, str, expr0, expr, closeparen) -> s2s "Expr_FSet" >> c2s ' ' >> c2s '(' >> showOpenParen openparen >> s2s ", " >> showStr str >> s2s ", " >> showExpr expr0 >> s2s ", " >> showExpr expr >> s2s ", " >> showCloseParen closeparen >> c2s ')' - | AbsBasilIR.Expr_FAccess (openparen, str, expr, closeparen) -> s2s "Expr_FAccess" >> c2s ' ' >> c2s '(' >> showOpenParen openparen >> s2s ", " >> showStr str >> s2s ", " >> showExpr expr >> s2s ", " >> showCloseParen closeparen >> c2s ')' + | AbsBasilIR.Expr_Ite (expr0, expr1, expr) -> s2s "Expr_Ite" >> c2s ' ' >> c2s '(' >> showExpr expr0 >> s2s ", " >> showExpr expr1 >> s2s ", " >> showExpr expr >> c2s ')' | AbsBasilIR.Expr_Match (expr, openparen, cases, closeparen) -> s2s "Expr_Match" >> c2s ' ' >> c2s '(' >> showExpr expr >> s2s ", " >> showOpenParen openparen >> s2s ", " >> showList showCase cases >> s2s ", " >> showCloseParen closeparen >> c2s ')' | AbsBasilIR.Expr_Cases (openparen, cases, closeparen) -> s2s "Expr_Cases" >> c2s ' ' >> c2s '(' >> showOpenParen openparen >> s2s ", " >> showList showCase cases >> s2s ", " >> showCloseParen closeparen >> c2s ')' | AbsBasilIR.Expr_Paren (openparen, expr, closeparen) -> s2s "Expr_Paren" >> c2s ' ' >> c2s '(' >> showOpenParen openparen >> s2s ", " >> showExpr expr >> s2s ", " >> showCloseParen closeparen >> c2s ')' + | AbsBasilIR.Expr_Field (expr, bident) -> s2s "Expr_Field" >> c2s ' ' >> c2s '(' >> showExpr expr >> s2s ", " >> showBIdent bident >> c2s ')' + | AbsBasilIR.Expr_FieldSet (expr0, localident, expr) -> s2s "Expr_FieldSet" >> c2s ' ' >> c2s '(' >> showExpr expr0 >> s2s ", " >> showLocalIdent localident >> s2s ", " >> showExpr expr >> c2s ')' + | AbsBasilIR.SortValRec (localident, beginrec, fieldassigns, endrec) -> s2s "SortValRec" >> c2s ' ' >> c2s '(' >> showLocalIdent localident >> s2s ", " >> showBeginRec beginrec >> s2s ", " >> showList showFieldAssign fieldassigns >> s2s ", " >> showEndRec endrec >> c2s ')' and showLambdaDef (e : AbsBasilIR.lambdaDef) : showable = match e with @@ -340,6 +342,10 @@ and showCase (e : AbsBasilIR.case) : showable = match e with | AbsBasilIR.CaseDefault expr -> s2s "CaseDefault" >> c2s ' ' >> c2s '(' >> showExpr expr >> c2s ')' +and showFieldAssign (e : AbsBasilIR.fieldAssign) : showable = match e with + AbsBasilIR.FieldAssign1 (localident, expr) -> s2s "FieldAssign1" >> c2s ' ' >> c2s '(' >> showLocalIdent localident >> s2s ", " >> showExpr expr >> c2s ')' + + and showEqOp (e : AbsBasilIR.eqOp) : showable = match e with AbsBasilIR.EqOp_eq -> s2s "EqOp_eq" | AbsBasilIR.EqOp_neq -> s2s "EqOp_neq" diff --git a/lib/fe/SkelBasilIR.ml b/lib/fe/SkelBasilIR.ml index 08033556..eff2aca7 100644 --- a/lib/fe/SkelBasilIR.ml +++ b/lib/fe/SkelBasilIR.ml @@ -329,11 +329,13 @@ and transExpr (x : expr) : result = match x with | Expr_SignExtend (openparen, intval, expr, closeparen) -> failure x | Expr_Extract (openparen, intval0, intval, expr, closeparen) -> failure x | Expr_Concat (openparen, exprs, closeparen) -> failure x - | Expr_FSet (openparen, str, expr0, expr, closeparen) -> failure x - | Expr_FAccess (openparen, str, expr, closeparen) -> failure x + | Expr_Ite (expr0, expr1, expr) -> failure x | Expr_Match (expr, openparen, cases, closeparen) -> failure x | Expr_Cases (openparen, cases, closeparen) -> failure x | Expr_Paren (openparen, expr, closeparen) -> failure x + | Expr_Field (expr, bident) -> failure x + | Expr_FieldSet (expr0, localident, expr) -> failure x + | SortValRec (localident, beginrec, fieldassigns, endrec) -> failure x and transLambdaDef (x : lambdaDef) : result = match x with @@ -363,6 +365,10 @@ and transCase (x : case) : result = match x with | CaseDefault expr -> failure x +and transFieldAssign (x : fieldAssign) : result = match x with + FieldAssign1 (localident, expr) -> failure x + + and transEqOp (x : eqOp) : result = match x with EqOp_eq -> failure x | EqOp_neq -> failure x diff --git a/lib/lang/algsimp.ml b/lib/lang/algsimp.ml index 41848f81..bf540db9 100644 --- a/lib/lang/algsimp.ml +++ b/lib/lang/algsimp.ml @@ -292,6 +292,6 @@ let%expect_test "normalise" = print_endline (BasilExpr.to_string e); [%expect {| - boolnot(boolnot(boolnot(booland(boolnot(boolnot(b:bool)), a:bool)))) - boolor(boolnot(b:bool), boolnot(a:bool)) + boolnot(boolnot(boolnot(booland(boolnot(boolnot(b)), a)))) + boolor(boolnot(b), boolnot(a)) |}] diff --git a/lib/lang/expr.ml b/lib/lang/expr.ml index 0e68f255..faae1161 100644 --- a/lib/lang/expr.ml +++ b/lib/lang/expr.ml @@ -469,13 +469,13 @@ module BasilExpr = struct let _, rtype = Types.uncurry (Var.typ name) in text (Var.name name) ^+ binding ^+ text ":" - ^+ text (Types.to_string rtype) + ^+ text (Types.to_string_rexp rtype) ^+ text "=" ^+ bracket "(" in_body ")" | name, { this = Some e } -> let rtype = Var.typ name in text (Var.name name) ^+ attrib ^+ text ":" - ^+ text (Types.to_string rtype) + ^+ text (Types.to_string_rexp rtype) ^+ text "=" ^ bracket "(" e ")" | _ -> failwith "undefined ") in @@ -510,7 +510,7 @@ module BasilExpr = struct return (text op ^ a ^ text " " ^ binding) | Lambda { bound_vars; in_body; attrib } -> pass () | Let { bound_vars; in_body; attrib } -> pass () - | RVar { id; attrib } -> return (text (Var.to_string id) ^ a) + | RVar { id; attrib } -> return (text (Var.name id) ^ a) | Constant { const } -> return (text (AllOps.to_string const) ^ a) | UnaryExpr { op = `ZeroExtend bits; arg = { this = Some arg } } -> return @@ -526,24 +526,15 @@ module BasilExpr = struct return (fill nil [ text "extract" ^ a ^ textpf "(%d,%d, " hi lo ^ e ^ text ")" ]) - | UnaryExpr { op = `FACCESS offset; arg = { this = Some arg } } -> - return - (fill - (text "," ^ newline) - [ text "faccess" ^ a ^ (textpf "(\"%s\"") offset; arg ^ text ")" ]) + | UnaryExpr { op = `ReadField field; arg = { this = Some arg } } -> + return (arg ^ text "." ^ text field) | BinaryExpr { - op = `FSET offset; - arg1 = { this = Some arg1 }; - arg2 = { this = Some arg2 }; + op = `WriteField field; + arg1 = { this = Some r }; + arg2 = { this = Some vl }; } -> - return - (fill - (text "," ^ newline) - [ - text "fset" ^ a ^ (textpf "(\"%s\"") offset; - arg1 ^ text ", " ^ arg2 ^ text ")"; - ]) + return @@ bracket "(" (r ^ text "." ^ text field ^+ text "<-" ^+ vl) ")" | UnaryExpr { op; arg = { this = Some e } } -> return (text (AllOps.to_string op) ^ a ^ bracket "(" e ")") | BinaryExpr @@ -570,6 +561,25 @@ module BasilExpr = struct ^ a ^ bracket "(" (fill (text "," ^ newline) [ e; e2 ]) ")"; ]) + | ApplyIntrin + { + op = `Cases; + args = + [ + { + inner = + Some + (BinaryExpr + { + op = `IfThen; + arg1 = { this = Some cond }; + arg2 = { this = Some thn }; + }); + }; + { this = Some els }; + ]; + } -> + return (text "if" ^+ cond ^+ text "then" ^+ thn ^+ text "else" ^+ els) | ApplyIntrin { op; args = es } when List.for_all FoldN.is_def es -> return (fill nil @@ -748,11 +758,11 @@ module BasilExpr = struct let zero_extend ?attrib ~n_prefix_bits (e : t) : t = unexp ?attrib ~op:(`ZeroExtend n_prefix_bits) e - let fset ?attrib ~(offset : string) (record : t) (e : t) : t = - binexp ?attrib ~op:(`FSET offset) record e + let field_store ?attrib ~(field : string) (record : t) (e : t) : t = + binexp ?attrib ~op:(`WriteField field) record e - let faccess ?attrib ~(offset : string) (record : t) : t = - unexp ?attrib ~op:(`FACCESS offset) record + let field_read ?attrib ~(field : string) (record : t) : t = + unexp ?attrib ~op:(`ReadField field) record let sign_extend ?attrib ~n_prefix_bits (e : t) : t = unexp ?attrib ~op:(`SignExtend n_prefix_bits) e @@ -766,6 +776,9 @@ module BasilExpr = struct let concat ?attrib (e : t) (f : t) : t = applyintrin ?attrib ~op:`BVConcat [ e; f ] + let ifthenelse ?attrib cond t e = + applyintrin ~op:`Cases [ binexp ~op:`IfThen cond t; e ] + let concatl ?attrib (e : t list) : t = applyintrin ?attrib ~op:`BVConcat e let forall ?attrib ~bound p = binding ?attrib ~op:`Forall bound p let exists ?attrib ~bound p = binding ?attrib ~op:`Exists bound p diff --git a/lib/lang/expr_eval.ml b/lib/lang/expr_eval.ml index 3f862d55..ea057d55 100644 --- a/lib/lang/expr_eval.ml +++ b/lib/lang/expr_eval.ml @@ -37,11 +37,11 @@ let eval_expr_alg (e : Ops.AllOps.const option BasilExpr.abstract_expr) = get_bv b >|= BVOps.eval_unary_unif op >|= bv | UnaryExpr { op = #BVOps.unary_bool as op; arg = b } -> get_bool b >|= BVOps.eval_unary_bool op >|= bv - | BinaryExpr { op = `FSET offset; arg1 = a; arg2 = b } -> + | BinaryExpr { op = `WriteField offset; arg1 = a; arg2 = b } -> let* a = get_record a in let* b = get_bv b in record (Record.set_field offset a b) - | UnaryExpr { op = `FACCESS offset; arg = a } -> + | UnaryExpr { op = `ReadField offset; arg = a } -> let* a = get_record a in let { value; _ } : Record.field = Record.get_field offset a in Some (bv value) @@ -128,6 +128,6 @@ let%expect_test _ = print_endline r; [%expect {| - bvmul(bvadd(0xa:bv10, 0xa:bv10), beans:bv10) - bvmul(0x14:bv10, beans:bv10) + bvmul(bvadd(0xa:bv10, 0xa:bv10), beans) + bvmul(0x14:bv10, beans) |}] diff --git a/lib/lang/expr_smt.ml b/lib/lang/expr_smt.ml index d952534c..90da5ddc 100644 --- a/lib/lang/expr_smt.ml +++ b/lib/lang/expr_smt.ml @@ -110,7 +110,7 @@ module SMTLib2 = struct let log = LSet.union (LSet.singleton Array) (LSet.union ll lr) in (list [ atom "Array"; tl; tr ], log) | Types.Variable v -> (atom v, LSet.empty) - | Types.Record e -> + | Types.Struct e -> failwith "unsupported: must be lowered to Sort/ADT/Datatype first" | Types.Pointer { upper; lower } -> ( list [ atom "Pointer "; fst (of_typ upper); fst (of_typ lower) ], diff --git a/lib/lang/ops.ml b/lib/lang/ops.ml index 82e76927..77398257 100644 --- a/lib/lang/ops.ml +++ b/lib/lang/ops.ml @@ -221,24 +221,60 @@ module IntOps = struct | #binary as b -> show_binary b end +module ADTOps = struct + (* open recursive variant value *) + type 'a t = { name : string; fields : (string * 'a) list; ptype : Types.t } + [@@deriving eq, ord, show] + + let get_typ { ptype } = ptype + + let to_string f { name; fields } = + name ^ " {" + ^ (fields |> List.map (fun (k, v) -> k ^ "=" ^ f v) |> String.concat "; ") + ^ "}" + + let get_field { fields } n = List.find (fst %> String.equal n) fields + + let set_field n r nv = + { + r with + fields = + List.map + (fun (k, v) -> if String.equal n k then (k, v) else (k, nv)) + r.fields; + } + + type unary = [ `ReadField of string ] + [@@deriving show { with_path = false }, eq, ord] + + type binary = [ `WriteField of string ] + [@@deriving show { with_path = false }, eq, ord] + + let eval_unary (u : unary) record = + match u with `ReadField field -> get_field record field + + let eval_binary (u : binary) = + match u with `WriteField field -> set_field field +end + module RecordOps = struct type const = [ `Record of Record.t ] [@@deriving show { with_path = false }, eq, ord] - type unary = [ `FACCESS of string ] + type unary = [ `ReadField of string ] [@@deriving show { with_path = false }, eq, ord] - type binary = [ `FSET of string ] + type binary = [ `WriteField of string ] [@@deriving show { with_path = false }, eq, ord] let eval_unary (u : unary) record = match u with - | `FACCESS offset -> + | `ReadField offset -> let { value; _ } : Record.field = Record.get_field offset record in value let eval_binary (u : binary) = - match u with `FSET offset -> Record.set_field offset + match u with `WriteField offset -> Record.set_field offset let show = function | #unary as u -> show_unary u @@ -281,14 +317,17 @@ module Spec = struct end module AllOps = struct - type const = - [ IntOps.const - | BVOps.const - | LogicalOps.const - | RecordOps.const - | PointerOps.const ] + type prim_const = + [ IntOps.const | BVOps.const | LogicalOps.const | PointerOps.const ] [@@deriving show { with_path = false }, eq, ord] + type const = [ prim_const | RecordOps.const | `Sort of const ADTOps.t ] + [@@deriving show { with_path = false }, eq, ord] + + module ADT = struct + type 'a t = { name : string; fields : string * 'a } + end + type unary = [ IntOps.unary | BVOps.unary @@ -326,6 +365,7 @@ module AllOps = struct | `Bitvector v -> return (Bitvector (Bitvec.size v)) | `Pointer (v, ty) -> return (Pointer ty) | `Record ((fields, typ) : Record.t) -> return typ + | `Sort s -> return (ADTOps.get_typ s) let ret_type_lambda (o : [< lambda ]) args a = let open Types in @@ -347,9 +387,16 @@ module AllOps = struct match a with | Bitvector s -> return @@ Bitvector (sz + s) | o -> Conflict [ (o, " - let { typ; _ } = get_field offset a in - return typ + | `ReadField field -> ( + match a with + | Sort _ -> + return + @@ Option.get_exn_or "no such field" + @@ adt_record_field field a + | Struct _ -> + let { typ } = struct_field field a in + return typ + | _ -> failwith "not a struct") | `BVNEG -> return a | `INTNEG -> return Integer | `Old -> return a @@ -377,7 +424,7 @@ module AllOps = struct | `BVAND | `BVOR | `BVADD | `BVMUL | `BVUDIV | `BVUREM | `BVSHL | `BVLSHR | `BVNAND | `BVXOR | `BVSUB | `BVSDIV | `BVSREM | `BVSMOD | `BVASHR -> return l - | `FSET _ -> return r + | `WriteField _ -> return l | `PTRADD -> return l | `MapAccess -> let m, r = Types.uncurry l in @@ -417,8 +464,9 @@ module AllOps = struct (** ops returning booleans *) - let to_string (op : [< const | unary | binary | intrin | lambda ]) = + let rec to_string (op : [< const | unary | binary | intrin | lambda ]) = match op with + | `Sort v -> ADTOps.to_string to_string v | `BVADD -> "bvadd" | `BVSREM -> "bvsrem" | `BVSDIV -> "bvsdiv" @@ -438,8 +486,8 @@ module AllOps = struct | `Exists -> "exists" | `SignExtend n -> Printf.sprintf "sign_extend_%d" n | `ZeroExtend n -> Printf.sprintf "zero_extend_%d" n - | `FSET offset -> Printf.sprintf "fset_%s" offset - | `FACCESS offset -> Printf.sprintf "asdfaccess_%s" offset + | `WriteField offset -> "write_field_" ^ offset + | `ReadField offset -> "read_field_" ^ offset | `PTRADD -> "ptradd" | `EQ -> "eq" | `INTADD -> "intadd" diff --git a/lib/lang/program.ml b/lib/lang/program.ml index 58e724d0..7cc0edf5 100644 --- a/lib/lang/program.ml +++ b/lib/lang/program.ml @@ -28,6 +28,13 @@ let pp_stmt fmt s = Format.pp_print_string fmt (show_stmt s) type prog_spec = { rely : BasilExpr.t list; guarantee : BasilExpr.t list } type func_type = Axiom of e | Uninterpreted | Function of e +type implicit_declaration = + | VariantCase of { + variant : string; + belongs_to : Types.t; + constructor : Var.t; (* function to construct a value of this case *) + } + type declaration = | Type of { binding : string; typ : Types.t } | Function of { @@ -82,6 +89,7 @@ let pretty_declaration d = type t = { modulename : string; globals : declaration StringMap.t; + implicit_decls : implicit_declaration StringMap.t; entry_proc : ID.t option; procs : proc IDMap.t; proc_names : ID.generator; @@ -145,6 +153,37 @@ let decl_global ?(attrib = StringMap.empty) p v = let decl = Variable { binding = v; attrib } in { p with globals = StringMap.add (Var.name v) decl p.globals } +let decl_typ ?(attrib = StringMap.empty) p t = + match t with + | Sort (name, []) as s -> + { + p with + globals = + StringMap.add name (Type { binding = name; typ = s }) p.globals; + implicit_decls = + StringMap.add name + (let ty = Types.curry [] s in + let constructor = Var.create name ty ~scope:Global in + VariantCase { variant = name; belongs_to = s; constructor }) + p.implicit_decls; + } + | Sort (name, variants) as s -> + { + p with + globals = + StringMap.add name (Type { binding = name; typ = s }) p.globals; + implicit_decls = + StringMap.add_list p.implicit_decls + (variants + |> List.map (function { variant; fields } -> + let args = List.map (function { field; typ } -> typ) fields in + let ty = Types.curry args s in + let constructor = Var.create variant ty ~scope:Global in + (variant, VariantCase { variant; belongs_to = s; constructor })) + ); + } + | _ -> failwith "not declarable type" + let add_decl ?(attrib = StringMap.empty) p v decl = { p with globals = StringMap.add v decl p.globals } @@ -157,6 +196,7 @@ let create_single_proc ?(name = "") () = modulename = name; entry_proc = Some procname; globals = StringMap.empty; + implicit_decls = StringMap.empty; procs = IDMap.singleton procname proc; proc_names; attrib = StringMap.empty; @@ -171,6 +211,7 @@ let empty ?name () = modulename; entry_proc = None; globals = StringMap.empty; + implicit_decls = StringMap.empty; procs = IDMap.empty; proc_names = ID.make_gen (); attrib = StringMap.empty; diff --git a/lib/loadir.ml b/lib/loadir.ml index 854e6022..be5b7ba3 100644 --- a/lib/loadir.ml +++ b/lib/loadir.ml @@ -146,14 +146,12 @@ module BasilASTLoader = struct | Decl_Type sort -> let name = unsafe_unsigil (`Local sort) in let typ = Types.mk_sort name in - let def : Program.declaration = Type { binding = name; typ } in - map_prog (fun prog -> Program.add_decl prog name def) prog + map_prog (fun prog -> Program.decl_typ prog typ) prog | Decl_RecType types -> let types = List.map trans_typedecl types in List.fold_left (fun prog (binding, typ) -> - let def : Program.declaration = Type { binding; typ } in - map_prog (fun prog -> Program.add_decl prog binding def) prog) + map_prog (fun prog -> Program.decl_typ prog typ) prog) prog types | Decl_Mem (modifiers, bident, type', spec) -> let attrib = StringMap.of_list (trans_varspec prog spec) in @@ -459,7 +457,7 @@ module BasilASTLoader = struct Types.mk_field (unsafe_unsigil (`Local id)) (trans_type ty) and transRECORDTYPE (fields : field list) = - Types.Record + Types.Struct (StringMap.of_list ((List.map (function Field1 (_, field_name, _, t, offset, _, _) -> ( transStr field_name, @@ -872,6 +870,30 @@ module BasilASTLoader = struct let msg = m ^ " " ^ vn in raise (LoadError { token_char_offset_range; msg; input = None }) + and lookup_constructor p_st ident = + let vn = unsafe_unsigil (`Local ident) in + match StringMap.find_opt vn p_st.prog.implicit_decls with + | Program.(Some (VariantCase { constructor })) -> constructor + | _ -> + let token_char_offset_range = Some (get_bident_loc (`Local ident)) in + let msg = "Unable to find constructor for:" ^ vn in + raise (LoadError { token_char_offset_range; msg; input = None }) + + and lookup_type p_st ident = + let vn = unsafe_unsigil (`Local ident) in + let token_char_offset_range = Some (get_bident_loc (`Local ident)) in + let fail () = + let msg = "Unable to find type declaration for:" ^ vn in + raise (LoadError { token_char_offset_range; msg; input = None }) + in + match StringMap.find_opt vn p_st.prog.globals with + | Some (Type { typ }) -> typ + | None -> ( + match StringMap.find_opt vn p_st.prog.implicit_decls with + | Program.(Some (VariantCase { belongs_to })) -> belongs_to + | _ -> fail ()) + | _ -> fail () + and lookup_global_decl ident p_st = let vn = unsafe_unsigil (`Global ident) in let token_char_offset_range = Some (get_bident_loc (`Global ident)) in @@ -946,6 +968,10 @@ module BasilASTLoader = struct in BasilExpr.applyintrin ~op:`Cases cases + and trans_field_assign trans_expr (f : fieldAssign) = + match f with + | FieldAssign1 (k, v) -> (unsafe_unsigil (`Local k), trans_expr v) + and trans_expr ?(binds = StringMap.empty) (p_st : load_st) (x : BasilIR.AbsBasilIR.expr) : BasilExpr.t = let trans_expr ?(nbinds = []) = @@ -1019,12 +1045,25 @@ module BasilASTLoader = struct ~hi_excl:(transIntVal ival0 |> Z.to_int) ~lo_incl:(transIntVal intval |> Z.to_int) (trans_expr expr) - | Expr_FAccess (o, offset, record, c) -> - BasilExpr.faccess ~attrib:(expr_range_attr o c) - ~offset:(transStr offset) (trans_expr record) - | Expr_FSet (o, offset, record, expr, c) -> - BasilExpr.fset ~attrib:(expr_range_attr o c) ~offset:(transStr offset) - (trans_expr record) (trans_expr expr) + | Expr_FieldSet (record, fname, value) -> + let fname = + String.chop_prefix ~pre:"." @@ unsafe_unsigil (`Local fname) + |> Option.get_exn_or "safe by parser" + in + BasilExpr.field_store ~field:fname (trans_expr record) + (trans_expr value) + | Expr_Field (record, fname) -> + let fname = + String.chop_prefix ~pre:"." @@ unsafe_unsigil (`Attr fname) + |> Option.get_exn_or "safe by parser" + in + BasilExpr.field_read ~field:fname (trans_expr record) + | SortValRec (variant, bi, fields, ei) -> + let f = BasilExpr.rvar @@ lookup_constructor p_st variant in + BasilExpr.apply_fun ~func:f + (List.map (trans_field_assign trans_expr) fields |> List.map snd) + | Expr_Ite (cond, t, e) -> + BasilExpr.ifthenelse (trans_expr cond) (trans_expr t) (trans_expr e) | Expr_LoadLe (o, intval, a1, a2, c) -> BasilExpr.load ~attrib:(expr_range_attr o c) ~bits:(Z.to_int @@ transIntVal intval) @@ -1507,7 +1546,7 @@ proc @main_4196260 () -> () [ block %main_entry [ $NF:bv1 := 0x1:bv1; - $ZF:bv1 := $NF:bv1; + $ZF:bv1 := $NF; goto (%main_basil_return_1); ]; block %main_basil_return_1 [ nop; return; ] @@ -1607,7 +1646,7 @@ proc @test1() -> () proc @test1() -> () { .name = "test1" } modifies $R0:bv64, $R1:bv64 captures $R0:bv64, $R1:bv64 - requires eq($R1:bv64, 0x0:bv64) - ensures eq($R1:bv64, 0x0:bv64) + requires eq($R1, 0x0:bv64) + ensures eq($R1, 0x0:bv64) ; |}] diff --git a/lib/passes.ml b/lib/passes.ml index b3aa0a0c..da48a0d4 100644 --- a/lib/passes.ml +++ b/lib/passes.ml @@ -162,6 +162,27 @@ module PassManager = struct doc = "Fail if the IR program is not type correct"; } + let split_memory_encoding = + { + name = "split-memory-encoding"; + apply = Prog Transforms.Memory_encoding.split_transform; + doc = "Generates a split base/offset pair memory encoding/model"; + } + + let flat_memory_encoding = + { + name = "flat-memory-encoding"; + apply = Prog Transforms.Memory_encoding.flat_transform; + doc = "Generates a flat (heavily quantified) memory encoding/model"; + } + + let memory_specification = + { + name = "memory-specification"; + apply = Prog Transforms.Memory_specification.transform; + doc = "Specifies programs for memory safety"; + } + let intra_function_summaries = { name = "intra-function-summaries"; @@ -202,6 +223,8 @@ module PassManager = struct sssa; full_ssa; type_check; + split_memory_encoding; + memory_specification; intra_function_summaries; inter_function_summaries; { diff --git a/lib/transforms/boogie_prepass.ml b/lib/transforms/boogie_prepass.ml index f1dad7e5..ac589aff 100644 --- a/lib/transforms/boogie_prepass.ml +++ b/lib/transforms/boogie_prepass.ml @@ -101,6 +101,7 @@ module Builtins = struct | `INTNEG -> Prefix "-" | `BVConcat -> Infix "++" | `IMPLIES -> Infix "==>" + | `ReadField s -> Postfix (Printf.sprintf "->%s" s) | `Extract (hi, lo) -> Postfix (Printf.sprintf "[%d:%d]" hi lo) | `BOOLTOBV1 -> Function "bool_to_bv1" | #Lang.Ops.AllOps.binary | #Lang.Ops.AllOps.unary | #Lang.Ops.AllOps.intrin @@ -257,7 +258,7 @@ module Instructions = struct in let steps = val_size / 8 in let body = - (if be then List.range (steps - 1) 0 else List.range 0 (steps - 1)) + (if be then List.range 0 (steps - 1) else List.range (steps - 1) 0) |> List.tl |> List.fold_left (fun acc i -> @@ -277,7 +278,7 @@ module Instructions = struct (Lang.Expr.BasilExpr.rvar index) (Lang.Expr.BasilExpr.bvconst (Bitvec.of_int ~size:addr_size - (if be then steps - 1 else 0))))) + (if be then 0 else steps - 1))))) in Lang.Expr.BasilExpr.binding ~op:`Lambda [ memory; index ] body @@ -289,6 +290,15 @@ module Instructions = struct StringMap.of_list [ (".extern", `List []); (".define", `List []) ] in let attribs = StringMap.singleton ".boogie" (`Assoc boogie_attribs) in + let body = + store_body (Var.typ rhs) + (match Lang.Expr.BasilExpr.type_of value with + | Types.Bitvector s -> s + | _ -> failwith "Expected bitvec type") + (match Lang.Expr.BasilExpr.type_of addr with + | Types.Bitvector s -> s + | _ -> failwith "Expected bitvec type") + in Some (Function { @@ -297,16 +307,8 @@ module Instructions = struct Var.create (Printf.sprintf "store%d_%s" size (Lang.Stmt.show_endian endian)) - (Var.typ lhs); - definition = - Function - (store_body (Var.typ rhs) - (match Lang.Expr.BasilExpr.type_of value with - | Types.Bitvector s -> s - | _ -> failwith "Expected bitvec type") - (match Lang.Expr.BasilExpr.type_of addr with - | Types.Bitvector s -> s - | _ -> failwith "Expected bitvec type")); + (Lang.Expr.BasilExpr.type_of body); + definition = Lang.Program.Function body; } : Lang.Program.declaration) | Lang.Stmt.Instr_Load { lhs; rhs; addr = Addr { addr; size; endian } } -> diff --git a/lib/transforms/dune b/lib/transforms/dune index 10dbb6ec..cd2d0a5f 100644 --- a/lib/transforms/dune +++ b/lib/transforms/dune @@ -9,6 +9,8 @@ cleanup_cfg may_read_uninit type_check + memory_encoding + memory_specification function_summaries boogie_prepass gamma_vars) diff --git a/lib/transforms/gamma_vars.ml b/lib/transforms/gamma_vars.ml index 4c86a3cf..3522bfc5 100644 --- a/lib/transforms/gamma_vars.ml +++ b/lib/transforms/gamma_vars.ml @@ -90,7 +90,7 @@ let update_stmts ?(check_names = false) (add : ID.t -> Var.t -> bool) pid (prog : Program.t) (b : (Var.t, Expr.BasilExpr.t) Block.t) = let open Stmt in let update_expr = update_expr ~check_names (add pid) in - let proc = ID.Map.find pid prog.procs in + let proc = IDMap.find pid prog.procs in Block.map ~phi:(fun a -> List.flat_map @@ -133,7 +133,7 @@ let update_stmts ?(check_names = false) (add : ID.t -> Var.t -> bool) pid args = update_args ~check_names (add pid) (fun _ -> true) args; } | Instr_Call { lhs; procid; args } -> - let callee = ID.Map.find procid prog.procs in + let callee = IDMap.find procid prog.procs in Instr_Call { lhs = @@ -198,7 +198,7 @@ let transform_proc ?(check_names = false) (add : ID.t -> Var.t -> bool) prog let transform ?(check_names = false) (p : Program.t) = let p = add_globals ~check_names (fun v -> true) p in let procs = - ID.Map.map + IDMap.map (fun proc -> transform_proc ~check_names (fun pid v -> true) p proc) p.procs in diff --git a/lib/transforms/livevars.ml b/lib/transforms/livevars.ml index f54c87e8..485dcd14 100644 --- a/lib/transforms/livevars.ml +++ b/lib/transforms/livevars.ml @@ -95,10 +95,8 @@ let%expect_test _ = print_endline (to_string e2); [%expect {| - forall (v1:bv1) :: (eq(v2:bv1, - forall (v2:bv1) :: (booland(v1:bv1, v2:bv1, v3:bv1)))) - forall (v1:bv1) :: (eq(0x16:bv5, - forall (v2:bv1) :: (booland(v1:bv1, v2:bv1, 0x16:bv5)))) + forall (v1:bv1) :: (eq(v2, forall (v2:bv1) :: (booland(v1, v2, v3)))) + forall (v1:bv1) :: (eq(0x16:bv5, forall (v2:bv1) :: (booland(v1, v2, 0x16:bv5)))) |}] module DSE = struct diff --git a/lib/transforms/memory_encoding.ml b/lib/transforms/memory_encoding.ml new file mode 100644 index 00000000..31db9146 --- /dev/null +++ b/lib/transforms/memory_encoding.ml @@ -0,0 +1,508 @@ +open Lang +open Lang.Common +open Lang.Expr +open Ops + +let fresh = Bitvec.of_int 0 ~size:2 +let live = Bitvec.of_int 1 ~size:2 +let dead = Bitvec.of_int 2 ~size:2 + +module Globals = struct + let mem_encoding = + Var.create "$mem_encoding" ~scope:Var.Global (Types.Variable "MemEncoding") +end + +module Calls = struct + open BasilExpr + + (** [addr_is_heap args] checks if an address belongs to the heap. args(0) is + the memory encoding object. args(1) is the address to check. *) + let addr_is_heap args = + apply_fun + ~func: + (rvar (Var.create "me_addr_is_heap" ~scope:Var.Global Types.Boolean)) + args + + (** [alloc_base args] returns the base address of a supplied allocation id. + args(0) is the memory encoding object. args(1) is the allocation id. *) + let alloc_base args = + apply_fun + ~func: + (rvar + (Var.create "me_alloc_base" ~scope:Var.Global (Types.Bitvector 64))) + args + + (** [alloc_live args] returns the liveness of an allocation. Returns value is + 0 for fresh, 1 for live, and 2 for dead, as a bv3. args(0) is the memory + encoding object. args(1) is the allocation id. *) + let alloc_live args = + apply_fun + ~func: + (rvar + (Var.create "me_alloc_live" ~scope:Var.Global (Types.Bitvector 2))) + args + + (** [alloc_size args] returns the size of an allocation. args(0) is the memory + encoding object. args(1) is the allocation id. *) + let alloc_size args = + apply_fun + ~func: + (rvar + (Var.create "me_alloc_size" ~scope:Var.Global (Types.Bitvector 64))) + args + + (** [addr_alloc args] returns the allocation id of an address. args(0) is the + memory encoding object. args(1) is the address. *) + let addr_alloc args = + apply_fun + ~func: + (rvar + (Var.create "me_addr_alloc" ~scope:Var.Global (Types.Bitvector 64))) + args + + (** [addr_offset args] returns the offset an address is into its allocation. + args(0) is the memory encoding object. args(1) is the address. *) + let addr_offset args = + apply_fun + ~func: + (rvar + (Var.create "me_addr_offset" ~scope:Var.Global (Types.Bitvector 64))) + args + + (** [alloc_size_update args] returns a new memory encoding with the size of an + allocation updated. args(0) is the memory encoding object. args(1) is the + allocation id. args(2) is the new size. *) + let alloc_size_update args = + apply_fun + ~func: + (rvar + (Var.create "me_alloc_size_update" ~scope:Var.Global + (Types.Variable "MemEncoding"))) + args + + (** [alloc_live_update args] returns a new memory encoding with the liveness + of an allocation updated. args(0) is the memory encoding object. args(1) + is the allocation id. args(2) is the new liveness value as a bv3. *) + let alloc_live_update args = + apply_fun + ~func: + (rvar + (Var.create "me_alloc_live_update" ~scope:Var.Global + (Types.Variable "MemEncoding"))) + args + + (** [allocate args] allocates space at a size, returning the updated memory + encoding. args(0) is the memory encoding object. args(1) is the address + being allocated at. args(2) is the size of the allocation. *) + let allocate args = + apply_fun + ~func: + (rvar + (Var.create "me_allocate" ~scope:Var.Global + (Types.Variable "MemEncoding"))) + args + + (** [can_alloc args] Returns whether an alloc, performed by [allocate], is + valid/allowed. args(0) is the memory encoding object. args(1) is the + target address. args(2) is the size of the allocation. *) + let can_alloc args = + apply_fun + ~func: + (rvar (Var.create "me_can_allocate" ~scope:Var.Global Types.Boolean)) + args + + (** [init_encoding args] Returns if a memory encoding is initialized. + args(0) is the memory encoding. *) + let init_encoding args = + apply_fun + ~func: + (rvar (Var.create "me_init_encoding" ~scope:Var.Global Types.Boolean)) + args + + (** [valid_access args] Checks if an access is valid. args(0) is the memory encoding object. args(1) is the address being accessed. args(2) is the size of the access in bytes. *) + let valid_access args = + apply_fun + ~func: + (rvar (Var.create "me_valid_access" ~scope:Var.Global Types.Boolean)) + args +end + +module type MemoryEncoding = sig + module Locals : sig + val mem_encoding : Var.t + val alloc : Var.t + val addr : Var.t + val size : Var.t + val live : Var.t + end + + val mem_encoding_type : Types.t + val can_allocate_body : Lang.Program.e + val alloc_size_body : Lang.Program.e + val alloc_base_body : Lang.Program.e + val addr_alloc_body : Lang.Program.e + val alloc_live_body : Lang.Program.e + val addr_offset_body : Lang.Program.e + val addr_is_heap_body : Lang.Program.e + val alloc_size_update_body : Lang.Program.e + val alloc_live_update_body : Lang.Program.e + val allocate_body : Lang.Program.e + val init_encoding_body : Lang.Program.e + val valid_access_body : Lang.Program.e +end + +module MemoryEncoder (Encoding : MemoryEncoding) = struct + let add_decl ?(attrib = Attrib.empty) (p : Program.t) (name : string) + (bindings : Var.t list) (body : BasilExpr.t) = + Lang.Program.add_decl ~attrib p name + (Lang.Program.Function + { + binding = + Bincaml_util.Common.Var.create name + (Lang.Expr.BasilExpr.type_of body); + attrib; + definition : Lang.Program.func_type = + Function (Lang.Expr.BasilExpr.binding ~op:`Lambda bindings body); + }) + + let add_mem_encoding p = + let p = + Lang.Program.add_decl p "mem_encoding_type" + (Lang.Program.Type + { binding = "MemEncoding"; typ = Encoding.mem_encoding_type }) + in + let p = + Lang.Program.add_decl p "mem_encoding_glob" + (Lang.Program.Variable + { binding = Globals.mem_encoding; attrib = Attrib.empty }) + in + p + + let attrib = + StringMap.of_list + [ + ( ".boogie", + `Assoc + (StringMap.of_list + [ + (".inline", `List []); + (".extern", `List []); + (* (".define", `List []) *) + ]) ); + ] + + let add_can_allocate p = + add_decl ~attrib p "me_can_allocate" + [ + Encoding.Locals.mem_encoding; Encoding.Locals.addr; Encoding.Locals.size; + ] + Encoding.can_allocate_body + + let add_allocate p = + add_decl ~attrib p "me_allocate" + [ + Encoding.Locals.mem_encoding; Encoding.Locals.addr; Encoding.Locals.size; + ] + Encoding.allocate_body + + let add_alloc_size p = + add_decl ~attrib p "me_alloc_size" + [ Encoding.Locals.mem_encoding; Encoding.Locals.alloc ] + Encoding.alloc_size_body + + let add_addr_alloc p = + add_decl ~attrib p "me_addr_alloc" + [ Encoding.Locals.mem_encoding; Encoding.Locals.addr ] + Encoding.addr_alloc_body + + let add_alloc_live p = + add_decl ~attrib p "me_alloc_live" + [ Encoding.Locals.mem_encoding; Encoding.Locals.alloc ] + Encoding.alloc_live_body + + let add_addr_offset p = + add_decl ~attrib p "me_addr_offset" + [ Encoding.Locals.mem_encoding; Encoding.Locals.addr ] + Encoding.addr_offset_body + + let add_alloc_base p = + add_decl ~attrib p "me_alloc_base" + [ Encoding.Locals.mem_encoding; Encoding.Locals.alloc ] + Encoding.alloc_base_body + + let add_addr_is_heap p = + add_decl ~attrib p "me_addr_is_heap" + [ Encoding.Locals.mem_encoding; Encoding.Locals.addr ] + Encoding.addr_is_heap_body + + let add_alloc_size_update p = + add_decl ~attrib p "me_alloc_size_update" + [ + Encoding.Locals.mem_encoding; + Encoding.Locals.alloc; + Encoding.Locals.size; + ] + Encoding.alloc_size_update_body + + let add_alloc_live_update p = + add_decl ~attrib p "me_alloc_live_update" + [ + Encoding.Locals.mem_encoding; + Encoding.Locals.alloc; + Encoding.Locals.live; + ] + Encoding.alloc_live_update_body + + let add_init_encoding p = + add_decl ~attrib p "me_init_encoding" + [ Encoding.Locals.mem_encoding ] + Encoding.init_encoding_body + + let add_valid_access_body p = + add_decl ~attrib p "me_valid_access" + [ + Encoding.Locals.mem_encoding; Encoding.Locals.addr; Encoding.Locals.size; + ] + Encoding.valid_access_body + + let add_decls (p : Lang.Program.t) = + List.fold_left + (fun acc f -> f acc) + p + [ + add_mem_encoding; + add_addr_offset; + add_alloc_base; + add_can_allocate; + add_alloc_live; + add_alloc_size; + add_addr_alloc; + add_addr_is_heap; + add_alloc_size_update; + add_alloc_live_update; + add_allocate; + add_init_encoding; + add_valid_access_body; + ] + + let transform (p : Lang.Program.t) = add_decls p +end + +module FlatMemory : MemoryEncoding = struct + open BasilExpr + + let mem_encoding_type : Types.t = + Types.Sort ("MemEncoding", [ Types.mk_variant "MemEncoding" [] ]) + + module Locals = struct + let mem_encoding : Var.t = + Var.create "mem_encoding" ~scope:Var.Local mem_encoding_type + + let alloc = Var.create "alloc" ~scope:Var.Local (Types.Bitvector 64) + let addr = Var.create "addr" ~scope:Var.Local (Types.Bitvector 64) + let size = Var.create "size" ~scope:Var.Local (Types.Bitvector 64) + let live = Var.create "live" ~scope:Var.Local (Types.Bitvector 2) + end + + let can_allocate_body : Lang.Program.e = boolconst false + let alloc_size_body : Lang.Program.e = boolconst false + let alloc_base_body : Lang.Program.e = boolconst false + let addr_alloc_body : Lang.Program.e = boolconst false + let alloc_live_body : Lang.Program.e = boolconst false + let addr_offset_body : Lang.Program.e = boolconst false + let addr_is_heap_body : Lang.Program.e = boolconst false + let alloc_size_update_body : Lang.Program.e = boolconst false + let alloc_live_update_body : Lang.Program.e = boolconst false + let allocate_body : Lang.Program.e = boolconst false + let init_encoding_body : Lang.Program.e = boolconst false + let valid_access_body : Lang.Program.e = boolconst false +end + +module SplitMemory : MemoryEncoding = struct + open BasilExpr + + let offset_size = 32 + let addr_size = 64 - offset_size + + let mem_encoding_type = + Types.Sort + ( "MemEncoding", + [ + Types.mk_variant "MemEncoding" + [ + Types.mk_field "alloc_live" + (Types.Map (Types.Bitvector 64, Types.Bitvector 2)); + Types.mk_field "alloc_size" + (Types.Map (Types.Bitvector 64, Types.Bitvector 64)); + Types.mk_field "addr_is_heap" + (Types.Map (Types.Bitvector 64, Types.Boolean)); + ]; + ] ) + + module Locals = struct + let mem_encoding = + Var.create "mem_encoding" ~scope:Var.Local mem_encoding_type + + let alloc = Var.create "alloc" ~scope:Var.Local (Types.Bitvector 64) + let addr = Var.create "addr" ~scope:Var.Local (Types.Bitvector 64) + let size = Var.create "size" ~scope:Var.Local (Types.Bitvector 64) + let live = Var.create "live" ~scope:Var.Local (Types.Bitvector 2) + + let alloc_live_access = + unexp ~op:(`ReadField "alloc_live") (rvar mem_encoding) + + let alloc_size_access = + unexp ~op:(`ReadField "alloc_size") (rvar mem_encoding) + + let addr_is_heap_access = + unexp ~op:(`ReadField "addr_is_heap") (rvar mem_encoding) + end + + let can_allocate_body = + applyintrin ~op:`AND + [ + (* Addr must be on the heap: *) + Calls.addr_is_heap [ rvar Locals.mem_encoding; rvar Locals.addr ]; + (* Address is a base address *) + binexp ~op:`EQ + (Calls.alloc_base [ rvar Locals.mem_encoding; rvar Locals.addr ]) + (rvar Locals.addr); + (* Adddress is fresh *) + binexp ~op:`EQ + (Calls.alloc_live + [ + rvar Locals.mem_encoding; + Calls.addr_alloc [ rvar Locals.mem_encoding; rvar Locals.addr ]; + ]) + (bvconst fresh); + (* Size is within bounds *) + binexp ~op:`BVULE (rvar Locals.size) + (bv_of_int ~size:64 (Int.pow 2 offset_size - 1)); + binexp ~op:`BVULT (bv_of_int ~size:64 0) (rvar Locals.size); + ] + + let alloc_size_body = + binexp ~op:`MapAccess Locals.alloc_size_access (rvar Locals.alloc) + + let alloc_base_body = + binexp ~op:`BVAND (rvar Locals.alloc) + (bv_of_int ~size:64 (Int.lnot (Int.pow 2 addr_size - 1))) + + let addr_alloc_body = rvar Locals.addr + + let alloc_live_body = + binexp ~op:`MapAccess Locals.alloc_live_access (rvar Locals.alloc) + + let addr_offset_body = + binexp ~op:`BVAND (rvar Locals.addr) + (bv_of_int ~size:64 (Int.pow 2 offset_size - 1)) + + let addr_is_heap_body = + binexp ~op:`MapAccess Locals.addr_is_heap_access (rvar Locals.addr) + + let alloc_size_update_body = + binexp ~op:(`WriteField "alloc_size") (rvar Locals.mem_encoding) + (applyintrin ~op:`MapUpdate + [ Locals.alloc_size_access; rvar Locals.alloc; rvar Locals.size ]) + + let alloc_live_update_body = + binexp ~op:(`WriteField "alloc_live") (rvar Locals.mem_encoding) + (applyintrin ~op:`MapUpdate + [ Locals.alloc_live_access; rvar Locals.alloc; rvar Locals.live ]) + + let allocate_body = + let alloc = + Calls.addr_alloc [ rvar Locals.mem_encoding; rvar Locals.addr ] + in + + Calls.alloc_size_update + [ + Calls.alloc_live_update + [ rvar Locals.mem_encoding; alloc; bvconst live ]; + alloc; + rvar Locals.size; + ] + + let init_encoding_body = + let i = Var.create "i" ~scope:Var.Local (Types.Bitvector 64) in + let trigger e = + `Assoc (StringMap.of_list [ (".triggers", `List [ `List [ `Expr e ] ]) ]) + in + applyintrin ~op:`AND + [ + (* Ensure that all heap addresses are bigger than the largest global address *) + forall + ~attrib: + (trigger (Calls.addr_is_heap [ rvar Locals.mem_encoding; rvar i ])) + ~bound:[ i ] + (binexp ~op:`EQ + (binexp ~op:`BVULT + (* TODO compute this value somehow *) + (bv_of_int 100000000 ~size:64) + (rvar i)) + (Calls.addr_is_heap [ rvar Locals.mem_encoding; rvar i ])); + (* Heap addresses are initially fresh *) + forall + ~attrib: + (trigger (Calls.alloc_live [ rvar Locals.mem_encoding; rvar i ])) + ~bound:[ i ] + (binexp ~op:`IMPLIES + (Calls.addr_is_heap [ rvar Locals.mem_encoding; rvar i ]) + (binexp ~op:`EQ + (Calls.alloc_live [ rvar Locals.mem_encoding; rvar i ]) + (bvconst fresh))); + (* Non heap addresses are dead *) + forall + ~attrib: + (trigger (Calls.alloc_live [ rvar Locals.mem_encoding; rvar i ])) + ~bound:[ i ] + (binexp ~op:`IMPLIES + (boolnot (Calls.addr_is_heap [ rvar Locals.mem_encoding; rvar i ])) + (binexp ~op:`EQ + (Calls.alloc_live [ rvar Locals.mem_encoding; rvar i ]) + (bvconst dead))); + ] + + let valid_access_body = + binexp ~op:`IMPLIES + (Calls.addr_is_heap [ rvar Locals.mem_encoding; rvar Locals.addr ]) + (applyintrin ~op:`AND + [ + binexp ~op:`EQ + (Calls.alloc_live + [ + rvar Locals.mem_encoding; + Calls.alloc_base + [ + rvar Locals.mem_encoding; + Calls.addr_alloc + [ rvar Locals.mem_encoding; rvar Locals.addr ]; + ]; + ]) + (bvconst live); + binexp ~op:`BVULE + (Calls.addr_offset + [ + rvar Locals.mem_encoding; + binexp ~op:`BVADD (rvar Locals.addr) (rvar Locals.size); + ]) + (Calls.alloc_size + [ + rvar Locals.mem_encoding; + Calls.alloc_base + [ + rvar Locals.mem_encoding; + Calls.addr_alloc + [ rvar Locals.mem_encoding; rvar Locals.addr ]; + ]; + ]); + ]) +end + +let split_transform (p : Program.t) = + let module E = MemoryEncoder (SplitMemory) in + E.transform p + +let flat_transform (p : Program.t) = + let module E = MemoryEncoder (FlatMemory) in + E.transform p diff --git a/lib/transforms/memory_specification.ml b/lib/transforms/memory_specification.ml new file mode 100644 index 00000000..18bd6a04 --- /dev/null +++ b/lib/transforms/memory_specification.ml @@ -0,0 +1,153 @@ +open Lang +open Lang.Common +open Lang.Expr +open Ops +open Memory_encoding + +(* TODO: Support simplify, have this produce _out vars appropriately? *) +let old e = BasilExpr.unexp ~op:`Old e + +let r n = + BasilExpr.rvar + (Var.create ~scope:Var.Global (Printf.sprintf "$R%d" n) (Types.Bitvector 64)) + +let transform_main p = + (* TODO: Specify Gammas Oneday *) + let spec = Procedure.specification p in + Procedure.set_specification p + { + spec with + requires = + spec.requires + @ [ Calls.init_encoding [ BasilExpr.rvar Globals.mem_encoding ] ]; + modifies_globs = spec.modifies_globs @ [ Globals.mem_encoding ]; + } + +let transform_malloc p = + (* TODO: Specify Gammas Oneday *) + let spec = Procedure.specification p in + let open BasilExpr in + Procedure.set_specification p + { + spec with + ensures = + spec.ensures + @ [ + (* Can allocate at new r0 with size old r0 *) + Calls.can_alloc + [ old @@ rvar Globals.mem_encoding; r 0; old @@ r 0 ]; + (* Offset of return address r0 is 0 *) + binexp ~op:`EQ + (Calls.addr_offset [ rvar Globals.mem_encoding; r 0 ]) + (bv_of_int ~size:64 0); + (* Base of associated allocation is r(0) *) + binexp ~op:`EQ + (Calls.alloc_base + [ + rvar Globals.mem_encoding; + Calls.addr_alloc [ rvar Globals.mem_encoding; r 0 ]; + ]) + (r 0); + (* Update the memory encoding: *) + binexp ~op:`EQ + (rvar Globals.mem_encoding) + (Calls.allocate + [ old @@ rvar Globals.mem_encoding; r 0; old @@ r 0 ]); + ]; + modifies_globs = spec.modifies_globs @ [ Globals.mem_encoding ]; + } + +let transform_free p = + (* TODO: Specify Gammas Oneday *) + let spec = Procedure.specification p in + let open BasilExpr in + Procedure.set_specification p + { + spec with + requires = + spec.requires + @ [ + (* Only free heap values *) + Calls.addr_is_heap [ rvar Globals.mem_encoding; r 0 ]; + (* Only free if offset is 0 *) + binexp ~op:`EQ (bv_of_int ~size:64 0) + (Calls.addr_offset [ rvar Globals.mem_encoding; r 0 ]); + (* The object must be live to free *) + binexp ~op:`EQ + (Calls.alloc_live + [ + rvar Globals.mem_encoding; + Calls.addr_alloc [ rvar Globals.mem_encoding; r 0 ]; + ]) + (bvconst live); + ]; + ensures = + spec.ensures + @ [ + binexp ~op:`EQ + (rvar Globals.mem_encoding) + (Calls.alloc_live_update + [ + old @@ rvar Globals.mem_encoding; + Calls.addr_alloc [ old @@ rvar Globals.mem_encoding; r 0 ]; + BasilExpr.bvconst dead; + ]); + ]; + modifies_globs = spec.modifies_globs @ [ Globals.mem_encoding ]; + } + +let transform_stmt (s : Program.stmt) = + (match s with + | Stmt.Instr_Store { lhs; rhs; value; addr = Addr { addr; size; endian } } + -> ( + let valid_assert = + Stmt.Instr_Assert + { + body = + BasilExpr.( + Calls.valid_access + [ + rvar Globals.mem_encoding; + addr; + bv_of_int ~size:64 (size / 8); + ]); + } + in + match Var.name rhs with "$mem" -> [ valid_assert; s ] | _ -> [ s ]) + | Stmt.Instr_Load { lhs; rhs; addr = Addr { addr; size; endian } } -> ( + let valid_assert = + Stmt.Instr_Assert + { + body = + BasilExpr.( + Calls.valid_access + [ + rvar Globals.mem_encoding; + addr; + bv_of_int ~size:64 (size / 8); + ]); + } + in + match Var.name rhs with "$mem" -> [ valid_assert; s ] | _ -> [ s ]) + | _ -> [ s ]) + |> List.to_iter + +let transform_proc entry (p : Program.proc) = + let p = + Procedure.map_blocks_nondet + (fun (i, b) -> Block.flat_map ~phi:Fun.id transform_stmt b) + p + in + let name = ID.name (Procedure.id p) in + match name with + | "@main" -> transform_main p + | e when String.equal entry e -> transform_main p + | "@malloc" -> transform_malloc p + | "@free" -> transform_free p + | _ -> p + +let transform (p : Program.t) = + let entry = p.entry_proc |> Option.map ID.name |> Option.get_or ~default:"" in + let procs = IDMap.map (transform_proc entry) p.procs in + let p = { p with procs } in + (fun prog -> Loader.Spec_modifies.set_modsets ~add_only:true prog) p diff --git a/lib/transforms/type_check.ml b/lib/transforms/type_check.ml index 1bb6a9f7..64d23d9a 100644 --- a/lib/transforms/type_check.ml +++ b/lib/transforms/type_check.ml @@ -27,10 +27,11 @@ let type_check stmt_id block_id expr = match op with | `Classification -> [] | `Gamma -> [] - | `FACCESS _ -> ( + | `Old -> [] + | `ReadField _ -> ( match arg with - | Record _ -> [] - | _ -> [ type_err "FACCESS body is not a record type" ]) + | Struct _ -> [] + | _ -> [ type_err "ReadField body is not a record type" ]) | `BoolNOT | `BOOLTOBV1 -> if Types.equal arg Types.Boolean then [] else [ type_err "%s body is not a boolean" @@ AllOps.to_string op ] @@ -53,7 +54,6 @@ let type_check stmt_id block_id expr = @@ AllOps.to_string op; ]) | _ -> [ type_err "%s body is not a bitvector" @@ AllOps.to_string op ]) - | `Old -> [] in let check_binary (op : Ops.AllOps.binary) (arg1 : Types.t) (arg2 : Types.t) : @@ -101,13 +101,13 @@ let type_check stmt_id block_id expr = | _ -> err @ [ type_err "%s is not of pointer type" @@ Types.to_string arg2 ]) - | `FSET offset -> + | `WriteField offset -> let err = match arg1 with - | Record _ -> [] + | Struct _ -> [] | _ -> [ type_err "%s is not of record type" @@ Types.to_string arg1 ] in - let { typ } : Types.record_field = Types.get_field offset arg1 in + let { typ } : Types.record_field = Types.struct_field offset arg1 in if List.length err = 1 || Types.equal arg2 typ then err else [ diff --git a/lib/util/types.ml b/lib/util/types.ml index 2e311705..9f576113 100644 --- a/lib/util/types.ml +++ b/lib/util/types.ml @@ -27,15 +27,17 @@ module StringMap = Map.Make (String) type t = | Boolean - | Integer - | Bitvector of int - | Unit - | Top - | Nothing - | Map of t * t - | Sort of string * variant list - | Record of record_field StringMap.t - | Pointer of pointer + | Integer (** mathematical integer type (Z)*) + | Bitvector of int (** bitvector of a given width *) + | Unit (** type inhabited by unit value *) + | Top (** greatest type *) + | Nothing (** least type / empty set *) + | Map of t * t (** function type *) + | Sort of string * variant list (** An Algebraic datatype *) + | Struct of record_field StringMap.t + (** a struct is a product type of a known layout that is representible as + a finite byte/bit sequence *) + | Pointer of pointer (** pointer type *) | Variable of string (* Possibly a name of a type declartion *) and variant = { variant : string; fields : field list } @@ -66,15 +68,12 @@ let mk_variant name fields = { variant = name; fields } let mk_enum name (cases : string list) = Sort (name, List.map (fun variant -> { variant; fields = [] }) cases) -(* ADT not Record type *) -let mk_record name (fields : field list) = +let mk_adt_record name (fields : field list) = Sort (name, [ mk_variant ("Record" ^ name) fields ]) -(* ADT not Record type *) -let record_field name t = +let adt_record_field name t = match t with - | Sort (sort_name, [ { variant; fields } ]) - when String.equal variant ("Record" ^ sort_name) -> + | Sort (_, [ { fields; _ } ]) -> fields |> List.find_map (function | { field; typ } when String.equal field name -> Some typ @@ -85,9 +84,9 @@ let mk_adt name (variants : (string * field list) list) = Sort (name, variants |> List.map (fun (variant, fields) -> { variant; fields })) -let get_field field_name record : record_field = +let struct_field field_name record : record_field = match record with - | Record fields -> ( + | Struct fields -> ( match StringMap.find_opt field_name fields with | None -> failwith @@ "No field at offset " ^ field_name | Some t -> t) @@ -110,7 +109,7 @@ let rec compare_partial (a : t) (b : t) = compare_partial lower lower1 |> function | Some 0 -> compare_partial upper upper1 | o -> o) - | Record fields, Record fields2 -> + | Struct fields, Struct fields2 -> Some (StringMap.compare (fun ({ typ = a; _ } : record_field) { typ = b; _ } -> @@ -144,7 +143,7 @@ let rec to_string = function | Variable name -> name | Pointer { lower; upper } -> Printf.sprintf "ptr(%s, %s)" (to_string lower) (to_string upper) - | Record record -> + | Struct record -> "{" ^ (StringMap.bindings record |> List.map (fun (k, ({ typ = v; offset } : record_field)) -> @@ -175,6 +174,12 @@ let rec to_string = function (function { variant; fields } -> fsort variant fields) variants +let to_string_rexp = function + | ( Boolean | Integer | Bitvector _ | Unit | Top | Nothing | Variable _ + | Pointer _ | Struct _ | Map _ ) as e -> + to_string e + | Sort (name, _) -> name + let%expect_test "dtp" = let lst = Sort @@ -192,7 +197,7 @@ let%expect_test "dtp" = ] ) in let rc = - mk_record "recs" [ mk_field "a" (Bitvector 12); mk_field "b" Boolean ] + mk_adt_record "recs" [ mk_field "a" (Bitvector 12); mk_field "b" Boolean ] in print_endline @@ to_string lst; print_endline @@ to_string rc; diff --git a/nix/shell.nix b/nix/shell.nix index 58c34064..e3803690 100644 --- a/nix/shell.nix +++ b/nix/shell.nix @@ -1,29 +1,38 @@ -{ lib -, stdenv -, mkShell - -# ocaml packages -, bincaml -, odoc -, odig -, ocaml-lsp -, ocamlformat - -# dev packages -, tree-sitter -, nodejs-slim -, perf -, bnfc-treesitter - +{ + lib, + stdenv, + mkShell, + + # ocaml packages + bincaml, + odoc, + odig, + ocaml-lsp, + ocamlformat, + + # dev packages + tree-sitter, + nodejs-slim, + perf, + bnfc-treesitter, + boogie, + cvc5, }: mkShell { packages = [ - odoc odig ocaml-lsp ocamlformat - tree-sitter nodejs-slim + odoc + odig + ocaml-lsp + ocamlformat + tree-sitter + nodejs-slim bnfc-treesitter + boogie + cvc5 # sherlodoc - not in nixpkgs? - ] ++ lib.optional stdenv.hostPlatform.isLinux perf; + ] + ++ lib.optional stdenv.hostPlatform.isLinux perf; inputsFrom = [ bincaml diff --git a/test/analysis/test_ide_live.ml b/test/analysis/test_ide_live.ml index 20604bf1..3bd03096 100644 --- a/test/analysis/test_ide_live.ml +++ b/test/analysis/test_ide_live.ml @@ -93,9 +93,9 @@ proc @main (x_in:bv64) -> () print_lives results main; [%expect {| @main + addr:bv64 $mem:(bv64->bv8) x_in:bv64 - addr:bv64 |}] let%expect_test "simple_call" = diff --git a/test/cram/basicssa.t b/test/cram/basicssa.t index 1ea70d79..0a74604b 100644 --- a/test/cram/basicssa.t +++ b/test/cram/basicssa.t @@ -25,43 +25,43 @@ Run on basic irreducible loop example [ block %main_entry [ - var #4:bv64 := bvadd($R31:bv64, 0xffffffffffffffe0:bv64); - $stack:(bv64->bv8) := store le $stack:(bv64->bv8) #4:bv64 $R29:bv64 64; - $stack:(bv64->bv8) := store le $stack:(bv64->bv8) bvadd(#4:bv64, 0x8:bv64) $R30:bv64 64; - $R31:bv64 := #4:bv64; - $R29:bv64 := $R31:bv64; - $stack:(bv64->bv8) := store le $stack:(bv64->bv8) bvadd($R31:bv64, 0x1c:bv64) extract(32,0, $R0:bv64) 32; - $stack:(bv64->bv8) := store le $stack:(bv64->bv8) bvadd($R31:bv64, 0x10:bv64) $R1:bv64 64; + var #4:bv64 := bvadd($R31, 0xffffffffffffffe0:bv64); + $stack:(bv64->bv8) := store le $stack:(bv64->bv8) #4 $R29 64; + $stack:(bv64->bv8) := store le $stack:(bv64->bv8) bvadd(#4, 0x8:bv64) $R30 64; + $R31:bv64 := #4; + $R29:bv64 := $R31; + $stack:(bv64->bv8) := store le $stack:(bv64->bv8) bvadd($R31, 0x1c:bv64) extract(32,0, $R0) 32; + $stack:(bv64->bv8) := store le $stack:(bv64->bv8) bvadd($R31, 0x10:bv64) $R1 64; $R0:bv64 := 0x20000:bv64; - $R0:bv64 := bvadd($R0:bv64, 0x3c:bv64); - $mem:(bv64->bv8) := store le $mem:(bv64->bv8) $R0:bv64 0x0:bv32 32; + $R0:bv64 := bvadd($R0, 0x3c:bv64); + $mem:(bv64->bv8) := store le $mem:(bv64->bv8) $R0 0x0:bv32 32; $R0:bv64 := 0x20000:bv64; - $R0:bv64 := bvadd($R0:bv64, 0x40:bv64); - var load18:bv32 := load le $mem:(bv64->bv8) $R0:bv64 32; - $R0:bv64 := zero_extend(32, load18:bv32); - $R0:bv64 := zero_extend(32, bvconcat(0x0:bv31, extract(1,0, $R0:bv64))); - var #5:bv32 := bvadd(extract(32,0, $R0:bv64), 0xffffffff:bv32); - $VF:bv1 := bvnot(booltobv1(eq(sign_extend(1, bvadd(#5:bv32, 0x1:bv32)), - bvadd(sign_extend(1, extract(32,0, $R0:bv64)), 0x0:bv33)))); - $CF:bv1 := bvnot(booltobv1(eq(zero_extend(1, bvadd(#5:bv32, 0x1:bv32)), - bvadd(zero_extend(1, extract(32,0, $R0:bv64)), 0x100000000:bv33)))); - $ZF:bv1 := booltobv1(eq(bvadd(#5:bv32, 0x1:bv32), 0x0:bv32)); - $NF:bv1 := extract(32,31, bvadd(#5:bv32, 0x1:bv32)); + $R0:bv64 := bvadd($R0, 0x40:bv64); + var load18:bv32 := load le $mem:(bv64->bv8) $R0 32; + $R0:bv64 := zero_extend(32, load18); + $R0:bv64 := zero_extend(32, bvconcat(0x0:bv31, extract(1,0, $R0))); + var #5:bv32 := bvadd(extract(32,0, $R0), 0xffffffff:bv32); + $VF:bv1 := bvnot(booltobv1(eq(sign_extend(1, bvadd(#5, 0x1:bv32)), + bvadd(sign_extend(1, extract(32,0, $R0)), 0x0:bv33)))); + $CF:bv1 := bvnot(booltobv1(eq(zero_extend(1, bvadd(#5, 0x1:bv32)), + bvadd(zero_extend(1, extract(32,0, $R0)), 0x100000000:bv33)))); + $ZF:bv1 := booltobv1(eq(bvadd(#5, 0x1:bv32), 0x0:bv32)); + $NF:bv1 := extract(32,31, bvadd(#5, 0x1:bv32)); goto (%main_27,%main_23); ]; block %main_23 [ - guard neq(booltobv1(eq($ZF:bv1, 0x1:bv1)), 0x0:bv1); + guard neq(booltobv1(eq($ZF, 0x1:bv1)), 0x0:bv1); goto (%main_21); ]; block %main_21 [ goto (%main_19); ]; block %main_27 [ - guard eq(booltobv1(eq($ZF:bv1, 0x1:bv1)), 0x0:bv1); + guard eq(booltobv1(eq($ZF, 0x1:bv1)), 0x0:bv1); goto (%main_25); ]; block %main_25 [ goto (%main_5); ]; block %main_5 [ $R0:bv64 := 0x0:bv64; - $R0:bv64 := bvadd($R0:bv64, 0x820:bv64); + $R0:bv64 := bvadd($R0, 0x820:bv64); $R30:bv64 := 0x7a0:bv64; call @puts_1584(); @@ -69,18 +69,18 @@ Run on basic irreducible loop example ]; block %main_3 [ $R0:bv64 := 0x20000:bv64; - $R0:bv64 := bvadd($R0:bv64, 0x3c:bv64); - var load19:bv32 := load le $mem:(bv64->bv8) $R0:bv64 32; - $R0:bv64 := zero_extend(32, load19:bv32); - $R1:bv64 := zero_extend(32, bvadd(extract(32,0, $R0:bv64), 0x1:bv32)); + $R0:bv64 := bvadd($R0, 0x3c:bv64); + var load19:bv32 := load le $mem:(bv64->bv8) $R0 32; + $R0:bv64 := zero_extend(32, load19); + $R1:bv64 := zero_extend(32, bvadd(extract(32,0, $R0), 0x1:bv32)); $R0:bv64 := 0x20000:bv64; - $R0:bv64 := bvadd($R0:bv64, 0x3c:bv64); - $mem:(bv64->bv8) := store le $mem:(bv64->bv8) $R0:bv64 extract(32,0, $R1:bv64) 32; + $R0:bv64 := bvadd($R0, 0x3c:bv64); + $mem:(bv64->bv8) := store le $mem:(bv64->bv8) $R0 extract(32,0, $R1) 32; goto (%main_19); ]; block %main_19 [ $R0:bv64 := 0x0:bv64; - $R0:bv64 := bvadd($R0:bv64, 0x820:bv64); + $R0:bv64 := bvadd($R0, 0x820:bv64); $R30:bv64 := 0x7d0:bv64; call @puts_1584(); @@ -88,27 +88,27 @@ Run on basic irreducible loop example ]; block %main_17 [ $R0:bv64 := 0x20000:bv64; - $R0:bv64 := bvadd($R0:bv64, 0x3c:bv64); - var load20:bv32 := load le $mem:(bv64->bv8) $R0:bv64 32; - $R0:bv64 := zero_extend(32, load20:bv32); - var #6:bv32 := bvadd(extract(32,0, $R0:bv64), 0xfffffffa:bv32); - $VF:bv1 := bvnot(booltobv1(eq(sign_extend(1, bvadd(#6:bv32, 0x1:bv32)), - bvadd(sign_extend(1, extract(32,0, $R0:bv64)), 0x1fffffffb:bv33)))); - $CF:bv1 := bvnot(booltobv1(eq(zero_extend(1, bvadd(#6:bv32, 0x1:bv32)), - bvadd(zero_extend(1, extract(32,0, $R0:bv64)), 0xfffffffb:bv33)))); - $ZF:bv1 := booltobv1(eq(bvadd(#6:bv32, 0x1:bv32), 0x0:bv32)); - $NF:bv1 := extract(32,31, bvadd(#6:bv32, 0x1:bv32)); + $R0:bv64 := bvadd($R0, 0x3c:bv64); + var load20:bv32 := load le $mem:(bv64->bv8) $R0 32; + $R0:bv64 := zero_extend(32, load20); + var #6:bv32 := bvadd(extract(32,0, $R0), 0xfffffffa:bv32); + $VF:bv1 := bvnot(booltobv1(eq(sign_extend(1, bvadd(#6, 0x1:bv32)), + bvadd(sign_extend(1, extract(32,0, $R0)), 0x1fffffffb:bv33)))); + $CF:bv1 := bvnot(booltobv1(eq(zero_extend(1, bvadd(#6, 0x1:bv32)), + bvadd(zero_extend(1, extract(32,0, $R0)), 0xfffffffb:bv33)))); + $ZF:bv1 := booltobv1(eq(bvadd(#6, 0x1:bv32), 0x0:bv32)); + $NF:bv1 := extract(32,31, bvadd(#6, 0x1:bv32)); goto (%main_15,%main_9); ]; block %main_9 [ - guard neq(bvnot(booltobv1(eq($ZF:bv1, 0x1:bv1))), 0x0:bv1); + guard neq(bvnot(booltobv1(eq($ZF, 0x1:bv1))), 0x0:bv1); goto (%main_7); ]; block %main_7 [ goto (%main_5); ]; block %main_15 [ - guard eq(bvnot(booltobv1(eq($ZF:bv1, 0x1:bv1))), 0x0:bv1); + guard eq(bvnot(booltobv1(eq($ZF, 0x1:bv1))), 0x0:bv1); $R0:bv64 := 0x0:bv64; - $R0:bv64 := bvadd($R0:bv64, 0x828:bv64); + $R0:bv64 := bvadd($R0, 0x828:bv64); $R30:bv64 := 0x7f4:bv64; call @puts_1584(); @@ -117,11 +117,11 @@ Run on basic irreducible loop example block %main_13 [ goto (%main_11); ]; block %main_11 [ $R0:bv64 := 0x0:bv64; - var load21:bv64 := load le $stack:(bv64->bv8) $R31:bv64 64; - $R29:bv64 := load21:bv64; - var load22:bv64 := load le $stack:(bv64->bv8) bvadd($R31:bv64, 0x8:bv64) 64; - $R30:bv64 := load22:bv64; - $R31:bv64 := bvadd($R31:bv64, 0x20:bv64); + var load21:bv64 := load le $stack:(bv64->bv8) $R31 64; + $R29:bv64 := load21; + var load22:bv64 := load le $stack:(bv64->bv8) bvadd($R31, 0x8:bv64) 64; + $R30:bv64 := load22; + $R31:bv64 := bvadd($R31, 0x20:bv64); goto (%main_basil_return_1); ]; block %main_basil_return_1 [ nop; return; ] @@ -147,47 +147,45 @@ Run on basic irreducible loop example [ block %inputs [ - (var CF_1:bv1 := CF_in:bv1, var NF_1:bv1 := NF_in:bv1, - var R0_1:bv64 := R0_in:bv64, var R1_1:bv64 := R1_in:bv64, - var R29_1:bv64 := R29_in:bv64, var R30_1:bv64 := R30_in:bv64, - var R31_1:bv64 := R31_in:bv64, var VF_1:bv1 := VF_in:bv1, - var ZF_1:bv1 := ZF_in:bv1); + (var CF_1:bv1 := CF_in, var NF_1:bv1 := NF_in, var R0_1:bv64 := R0_in, + var R1_1:bv64 := R1_in, var R29_1:bv64 := R29_in, var R30_1:bv64 := R30_in, + var R31_1:bv64 := R31_in, var VF_1:bv1 := VF_in, var ZF_1:bv1 := ZF_in); goto (%main_entry); ]; block %main_entry [ - var #4_1:bv64 := bvadd(R31_1:bv64, 0xffffffffffffffe0:bv64); - $stack:(bv64->bv8) := store le $stack:(bv64->bv8) #4_1:bv64 R29_1:bv64 64; - $stack:(bv64->bv8) := store le $stack:(bv64->bv8) bvadd(#4_1:bv64, 0x8:bv64) R30_1:bv64 64; - var R31_2:bv64 := #4_1:bv64; - var R29_2:bv64 := R31_2:bv64; - $stack:(bv64->bv8) := store le $stack:(bv64->bv8) bvadd(R31_2:bv64, 0x1c:bv64) extract(32,0, R0_1:bv64) 32; - $stack:(bv64->bv8) := store le $stack:(bv64->bv8) bvadd(R31_2:bv64, 0x10:bv64) R1_1:bv64 64; + var #4_1:bv64 := bvadd(R31_1, 0xffffffffffffffe0:bv64); + $stack:(bv64->bv8) := store le $stack:(bv64->bv8) #4_1 R29_1 64; + $stack:(bv64->bv8) := store le $stack:(bv64->bv8) bvadd(#4_1, 0x8:bv64) R30_1 64; + var R31_2:bv64 := #4_1; + var R29_2:bv64 := R31_2; + $stack:(bv64->bv8) := store le $stack:(bv64->bv8) bvadd(R31_2, 0x1c:bv64) extract(32,0, R0_1) 32; + $stack:(bv64->bv8) := store le $stack:(bv64->bv8) bvadd(R31_2, 0x10:bv64) R1_1 64; var R0_2:bv64 := 0x20000:bv64; - var R0_3:bv64 := bvadd(R0_2:bv64, 0x3c:bv64); - $mem:(bv64->bv8) := store le $mem:(bv64->bv8) R0_3:bv64 0x0:bv32 32; + var R0_3:bv64 := bvadd(R0_2, 0x3c:bv64); + $mem:(bv64->bv8) := store le $mem:(bv64->bv8) R0_3 0x0:bv32 32; var R0_4:bv64 := 0x20000:bv64; - var R0_5:bv64 := bvadd(R0_4:bv64, 0x40:bv64); - var load18_1:bv32 := load le $mem:(bv64->bv8) R0_5:bv64 32; - var R0_6:bv64 := zero_extend(32, load18_1:bv32); - var R0_7:bv64 := zero_extend(32, bvconcat(0x0:bv31, extract(1,0, R0_6:bv64))); - var #5_1:bv32 := bvadd(extract(32,0, R0_7:bv64), 0xffffffff:bv32); - var VF_2:bv1 := bvnot(booltobv1(eq(sign_extend(1, bvadd(#5_1:bv32, 0x1:bv32)), - sign_extend(1, extract(32,0, R0_7:bv64))))); - var CF_2:bv1 := bvnot(booltobv1(eq(zero_extend(1, bvadd(#5_1:bv32, 0x1:bv32)), - bvadd(zero_extend(1, extract(32,0, R0_7:bv64)), 0x100000000:bv33)))); - var ZF_2:bv1 := booltobv1(eq(bvadd(#5_1:bv32, 0x1:bv32), 0x0:bv32)); - var NF_2:bv1 := extract(32,31, bvadd(#5_1:bv32, 0x1:bv32)); + var R0_5:bv64 := bvadd(R0_4, 0x40:bv64); + var load18_1:bv32 := load le $mem:(bv64->bv8) R0_5 32; + var R0_6:bv64 := zero_extend(32, load18_1); + var R0_7:bv64 := zero_extend(32, bvconcat(0x0:bv31, extract(1,0, R0_6))); + var #5_1:bv32 := bvadd(extract(32,0, R0_7), 0xffffffff:bv32); + var VF_2:bv1 := bvnot(booltobv1(eq(sign_extend(1, bvadd(#5_1, 0x1:bv32)), + sign_extend(1, extract(32,0, R0_7))))); + var CF_2:bv1 := bvnot(booltobv1(eq(zero_extend(1, bvadd(#5_1, 0x1:bv32)), + bvadd(zero_extend(1, extract(32,0, R0_7)), 0x100000000:bv33)))); + var ZF_2:bv1 := booltobv1(eq(bvadd(#5_1, 0x1:bv32), 0x0:bv32)); + var NF_2:bv1 := extract(32,31, bvadd(#5_1, 0x1:bv32)); goto (%main_27,%main_23); ]; block %main_23 [ - var ZF_4:bv1 := ZF_2:bv1; - guard neq(booltobv1(eq(ZF_4:bv1, 0x1:bv1)), 0x0:bv1); + var ZF_4:bv1 := ZF_2; + guard neq(booltobv1(eq(ZF_4, 0x1:bv1)), 0x0:bv1); goto (%main_21); ]; block %main_21 [ goto (%main_19); ]; block %main_27 [ - var ZF_3:bv1 := ZF_2:bv1; - guard eq(booltobv1(eq(ZF_3:bv1, 0x1:bv1)), 0x0:bv1); + var ZF_3:bv1 := ZF_2; + guard eq(booltobv1(eq(ZF_3, 0x1:bv1)), 0x0:bv1); goto (%main_25); ]; block %main_25 [ goto (%main_5); ]; @@ -201,25 +199,24 @@ Run on basic irreducible loop example var ZF_9:bv1 := phi(%main_25 -> ZF_3:bv1, %main_7 -> ZF_8:bv1) ) [ var R0_14:bv64 := 0x0:bv64; - var R0_15:bv64 := bvadd(R0_14:bv64, 0x820:bv64); + var R0_15:bv64 := bvadd(R0_14, 0x820:bv64); var R30_4:bv64 := 0x7a0:bv64; (var CF_7:bv1=CF_out, var NF_7:bv1=NF_out, var R0_16:bv64=R0_out, var R1_5:bv64=R1_out, var R29_6:bv64=R29_out, var R30_5:bv64=R30_out, var R31_6:bv64=R31_out, var VF_7:bv1=VF_out, var ZF_10:bv1=ZF_out) := - call @puts_1584(CF_in=CF_6:bv1, NF_in=NF_6:bv1, R0_in=R0_15:bv64, - R1_in=R1_4:bv64, R29_in=R29_5:bv64, R30_in=R30_4:bv64, R31_in=R31_5:bv64, - VF_in=VF_6:bv1, ZF_in=ZF_9:bv1); + call @puts_1584(CF_in=CF_6, NF_in=NF_6, R0_in=R0_15, R1_in=R1_4, R29_in=R29_5, + R30_in=R30_4, R31_in=R31_5, VF_in=VF_6, ZF_in=ZF_9); goto (%main_3); ]; block %main_3 [ var R0_17:bv64 := 0x20000:bv64; - var R0_18:bv64 := bvadd(R0_17:bv64, 0x3c:bv64); - var load19_1:bv32 := load le $mem:(bv64->bv8) R0_18:bv64 32; - var R0_19:bv64 := zero_extend(32, load19_1:bv32); - var R1_6:bv64 := zero_extend(32, bvadd(extract(32,0, R0_19:bv64), 0x1:bv32)); + var R0_18:bv64 := bvadd(R0_17, 0x3c:bv64); + var load19_1:bv32 := load le $mem:(bv64->bv8) R0_18 32; + var R0_19:bv64 := zero_extend(32, load19_1); + var R1_6:bv64 := zero_extend(32, bvadd(extract(32,0, R0_19), 0x1:bv32)); var R0_20:bv64 := 0x20000:bv64; - var R0_21:bv64 := bvadd(R0_20:bv64, 0x3c:bv64); - $mem:(bv64->bv8) := store le $mem:(bv64->bv8) R0_21:bv64 extract(32,0, R1_6:bv64) 32; + var R0_21:bv64 := bvadd(R0_20, 0x3c:bv64); + $mem:(bv64->bv8) := store le $mem:(bv64->bv8) R0_21 extract(32,0, R1_6) 32; goto (%main_19); ]; block %main_19 ( @@ -232,67 +229,64 @@ Run on basic irreducible loop example var ZF_5:bv1 := phi(%main_3 -> ZF_10:bv1, %main_21 -> ZF_4:bv1) ) [ var R0_8:bv64 := 0x0:bv64; - var R0_9:bv64 := bvadd(R0_8:bv64, 0x820:bv64); + var R0_9:bv64 := bvadd(R0_8, 0x820:bv64); var R30_2:bv64 := 0x7d0:bv64; (var CF_4:bv1=CF_out, var NF_4:bv1=NF_out, var R0_10:bv64=R0_out, var R1_3:bv64=R1_out, var R29_4:bv64=R29_out, var R30_3:bv64=R30_out, var R31_4:bv64=R31_out, var VF_4:bv1=VF_out, var ZF_6:bv1=ZF_out) := - call @puts_1584(CF_in=CF_3:bv1, NF_in=NF_3:bv1, R0_in=R0_9:bv64, - R1_in=R1_2:bv64, R29_in=R29_3:bv64, R30_in=R30_2:bv64, R31_in=R31_3:bv64, - VF_in=VF_3:bv1, ZF_in=ZF_5:bv1); + call @puts_1584(CF_in=CF_3, NF_in=NF_3, R0_in=R0_9, R1_in=R1_2, R29_in=R29_3, + R30_in=R30_2, R31_in=R31_3, VF_in=VF_3, ZF_in=ZF_5); goto (%main_17); ]; block %main_17 [ var R0_11:bv64 := 0x20000:bv64; - var R0_12:bv64 := bvadd(R0_11:bv64, 0x3c:bv64); - var load20_1:bv32 := load le $mem:(bv64->bv8) R0_12:bv64 32; - var R0_13:bv64 := zero_extend(32, load20_1:bv32); - var #6_1:bv32 := bvadd(extract(32,0, R0_13:bv64), 0xfffffffa:bv32); - var VF_5:bv1 := bvnot(booltobv1(eq(sign_extend(1, bvadd(#6_1:bv32, 0x1:bv32)), - bvadd(sign_extend(1, extract(32,0, R0_13:bv64)), 0x1fffffffb:bv33)))); - var CF_5:bv1 := bvnot(booltobv1(eq(zero_extend(1, bvadd(#6_1:bv32, 0x1:bv32)), - bvadd(zero_extend(1, extract(32,0, R0_13:bv64)), 0xfffffffb:bv33)))); - var ZF_7:bv1 := booltobv1(eq(bvadd(#6_1:bv32, 0x1:bv32), 0x0:bv32)); - var NF_5:bv1 := extract(32,31, bvadd(#6_1:bv32, 0x1:bv32)); + var R0_12:bv64 := bvadd(R0_11, 0x3c:bv64); + var load20_1:bv32 := load le $mem:(bv64->bv8) R0_12 32; + var R0_13:bv64 := zero_extend(32, load20_1); + var #6_1:bv32 := bvadd(extract(32,0, R0_13), 0xfffffffa:bv32); + var VF_5:bv1 := bvnot(booltobv1(eq(sign_extend(1, bvadd(#6_1, 0x1:bv32)), + bvadd(sign_extend(1, extract(32,0, R0_13)), 0x1fffffffb:bv33)))); + var CF_5:bv1 := bvnot(booltobv1(eq(zero_extend(1, bvadd(#6_1, 0x1:bv32)), + bvadd(zero_extend(1, extract(32,0, R0_13)), 0xfffffffb:bv33)))); + var ZF_7:bv1 := booltobv1(eq(bvadd(#6_1, 0x1:bv32), 0x0:bv32)); + var NF_5:bv1 := extract(32,31, bvadd(#6_1, 0x1:bv32)); goto (%main_15,%main_9); ]; block %main_9 [ - var ZF_8:bv1 := ZF_7:bv1; - guard neq(bvnot(booltobv1(eq(ZF_8:bv1, 0x1:bv1))), 0x0:bv1); + var ZF_8:bv1 := ZF_7; + guard neq(bvnot(booltobv1(eq(ZF_8, 0x1:bv1))), 0x0:bv1); goto (%main_7); ]; block %main_7 [ goto (%main_5); ]; block %main_15 [ - var ZF_11:bv1 := ZF_7:bv1; - guard eq(bvnot(booltobv1(eq(ZF_11:bv1, 0x1:bv1))), 0x0:bv1); + var ZF_11:bv1 := ZF_7; + guard eq(bvnot(booltobv1(eq(ZF_11, 0x1:bv1))), 0x0:bv1); var R0_22:bv64 := 0x0:bv64; - var R0_23:bv64 := bvadd(R0_22:bv64, 0x828:bv64); + var R0_23:bv64 := bvadd(R0_22, 0x828:bv64); var R30_6:bv64 := 0x7f4:bv64; (var CF_8:bv1=CF_out, var NF_8:bv1=NF_out, var R0_24:bv64=R0_out, var R1_7:bv64=R1_out, var R29_7:bv64=R29_out, var R30_7:bv64=R30_out, var R31_7:bv64=R31_out, var VF_8:bv1=VF_out, var ZF_12:bv1=ZF_out) := - call @puts_1584(CF_in=CF_5:bv1, NF_in=NF_5:bv1, R0_in=R0_23:bv64, - R1_in=R1_3:bv64, R29_in=R29_4:bv64, R30_in=R30_6:bv64, R31_in=R31_4:bv64, - VF_in=VF_5:bv1, ZF_in=ZF_11:bv1); + call @puts_1584(CF_in=CF_5, NF_in=NF_5, R0_in=R0_23, R1_in=R1_3, R29_in=R29_4, + R30_in=R30_6, R31_in=R31_4, VF_in=VF_5, ZF_in=ZF_11); goto (%main_13); ]; block %main_13 [ goto (%main_11); ]; block %main_11 [ var R0_25:bv64 := 0x0:bv64; - var load21_1:bv64 := load le $stack:(bv64->bv8) R31_7:bv64 64; - var R29_8:bv64 := load21_1:bv64; - var load22_1:bv64 := load le $stack:(bv64->bv8) bvadd(R31_7:bv64, 0x8:bv64) 64; - var R30_8:bv64 := load22_1:bv64; - var R31_8:bv64 := bvadd(R31_7:bv64, 0x20:bv64); + var load21_1:bv64 := load le $stack:(bv64->bv8) R31_7 64; + var R29_8:bv64 := load21_1; + var load22_1:bv64 := load le $stack:(bv64->bv8) bvadd(R31_7, 0x8:bv64) 64; + var R30_8:bv64 := load22_1; + var R31_8:bv64 := bvadd(R31_7, 0x20:bv64); goto (%main_basil_return_1); ]; block %main_basil_return_1 [ goto (%returns); ]; block %returns [ - (var CF_out:bv1 := CF_8:bv1, var NF_out:bv1 := NF_8:bv1, - var R0_out:bv64 := R0_25:bv64, var R1_out:bv64 := R1_7:bv64, - var R29_out:bv64 := R29_8:bv64, var R30_out:bv64 := R30_8:bv64, - var R31_out:bv64 := R31_8:bv64, var VF_out:bv1 := VF_8:bv1, - var ZF_out:bv1 := ZF_12:bv1); + (var CF_out:bv1 := CF_8, var NF_out:bv1 := NF_8, var R0_out:bv64 := R0_25, + var R1_out:bv64 := R1_7, var R29_out:bv64 := R29_8, + var R30_out:bv64 := R30_8, var R31_out:bv64 := R31_8, var VF_out:bv1 := VF_8, + var ZF_out:bv1 := ZF_12); return; ] ]; @@ -312,7 +306,7 @@ Run on basic irreducible loop example --- > modifies $mem:(bv64->bv8), $stack:(bv64->bv8), $mem:(bv64->bv8) > captures $mem:(bv64->bv8), $stack:(bv64->bv8), $mem:(bv64->bv8) - 168,169c168,169 + 162,163c162,163 < modifies $mem:(bv64->bv8), $stack:(bv64->bv8) < captures $mem:(bv64->bv8), $stack:(bv64->bv8) --- @@ -343,7 +337,7 @@ Multiple loops dependencies of loops etc are handled correctly > proc @main(R0_in:bv64) -> (R0_out:bv64) { } > 7a6 - > block %inputs [ var R0_1:bv64 := R0_in:bv64; goto (%e); ]; + > block %inputs [ var R0_1:bv64 := R0_in; goto (%e); ]; 9,12c8,16 < block %e1 [ $R0:bv64 := 0x1:bv64; goto (%e2); ]; < block %e2 [ goto (%e4,%e1); ]; @@ -358,5 +352,5 @@ Multiple loops dependencies of loops etc are handled correctly > block %e4 ( > var R0_5:bv64 := phi(%e2 -> R0_4:bv64, %e3 -> R0_2:bv64, %e2 -> R0_4:bv64) > ) [ goto (%returns); ]; - > block %returns [ var R0_out:bv64 := R0_5:bv64; return; ] + > block %returns [ var R0_out:bv64 := R0_5; return; ] [1] diff --git a/test/cram/dune b/test/cram/dune index fc2c9272..b1c060ef 100644 --- a/test/cram/dune +++ b/test/cram/dune @@ -8,7 +8,7 @@ concat.il)) (cram - (applies_to * \ expr_smt) + (applies_to * \ expr_smt malloc_free) (deps loop_dfg.sexp ../../examples/loop.il @@ -37,3 +37,13 @@ ll_spec.il ll_spec.sexp ../../bin/main.exe)) + +(cram + (applies_to malloc_free) + (enabled_if + (and %{bin-available:boogie} %{bin-available:cvc5})) + (deps + %{bin:bincaml} + ../../examples/memory/malloc_free.il + ../../examples/memory/malloc_free_oob.il + ./malloc_free.sexp)) diff --git a/test/cram/expr_smt.t b/test/cram/expr_smt.t index f257ff1d..36afcb63 100644 --- a/test/cram/expr_smt.t +++ b/test/cram/expr_smt.t @@ -7,74 +7,72 @@ Should output no errors Check concat rewrites work $ diff before.il after.il - 17,81c17,18 - < $R28:bv64 := bvor(bvand(bvconcat(extract(1,0, bvlshr(var1_4206396_bv64:bv64, - < 0x1f:bv64)), extract(1,0, bvlshr(var1_4206396_bv64:bv64, 0x1f:bv64)), - < extract(1,0, bvlshr(var1_4206396_bv64:bv64, 0x1f:bv64)), - < extract(1,0, bvlshr(var1_4206396_bv64:bv64, 0x1f:bv64)), - < extract(1,0, bvlshr(var1_4206396_bv64:bv64, 0x1f:bv64)), - < extract(1,0, bvlshr(var1_4206396_bv64:bv64, 0x1f:bv64)), - < extract(1,0, bvlshr(var1_4206396_bv64:bv64, 0x1f:bv64)), - < extract(1,0, bvlshr(var1_4206396_bv64:bv64, 0x1f:bv64)), - < extract(1,0, bvlshr(var1_4206396_bv64:bv64, 0x1f:bv64)), - < extract(1,0, bvlshr(var1_4206396_bv64:bv64, 0x1f:bv64)), - < extract(1,0, bvlshr(var1_4206396_bv64:bv64, 0x1f:bv64)), - < extract(1,0, bvlshr(var1_4206396_bv64:bv64, 0x1f:bv64)), - < extract(1,0, bvlshr(var1_4206396_bv64:bv64, 0x1f:bv64)), - < extract(1,0, bvlshr(var1_4206396_bv64:bv64, 0x1f:bv64)), - < extract(1,0, bvlshr(var1_4206396_bv64:bv64, 0x1f:bv64)), - < extract(1,0, bvlshr(var1_4206396_bv64:bv64, 0x1f:bv64)), - < extract(1,0, bvlshr(var1_4206396_bv64:bv64, 0x1f:bv64)), - < extract(1,0, bvlshr(var1_4206396_bv64:bv64, 0x1f:bv64)), - < extract(1,0, bvlshr(var1_4206396_bv64:bv64, 0x1f:bv64)), - < extract(1,0, bvlshr(var1_4206396_bv64:bv64, 0x1f:bv64)), - < extract(1,0, bvlshr(var1_4206396_bv64:bv64, 0x1f:bv64)), - < extract(1,0, bvlshr(var1_4206396_bv64:bv64, 0x1f:bv64)), - < extract(1,0, bvlshr(var1_4206396_bv64:bv64, 0x1f:bv64)), - < extract(1,0, bvlshr(var1_4206396_bv64:bv64, 0x1f:bv64)), - < extract(1,0, bvlshr(var1_4206396_bv64:bv64, 0x1f:bv64)), - < extract(1,0, bvlshr(var1_4206396_bv64:bv64, 0x1f:bv64)), - < extract(1,0, bvlshr(var1_4206396_bv64:bv64, 0x1f:bv64)), - < extract(1,0, bvlshr(var1_4206396_bv64:bv64, 0x1f:bv64)), - < extract(1,0, bvlshr(var1_4206396_bv64:bv64, 0x1f:bv64)), - < extract(1,0, bvlshr(var1_4206396_bv64:bv64, 0x1f:bv64)), - < extract(1,0, bvlshr(var1_4206396_bv64:bv64, 0x1f:bv64)), - < extract(1,0, bvlshr(var1_4206396_bv64:bv64, 0x1f:bv64)), - < extract(1,0, bvlshr(var1_4206396_bv64:bv64, 0x1f:bv64)), - < extract(1,0, bvlshr(var1_4206396_bv64:bv64, 0x1f:bv64)), - < extract(1,0, bvlshr(var1_4206396_bv64:bv64, 0x1f:bv64)), - < extract(1,0, bvlshr(var1_4206396_bv64:bv64, 0x1f:bv64)), - < extract(1,0, bvlshr(var1_4206396_bv64:bv64, 0x1f:bv64)), - < extract(1,0, bvlshr(var1_4206396_bv64:bv64, 0x1f:bv64)), - < extract(1,0, bvlshr(var1_4206396_bv64:bv64, 0x1f:bv64)), - < extract(1,0, bvlshr(var1_4206396_bv64:bv64, 0x1f:bv64)), - < extract(1,0, bvlshr(var1_4206396_bv64:bv64, 0x1f:bv64)), - < extract(1,0, bvlshr(var1_4206396_bv64:bv64, 0x1f:bv64)), - < extract(1,0, bvlshr(var1_4206396_bv64:bv64, 0x1f:bv64)), - < extract(1,0, bvlshr(var1_4206396_bv64:bv64, 0x1f:bv64)), - < extract(1,0, bvlshr(var1_4206396_bv64:bv64, 0x1f:bv64)), - < extract(1,0, bvlshr(var1_4206396_bv64:bv64, 0x1f:bv64)), - < extract(1,0, bvlshr(var1_4206396_bv64:bv64, 0x1f:bv64)), - < extract(1,0, bvlshr(var1_4206396_bv64:bv64, 0x1f:bv64)), - < extract(1,0, bvlshr(var1_4206396_bv64:bv64, 0x1f:bv64)), - < extract(1,0, bvlshr(var1_4206396_bv64:bv64, 0x1f:bv64)), - < extract(1,0, bvlshr(var1_4206396_bv64:bv64, 0x1f:bv64)), - < extract(1,0, bvlshr(var1_4206396_bv64:bv64, 0x1f:bv64)), - < extract(1,0, bvlshr(var1_4206396_bv64:bv64, 0x1f:bv64)), - < extract(1,0, bvlshr(var1_4206396_bv64:bv64, 0x1f:bv64)), - < extract(1,0, bvlshr(var1_4206396_bv64:bv64, 0x1f:bv64)), - < extract(1,0, bvlshr(var1_4206396_bv64:bv64, 0x1f:bv64)), - < extract(1,0, bvlshr(var1_4206396_bv64:bv64, 0x1f:bv64)), - < extract(1,0, bvlshr(var1_4206396_bv64:bv64, 0x1f:bv64)), - < extract(1,0, bvlshr(var1_4206396_bv64:bv64, 0x1f:bv64)), - < extract(1,0, bvlshr(var1_4206396_bv64:bv64, 0x1f:bv64)), - < extract(1,0, bvlshr(var1_4206396_bv64:bv64, 0x1f:bv64)), - < extract(1,0, bvlshr(var1_4206396_bv64:bv64, 0x1f:bv64)), - < extract(1,0, bvlshr(var1_4206396_bv64:bv64, 0x1f:bv64)), - < extract(1,0, bvlshr(var1_4206396_bv64:bv64, 0x1f:bv64))), - < 0xffffffff00000000:bv64), + 17,80c17 + < $R28:bv64 := bvor(bvand(bvconcat(extract(1,0, bvlshr(var1_4206396_bv64, + < 0x1f:bv64)), extract(1,0, bvlshr(var1_4206396_bv64, 0x1f:bv64)), + < extract(1,0, bvlshr(var1_4206396_bv64, 0x1f:bv64)), + < extract(1,0, bvlshr(var1_4206396_bv64, 0x1f:bv64)), + < extract(1,0, bvlshr(var1_4206396_bv64, 0x1f:bv64)), + < extract(1,0, bvlshr(var1_4206396_bv64, 0x1f:bv64)), + < extract(1,0, bvlshr(var1_4206396_bv64, 0x1f:bv64)), + < extract(1,0, bvlshr(var1_4206396_bv64, 0x1f:bv64)), + < extract(1,0, bvlshr(var1_4206396_bv64, 0x1f:bv64)), + < extract(1,0, bvlshr(var1_4206396_bv64, 0x1f:bv64)), + < extract(1,0, bvlshr(var1_4206396_bv64, 0x1f:bv64)), + < extract(1,0, bvlshr(var1_4206396_bv64, 0x1f:bv64)), + < extract(1,0, bvlshr(var1_4206396_bv64, 0x1f:bv64)), + < extract(1,0, bvlshr(var1_4206396_bv64, 0x1f:bv64)), + < extract(1,0, bvlshr(var1_4206396_bv64, 0x1f:bv64)), + < extract(1,0, bvlshr(var1_4206396_bv64, 0x1f:bv64)), + < extract(1,0, bvlshr(var1_4206396_bv64, 0x1f:bv64)), + < extract(1,0, bvlshr(var1_4206396_bv64, 0x1f:bv64)), + < extract(1,0, bvlshr(var1_4206396_bv64, 0x1f:bv64)), + < extract(1,0, bvlshr(var1_4206396_bv64, 0x1f:bv64)), + < extract(1,0, bvlshr(var1_4206396_bv64, 0x1f:bv64)), + < extract(1,0, bvlshr(var1_4206396_bv64, 0x1f:bv64)), + < extract(1,0, bvlshr(var1_4206396_bv64, 0x1f:bv64)), + < extract(1,0, bvlshr(var1_4206396_bv64, 0x1f:bv64)), + < extract(1,0, bvlshr(var1_4206396_bv64, 0x1f:bv64)), + < extract(1,0, bvlshr(var1_4206396_bv64, 0x1f:bv64)), + < extract(1,0, bvlshr(var1_4206396_bv64, 0x1f:bv64)), + < extract(1,0, bvlshr(var1_4206396_bv64, 0x1f:bv64)), + < extract(1,0, bvlshr(var1_4206396_bv64, 0x1f:bv64)), + < extract(1,0, bvlshr(var1_4206396_bv64, 0x1f:bv64)), + < extract(1,0, bvlshr(var1_4206396_bv64, 0x1f:bv64)), + < extract(1,0, bvlshr(var1_4206396_bv64, 0x1f:bv64)), + < extract(1,0, bvlshr(var1_4206396_bv64, 0x1f:bv64)), + < extract(1,0, bvlshr(var1_4206396_bv64, 0x1f:bv64)), + < extract(1,0, bvlshr(var1_4206396_bv64, 0x1f:bv64)), + < extract(1,0, bvlshr(var1_4206396_bv64, 0x1f:bv64)), + < extract(1,0, bvlshr(var1_4206396_bv64, 0x1f:bv64)), + < extract(1,0, bvlshr(var1_4206396_bv64, 0x1f:bv64)), + < extract(1,0, bvlshr(var1_4206396_bv64, 0x1f:bv64)), + < extract(1,0, bvlshr(var1_4206396_bv64, 0x1f:bv64)), + < extract(1,0, bvlshr(var1_4206396_bv64, 0x1f:bv64)), + < extract(1,0, bvlshr(var1_4206396_bv64, 0x1f:bv64)), + < extract(1,0, bvlshr(var1_4206396_bv64, 0x1f:bv64)), + < extract(1,0, bvlshr(var1_4206396_bv64, 0x1f:bv64)), + < extract(1,0, bvlshr(var1_4206396_bv64, 0x1f:bv64)), + < extract(1,0, bvlshr(var1_4206396_bv64, 0x1f:bv64)), + < extract(1,0, bvlshr(var1_4206396_bv64, 0x1f:bv64)), + < extract(1,0, bvlshr(var1_4206396_bv64, 0x1f:bv64)), + < extract(1,0, bvlshr(var1_4206396_bv64, 0x1f:bv64)), + < extract(1,0, bvlshr(var1_4206396_bv64, 0x1f:bv64)), + < extract(1,0, bvlshr(var1_4206396_bv64, 0x1f:bv64)), + < extract(1,0, bvlshr(var1_4206396_bv64, 0x1f:bv64)), + < extract(1,0, bvlshr(var1_4206396_bv64, 0x1f:bv64)), + < extract(1,0, bvlshr(var1_4206396_bv64, 0x1f:bv64)), + < extract(1,0, bvlshr(var1_4206396_bv64, 0x1f:bv64)), + < extract(1,0, bvlshr(var1_4206396_bv64, 0x1f:bv64)), + < extract(1,0, bvlshr(var1_4206396_bv64, 0x1f:bv64)), + < extract(1,0, bvlshr(var1_4206396_bv64, 0x1f:bv64)), + < extract(1,0, bvlshr(var1_4206396_bv64, 0x1f:bv64)), + < extract(1,0, bvlshr(var1_4206396_bv64, 0x1f:bv64)), + < extract(1,0, bvlshr(var1_4206396_bv64, 0x1f:bv64)), + < extract(1,0, bvlshr(var1_4206396_bv64, 0x1f:bv64)), + < extract(1,0, bvlshr(var1_4206396_bv64, 0x1f:bv64)), + < extract(1,0, bvlshr(var1_4206396_bv64, 0x1f:bv64))), --- - > $R28:bv64 := bvor(bvand(sign_extend(63, - > extract(32,31, var1_4206396_bv64:bv64)), 0xffffffff00000000:bv64), + > $R28:bv64 := bvor(bvand(sign_extend(63, extract(32,31, var1_4206396_bv64)), [1] diff --git a/test/cram/gammavars.t b/test/cram/gammavars.t index 14fa1206..3cfdb00e 100644 --- a/test/cram/gammavars.t +++ b/test/cram/gammavars.t @@ -8,94 +8,90 @@ < proc @main() -> (out:bv64) { } < modifies $x:bv64 < captures $x:bv64 - < requires gamma($x:bv64) - < ensures gamma($x:bv64) + < requires gamma($x) + < ensures gamma($x) --- > proc @main() -> (Gamma_out:bool, out:bv64) { } > modifies Gamma_$x:bool, $x:bv64 > captures Gamma_$x:bool, $x:bv64 - > requires Gamma_$x:bool - > ensures Gamma_$x:bool - 11,12c12,13 - < ($x:bv64=out) := - < call @f(z=$x:bv64); + > requires Gamma_$x + > ensures Gamma_$x + 10,11c11,19 + < block %main_entry [ ($x:bv64=out) := call @f(z=$x); goto (%main_return); ]; + < block %main_return [ var out:bv64 := $x; return; ] --- + > block %main_entry [ > (Gamma_$x:bool=Gamma_out, $x:bv64=out) := - > call @f(Gamma_z=Gamma_$x:bool, z=$x:bv64); - 15c16,19 - < block %main_return [ var out:bv64 := $x:bv64; return; ] - --- + > call @f(Gamma_z=Gamma_$x, z=$x); + > goto (%main_return); + > ]; > block %main_return [ - > (var Gamma_out:bool := Gamma_$x:bool, var out:bv64 := $x:bv64); + > (var Gamma_out:bool := Gamma_$x, var out:bv64 := $x); > return; > ] - 17,19c21,23 + 13,15c21,23 < proc @f(z:bv64) -> (out:bv64) { } - < requires gamma(z:bv64) - < ensures eq(gamma(out:bv64), old(gamma(z:bv64))) + < requires gamma(z) + < ensures eq(gamma(out), old(gamma(z))) --- > proc @f(Gamma_z:bool, z:bv64) -> (Gamma_out:bool, out:bv64) { } - > requires Gamma_z:bool - > ensures eq(Gamma_out:bool, old(Gamma_z:bool)) - 23,25c27,30 + > requires Gamma_z + > ensures eq(Gamma_out, old(Gamma_z)) + 19,21c27,29 < (var out:bv64=out) := - < call @h(a=z:bv64, b=bvmul(z:bv64, z:bv64)); - < var out:bv64 := out:bv64; + < call @h(a=z, b=bvmul(z, z)); + < var out:bv64 := out; --- > (var Gamma_out:bool=Gamma_out, var out:bv64=out) := - > call @h(Gamma_a=Gamma_z:bool, Gamma_b=Gamma_z:bool, a=z:bv64, - > b=bvmul(z:bv64, z:bv64)); - > (var Gamma_out:bool := Gamma_out:bool, var out:bv64 := out:bv64); - 29,31c34,36 + > call @h(Gamma_a=Gamma_z, Gamma_b=Gamma_z, a=z, b=bvmul(z, z)); + > (var Gamma_out:bool := Gamma_out, var out:bv64 := out); + 25,27c33,35 < proc @g(a:bv64) -> (out:bv64) { } - < requires gamma(a:bv64) - < ensures eq(gamma(out:bv64), old(gamma(a:bv64))) + < requires gamma(a) + < ensures eq(gamma(out), old(gamma(a))) --- > proc @g(Gamma_a:bool, a:bv64) -> (Gamma_out:bool, out:bv64) { } - > requires Gamma_a:bool - > ensures eq(Gamma_out:bool, old(Gamma_a:bool)) - 35,37c40,43 + > requires Gamma_a + > ensures eq(Gamma_out, old(Gamma_a)) + 31,33c39,41 < (var out:bv64=out) := - < call @h(a=a:bv64, b=bvsub(a:bv64, 0x1:bv64)); - < var out:bv64 := out:bv64; + < call @h(a=a, b=bvsub(a, 0x1:bv64)); + < var out:bv64 := out; --- > (var Gamma_out:bool=Gamma_out, var out:bv64=out) := - > call @h(Gamma_a=Gamma_a:bool, Gamma_b=Gamma_a:bool, a=a:bv64, - > b=bvsub(a:bv64, 0x1:bv64)); - > (var Gamma_out:bool := Gamma_out:bool, var out:bv64 := out:bv64); - 41,44c47,50 + > call @h(Gamma_a=Gamma_a, Gamma_b=Gamma_a, a=a, b=bvsub(a, 0x1:bv64)); + > (var Gamma_out:bool := Gamma_out, var out:bv64 := out); + 37,39c45,47 < proc @h(a:bv64, b:bv64) -> (out:bv64) { } - < requires booland(gamma(a:bv64), gamma(b:bv64)) - < ensures boolor(boolnot(booland(old(gamma(a:bv64)), old(gamma(b:bv64)))), - < gamma(out:bv64)) + < requires booland(gamma(a), gamma(b)) + < ensures boolor(boolnot(booland(old(gamma(a)), old(gamma(b)))), gamma(out)) --- > proc @h(Gamma_a:bool, Gamma_b:bool, a:bv64, b:bv64) -> (Gamma_out:bool, out:bv64) { } - > requires booland(Gamma_a:bool, Gamma_b:bool) - > ensures boolor(boolnot(booland(old(Gamma_a:bool), old(Gamma_b:bool))), - > Gamma_out:bool) - 49c55 - < assert gamma(a:bv64); + > requires booland(Gamma_a, Gamma_b) + > ensures boolor(boolnot(booland(old(Gamma_a), old(Gamma_b))), Gamma_out) + 44c52 + < assert gamma(a); --- - > assert Gamma_a:bool; - 51c57 - < var c:bv64 := b:bv64; + > assert Gamma_a; + 46c54 + < var c:bv64 := b; --- - > (var Gamma_c:bool := Gamma_b:bool, var c:bv64 := b:bv64); - 55c61 - < assert gamma(a:bv64); + > (var Gamma_c:bool := Gamma_b, var c:bv64 := b); + 50c58 + < assert gamma(a); --- - > assert Gamma_a:bool; - 57,58c63,64 + > assert Gamma_a; + 52,53c60,61 < (var c:bv64=out) := - < call @g(a=bvadd(a:bv64, b:bv64)); + < call @g(a=bvadd(a, b)); --- > (var Gamma_c:bool=Gamma_out, var c:bv64=out) := - > call @g(Gamma_a=booland(Gamma_a:bool, Gamma_b:bool), a=bvadd(a:bv64, b:bv64)); - 61c67,70 - < block %h_return [ var out:bv64 := bvadd(c:bv64, 0x1:bv64); return; ] + > call @g(Gamma_a=booland(Gamma_a, Gamma_b), a=bvadd(a, b)); + 56c64,67 + < block %h_return [ var out:bv64 := bvadd(c, 0x1:bv64); return; ] --- > block %h_return [ - > (var Gamma_out:bool := Gamma_c:bool, var out:bv64 := bvadd(c:bv64, 0x1:bv64)); + > (var Gamma_out:bool := Gamma_c, var out:bv64 := bvadd(c, 0x1:bv64)); > return; > ] [1] diff --git a/test/cram/inter_dead.t b/test/cram/inter_dead.t index 46d002f2..462408cb 100644 --- a/test/cram/inter_dead.t +++ b/test/cram/inter_dead.t @@ -9,13 +9,13 @@ [ block %main_entry [ - (var a:bv64 := inp:bv64, var b:bv64 := inp:bv64); + (var a:bv64 := inp, var b:bv64 := inp); (var a:bv64=out) := - call @fun1(c=a:bv64, d=b:bv64); + call @fun1(c=a, d=b); (var x:bv64=out) := - call @fun1(c=a:bv64, d=b:bv64); - assert eq(x:bv64, bvadd(a:bv64, a:bv64)); - assert eq(y:bv64, 0); + call @fun1(c=a, d=b); + assert eq(x, bvadd(a, a)); + assert eq(y, 0); nop; return; ] @@ -26,8 +26,8 @@ [ block %fun1_entry [ (var e:bv64=out2) := - call @fun2(f=d:bv64); - var out:bv64 := bvadd(c:bv64, e:bv64); + call @fun2(f=d); + var out:bv64 := bvadd(c, e); return; ] ]; @@ -36,8 +36,8 @@ [ block %fun2_entry [ - var g:bv64 := $global:bv64; - var out2:bv64 := bvadd(g:bv64, g:bv64); + var g:bv64 := $global; + var out2:bv64 := bvadd(g, g); return; ] ]; @@ -50,13 +50,13 @@ [ block %main_entry [ - (var a:bv64 := inp:bv64, var b:bv64 := inp:bv64); + (var a:bv64 := inp, var b:bv64 := inp); (var a:bv64=out) := - call @fun1(c=a:bv64, d=b:bv64); + call @fun1(c=a, d=b); (var x:bv64=out) := - call @fun1(c=a:bv64, d=b:bv64); - assert eq(x:bv64, bvadd(a:bv64, a:bv64)); - assert eq(y:bv64, 0); + call @fun1(c=a, d=b); + assert eq(x, bvadd(a, a)); + assert eq(y, 0); return; ] ]; @@ -66,8 +66,8 @@ [ block %fun1_entry [ (var e:bv64=out2) := - call @fun2(f=d:bv64); - var out:bv64 := bvadd(c:bv64, e:bv64); + call @fun2(f=d); + var out:bv64 := bvadd(c, e); return; ] ]; @@ -76,8 +76,8 @@ [ block %fun2_entry [ - var g:bv64 := $global:bv64; - var out2:bv64 := bvadd(g:bv64, g:bv64); + var g:bv64 := $global; + var out2:bv64 := bvadd(g, g); return; ] ]; @@ -90,13 +90,13 @@ [ block %main_entry [ - var a:bv64 := inp:bv64; + var a:bv64 := inp; (var a:bv64=out) := - call @fun1(c=a:bv64); + call @fun1(c=a); (var x:bv64=out) := - call @fun1(c=a:bv64); - assert eq(x:bv64, bvadd(a:bv64, a:bv64)); - assert eq(y:bv64, 0); + call @fun1(c=a); + assert eq(x, bvadd(a, a)); + assert eq(y, 0); return; ] ]; @@ -107,7 +107,7 @@ block %fun1_entry [ (var e:bv64=out2) := call @fun2(); - var out:bv64 := bvadd(c:bv64, e:bv64); + var out:bv64 := bvadd(c, e); return; ] ]; @@ -116,25 +116,25 @@ [ block %fun2_entry [ - var g:bv64 := $global:bv64; - var out2:bv64 := bvadd(g:bv64, g:bv64); + var g:bv64 := $global; + var out2:bv64 := bvadd(g, g); return; ] ]; $ diff inter.il intra.il 8c8 - < var a:bv64 := inp:bv64; + < var a:bv64 := inp; --- - > (var a:bv64 := inp:bv64, var b:bv64 := inp:bv64); + > (var a:bv64 := inp, var b:bv64 := inp); 10c10 - < call @fun1(c=a:bv64); + < call @fun1(c=a); --- - > call @fun1(c=a:bv64, d=b:bv64); + > call @fun1(c=a, d=b); 12c12 - < call @fun1(c=a:bv64); + < call @fun1(c=a); --- - > call @fun1(c=a:bv64, d=b:bv64); + > call @fun1(c=a, d=b); 18c18 < proc @fun1(c:bv64) -> (out:bv64) { } --- @@ -142,7 +142,7 @@ 24c24 < call @fun2(); --- - > call @fun2(f=d:bv64); + > call @fun2(f=d); 29c29 < proc @fun2() -> (out2:bv64) { } --- diff --git a/test/cram/lambdalifting.t b/test/cram/lambdalifting.t index 9d7c5877..2ec246c9 100644 --- a/test/cram/lambdalifting.t +++ b/test/cram/lambdalifting.t @@ -17,30 +17,24 @@ written by @caller. After the pass: --- > proc @callee(x_in:bv32, y_in:bv32) -> (x_out:bv32) { } > - 9,10c6,12 - < block %entry [ $x:bv32 := bvadd($x:bv32, $y:bv32); goto (%ret); ]; + 9,10c6,9 + < block %entry [ $x:bv32 := bvadd($x, $y); goto (%ret); ]; < block %ret [ nop; return; ] --- - > block %inputs [ - > (var x:bv32 := x_in:bv32, var y:bv32 := y_in:bv32); - > goto (%entry); - > ]; - > block %entry [ var x:bv32 := bvadd(x:bv32, y:bv32); goto (%ret); ]; + > block %inputs [ (var x:bv32 := x_in, var y:bv32 := y_in); goto (%entry); ]; + > block %entry [ var x:bv32 := bvadd(x, y); goto (%ret); ]; > block %ret [ nop; goto (%returns); ]; - > block %returns [ var x_out:bv32 := x:bv32; return; ] - 12,14c14,15 + > block %returns [ var x_out:bv32 := x; return; ] + 12,14c11,12 < proc @caller() -> () { } < modifies $x:bv32, $y:bv32 < captures $x:bv32, $y:bv32 --- > proc @caller(x_in:bv32, y_in:bv32) -> (x_out:bv32, y_out:bv32) { } > - 16a18,21 - > block %inputs [ - > (var x:bv32 := x_in:bv32, var y:bv32 := y_in:bv32); - > goto (%entry); - > ]; - 18,21c23,26 + 16a15 + > block %inputs [ (var x:bv32 := x_in, var y:bv32 := y_in); goto (%entry); ]; + 18,21c17,20 < $y:bv32 := 0x0:bv32; < $x:bv32 := 0x1:bv32; < @@ -49,15 +43,12 @@ written by @caller. After the pass: > var y:bv32 := 0x0:bv32; > var x:bv32 := 0x1:bv32; > (var x:bv32=x_out) := - > call @callee(x_in=x:bv32, y_in=y:bv32); - 24c29,33 + > call @callee(x_in=x, y_in=y); + 24c23,24 < block %ret [ nop; return; ] --- > block %ret [ nop; goto (%returns); ]; - > block %returns [ - > (var x_out:bv32 := x:bv32, var y_out:bv32 := y:bv32); - > return; - > ] + > block %returns [ (var x_out:bv32 := x, var y_out:bv32 := y); return; ] [1] @@ -77,41 +68,34 @@ all global refs in requires (not just those under Old) become in-params. < proc @callee() -> () { } < modifies $x:bv32 < captures $x:bv32, $y:bv32 - < requires eq($x:bv32, 0x1:bv32) - < ensures eq($x:bv32, bvadd(old($x:bv32), $y:bv32)) + < requires eq($x, 0x1:bv32) + < ensures eq($x, bvadd(old($x), $y)) --- > proc @callee(x_in:bv32, y_in:bv32) -> (x_out:bv32) { } - > requires eq(x_in:bv32, 0x1:bv32) - > ensures eq(x_out:bv32, bvadd(x_in:bv32, y_in:bv32)) - 10a7,10 - > block %inputs [ - > (var x:bv32 := x_in:bv32, var y:bv32 := y_in:bv32); - > goto (%entry); - > ]; - 12,13c12,13 - < assert eq($x:bv32, old($x:bv32)); - < $x:bv32 := bvadd($x:bv32, $y:bv32); - --- - > assert eq(x:bv32, x_in:bv32); - > var x:bv32 := bvadd(x:bv32, y:bv32); - 16c16,17 + > requires eq(x_in, 0x1:bv32) + > ensures eq(x_out, bvadd(x_in, y_in)) + 11,16c7,10 + < block %entry [ + < assert eq($x, old($x)); + < $x:bv32 := bvadd($x, $y); + < goto (%ret); + < ]; < block %ret [ nop; return; ] --- + > block %inputs [ (var x:bv32 := x_in, var y:bv32 := y_in); goto (%entry); ]; + > block %entry [ assert eq(x, x_in); var x:bv32 := bvadd(x, y); goto (%ret); ]; > block %ret [ nop; goto (%returns); ]; - > block %returns [ var x_out:bv32 := x:bv32; return; ] - 18,20c19,20 + > block %returns [ var x_out:bv32 := x; return; ] + 18,20c12,13 < proc @caller() -> () { } < modifies $x:bv32, $y:bv32 < captures $x:bv32, $y:bv32 --- > proc @caller(x_in:bv32, y_in:bv32) -> (x_out:bv32, y_out:bv32) { } > - 22a23,26 - > block %inputs [ - > (var x:bv32 := x_in:bv32, var y:bv32 := y_in:bv32); - > goto (%entry); - > ]; - 24,27c28,31 + 22a16 + > block %inputs [ (var x:bv32 := x_in, var y:bv32 := y_in); goto (%entry); ]; + 24,27c18,21 < $y:bv32 := 0x0:bv32; < $x:bv32 := 0x1:bv32; < @@ -120,15 +104,12 @@ all global refs in requires (not just those under Old) become in-params. > var y:bv32 := 0x0:bv32; > var x:bv32 := 0x1:bv32; > (var x:bv32=x_out) := - > call @callee(x_in=x:bv32, y_in=y:bv32); - 30c34,38 + > call @callee(x_in=x, y_in=y); + 30c24,25 < block %ret [ nop; return; ] --- > block %ret [ nop; goto (%returns); ]; - > block %returns [ - > (var x_out:bv32 := x:bv32, var y_out:bv32 := y:bv32); - > return; - > ] + > block %returns [ (var x_out:bv32 := x, var y_out:bv32 := y); return; ] [1] diff --git a/test/cram/malloc_free.sexp b/test/cram/malloc_free.sexp new file mode 100644 index 00000000..e777b29b --- /dev/null +++ b/test/cram/malloc_free.sexp @@ -0,0 +1,9 @@ +(load-il "../../examples/memory/malloc_free.il") +(run-transforms "split-memory-encoding") +(run-transforms "memory-specification") +(dump-boogie "good.bpl") + +(load-il "../../examples/memory/malloc_free_oob.il") +(run-transforms "split-memory-encoding") +(run-transforms "memory-specification") +(dump-boogie "bad.bpl") diff --git a/test/cram/malloc_free.t b/test/cram/malloc_free.t new file mode 100644 index 00000000..6ad7fdb4 --- /dev/null +++ b/test/cram/malloc_free.t @@ -0,0 +1,430 @@ + $ bincaml script malloc_free.sexp + + $ cat ./good.bpl + var $R0: bv64; + var $R1: bv64; + var $R16: bv64; + var $R17: bv64; + var $R29: bv64; + var $R30: bv64; + var $R31: bv64; + var $mem: [bv64]bv8; + var $stack: [bv64]bv8; + var $mem_encoding: MemEncoding; + + function f$magic(a: [bv64]bv8, b: [bv64]bv8) returns ([bv64]bv8) { a } + function {:extern } {:bvbuiltin "bvadd"} bvadd_bv64(bv64, bv64) returns (bv64); + function {:extern } {:bvbuiltin "bvand"} bvand_bv64(bv64, bv64) returns (bv64); + function {:extern } {:bvbuiltin "bvule"} bvule_bv64_bv64_bool(bv64, bv64) returns (bool); + function {:extern } {:bvbuiltin "bvult"} bvult_bv64_bv64_bool(bv64, bv64) returns (bool); + function {:extern } load64_le(#memory: [bv64]bv8, #index: bv64) returns (bv64) { + (((((((#memory[bvadd_bv64(#index, 7bv64)] + ++ + #memory[bvadd_bv64(#index, 6bv64)]): bv16 + ++ + #memory[bvadd_bv64(#index, 5bv64)]): bv24 + ++ + #memory[bvadd_bv64(#index, 4bv64)]): bv32 + ++ + #memory[bvadd_bv64(#index, 3bv64)]): bv40 + ++ + #memory[bvadd_bv64(#index, 2bv64)]): bv48 + ++ + #memory[bvadd_bv64(#index, 1bv64)]): bv56 + ++ + #memory[bvadd_bv64(#index, 0bv64)]): bv64 + } + function {:inline } {:extern } me_addr_alloc(mem_encoding: MemEncoding, addr: bv64) returns (bv64) { + addr + } + function {:inline } {:extern } me_addr_is_heap(mem_encoding: MemEncoding, addr: bv64) returns (bool) { + mem_encoding->addr_is_heap[addr] + } + function {:inline } {:extern } me_addr_offset(mem_encoding: MemEncoding, addr: bv64) returns (bv64) { + bvand_bv64(addr, 4294967295bv64) + } + function {:inline } {:extern } me_alloc_base(mem_encoding: MemEncoding, alloc: bv64) returns (bv64) { + bvand_bv64(alloc, 18446744069414584320bv64) + } + function {:inline } {:extern } me_alloc_live(mem_encoding: MemEncoding, alloc: bv64) returns (bv2) { + mem_encoding->alloc_live[alloc] + } + function {:inline } {:extern } me_alloc_live_update(mem_encoding: MemEncoding, alloc: bv64, live: bv2) returns (MemEncoding) { + mem_encoding->(alloc_live := mem_encoding->alloc_live[alloc := live]) + } + function {:inline } {:extern } me_alloc_size(mem_encoding: MemEncoding, alloc: bv64) returns (bv64) { + mem_encoding->alloc_size[alloc] + } + function {:inline } {:extern } me_alloc_size_update(mem_encoding: MemEncoding, alloc: bv64, size: bv64) returns (MemEncoding) { + mem_encoding->(alloc_size := mem_encoding->alloc_size[alloc := size]) + } + function {:inline } {:extern } me_allocate(mem_encoding: MemEncoding, addr: bv64, size: bv64) returns (MemEncoding) { + me_alloc_size_update( + me_alloc_live_update(mem_encoding, me_addr_alloc(mem_encoding, addr), 1bv2), + me_addr_alloc(mem_encoding, addr), + size + ) + } + function {:inline } {:extern } me_can_allocate(mem_encoding: MemEncoding, addr: bv64, size: bv64) returns (bool) { + ((((me_addr_is_heap(mem_encoding, addr)&&(me_alloc_base(mem_encoding, addr) == addr))&&(me_alloc_live( + mem_encoding, + me_addr_alloc(mem_encoding, addr) + ) == 0bv2))&&bvule_bv64_bv64_bool(size, 4294967295bv64))&&bvult_bv64_bv64_bool( + 0bv64, + size + )) + } + function {:inline } {:extern } me_init_encoding(mem_encoding: MemEncoding) returns (bool) { + (((forall + i: bv64 :: + {me_addr_is_heap(mem_encoding, i)} + (bvult_bv64_bv64_bool(100000000bv64, i) == me_addr_is_heap(mem_encoding, i)))&&(forall + i: bv64 :: + {me_alloc_live(mem_encoding, i)} + (me_addr_is_heap(mem_encoding, i) ==> (me_alloc_live(mem_encoding, i) == 0bv2))))&&(forall + i: bv64 :: + {me_alloc_live(mem_encoding, i)} + ((!(me_addr_is_heap(mem_encoding, i))) ==> (me_alloc_live(mem_encoding, i) == 2bv2)))) + } + function {:inline } {:extern } me_valid_access(mem_encoding: MemEncoding, addr: bv64, size: bv64) returns (bool) { + (me_addr_is_heap(mem_encoding, addr) ==> ((me_alloc_live( + mem_encoding, + me_alloc_base(mem_encoding, me_addr_alloc(mem_encoding, addr)) + ) == 1bv2)&&bvule_bv64_bv64_bool( + me_addr_offset(mem_encoding, bvadd_bv64(addr, size)), + me_alloc_size( + mem_encoding, + me_alloc_base(mem_encoding, me_addr_alloc(mem_encoding, addr)) + ) + ))) + } + datatype MemEncoding {MemEncoding(alloc_live: [bv64]bv2, alloc_size: [bv64]bv64, addr_is_heap: [bv64]bool)} + function {:extern } {:define } store64_le(#memory: [bv64]bv8, #index: bv64, #value: bv64) returns ([bv64]bv8) { + #memory[#index := #value[8:0]][bvadd_bv64(#index, 1bv64) := #value[16:8]][bvadd_bv64( + #index, + 2bv64 + ) := #value[24:16]][bvadd_bv64(#index, 3bv64) := #value[32:24]][bvadd_bv64( + #index, + 4bv64 + ) := #value[40:32]][bvadd_bv64(#index, 5bv64) := #value[48:40]][bvadd_bv64( + #index, + 6bv64 + ) := #value[56:48]][bvadd_bv64(#index, 7bv64) := #value[64:56]] + } + function {:extern } {:define } store8_le(#memory: [bv64]bv8, #index: bv64, #value: bv8) returns ([bv64]bv8) { + #memory[#index := #value[8:0]] + } + + procedure p$free(); + modifies $mem_encoding, $mem, $stack, $R0, $R1, $R16, $R17, $R29, $R30, $R31; + ensures ($mem_encoding == me_alloc_live_update( + old($mem_encoding), + me_addr_alloc(old($mem_encoding), $R0), + 2bv2 + )); + requires me_addr_is_heap($mem_encoding, $R0); + requires (0bv64 == me_addr_offset($mem_encoding, $R0)); + requires (me_alloc_live($mem_encoding, me_addr_alloc($mem_encoding, $R0)) == 1bv2); + + procedure p$malloc(); + modifies $mem_encoding, $mem, $stack, $R0, $R1, $R16, $R17, $R29, $R30, $R31; + ensures me_can_allocate(old($mem_encoding), $R0, old($R0)); + ensures (me_addr_offset($mem_encoding, $R0) == 0bv64); + ensures (me_alloc_base($mem_encoding, me_addr_alloc($mem_encoding, $R0)) == $R0); + ensures ($mem_encoding == me_allocate(old($mem_encoding), $R0, old($R0))); + + procedure p$main(); + modifies $mem_encoding, $mem, $stack, $R0, $R1, $R16, $R17, $R29, $R30, $R31; + requires me_init_encoding($mem_encoding); + implementation p$main() { + var Exp18__5_25: bv64; + var Exp16__5_24: bv64; + var Exp14__5_2: bv64; + var Exp14__5_21: bv64; + var Cse0__5_23: bv64; + var Exp14__5_1: bv64; + var R30_begin_FUN_7a0_1952: bv64; + var R30_begin_FUN_770_1904: bv64; + var Exp14__5_22: bv64; + b#main_entry: + Cse0__5_23 := bvadd_bv64($R31, 18446744073709551584bv64); + $stack := store64_le($stack, Cse0__5_23, $R29); + $stack := store64_le($stack, bvadd_bv64(Cse0__5_23, 8bv64), $R30); + $R31 := Cse0__5_23; + $R29 := $R31; + $R0 := 17bv64; + $R30 := 2292bv64; + goto b#FUN_770_entry_9; + b#FUN_770_entry_9: + R30_begin_FUN_770_1904 := $R30; + $R16 := 131072bv64; + assert me_valid_access($mem_encoding, bvadd_bv64($R16, 16bv64), 8bv64); + Exp14__5_2 := load64_le($mem, bvadd_bv64($R16, 16bv64)); + $R17 := Exp14__5_2; + $R16 := bvadd_bv64($R16, 16bv64); + assert ($R30 == R30_begin_FUN_770_1904); + $R0 := 1bv64; + call p$malloc(); + goto b#FUN_770_basil_return_1_10; + b#FUN_770_basil_return_1_10: + goto b#_inlineret_4; + b#_inlineret_4: + goto b#main_5; + b#main_5: + $stack := store64_le($stack, bvadd_bv64($R31, 24bv64), $R0); + Exp14__5_21 := load64_le($stack, bvadd_bv64($R31, 24bv64)); + $R0 := Exp14__5_21; + $R0 := bvadd_bv64($R0, 0bv64); + $R1 := 121bv64; + assert me_valid_access($mem_encoding, $R0, 1bv64); + $mem := store8_le($mem, $R0, $R1[8:0]); + Exp14__5_22 := load64_le($stack, bvadd_bv64($R31, 24bv64)); + $R0 := Exp14__5_22; + $R30 := 2320bv64; + goto b#FUN_7a0_entry_7; + b#FUN_7a0_entry_7: + R30_begin_FUN_7a0_1952 := $R30; + $R16 := 131072bv64; + assert me_valid_access($mem_encoding, bvadd_bv64($R16, 40bv64), 8bv64); + Exp14__5_1 := load64_le($mem, bvadd_bv64($R16, 40bv64)); + $R17 := Exp14__5_1; + $R16 := bvadd_bv64($R16, 40bv64); + assert ($R30 == R30_begin_FUN_7a0_1952); + call p$free(); + goto b#FUN_7a0_basil_return_1_8; + b#FUN_7a0_basil_return_1_8: + goto b#_inlineret_3; + b#_inlineret_3: + goto b#main_3; + b#main_3: + $R0 := 0bv64; + Exp16__5_24 := load64_le($stack, $R31); + Exp18__5_25 := load64_le($stack, bvadd_bv64($R31, 8bv64)); + $R29 := Exp16__5_24; + $R30 := Exp18__5_25; + $R31 := bvadd_bv64($R31, 32bv64); + goto b#main_basil_return_1; + b#main_basil_return_1: + assert true; + return; + } + + $ boogie ./good.bpl + + Boogie program verifier finished with 1 verified, 0 errors + + $ cat ./bad.bpl + var $R0: bv64; + var $R1: bv64; + var $R16: bv64; + var $R17: bv64; + var $R29: bv64; + var $R30: bv64; + var $R31: bv64; + var $mem: [bv64]bv8; + var $stack: [bv64]bv8; + var $mem_encoding: MemEncoding; + + function f$magic(a: [bv64]bv8, b: [bv64]bv8) returns ([bv64]bv8) { a } + function {:extern } {:bvbuiltin "bvadd"} bvadd_bv64(bv64, bv64) returns (bv64); + function {:extern } {:bvbuiltin "bvand"} bvand_bv64(bv64, bv64) returns (bv64); + function {:extern } {:bvbuiltin "bvule"} bvule_bv64_bv64_bool(bv64, bv64) returns (bool); + function {:extern } {:bvbuiltin "bvult"} bvult_bv64_bv64_bool(bv64, bv64) returns (bool); + function {:extern } load64_le(#memory: [bv64]bv8, #index: bv64) returns (bv64) { + (((((((#memory[bvadd_bv64(#index, 7bv64)] + ++ + #memory[bvadd_bv64(#index, 6bv64)]): bv16 + ++ + #memory[bvadd_bv64(#index, 5bv64)]): bv24 + ++ + #memory[bvadd_bv64(#index, 4bv64)]): bv32 + ++ + #memory[bvadd_bv64(#index, 3bv64)]): bv40 + ++ + #memory[bvadd_bv64(#index, 2bv64)]): bv48 + ++ + #memory[bvadd_bv64(#index, 1bv64)]): bv56 + ++ + #memory[bvadd_bv64(#index, 0bv64)]): bv64 + } + function {:inline } {:extern } me_addr_alloc(mem_encoding: MemEncoding, addr: bv64) returns (bv64) { + addr + } + function {:inline } {:extern } me_addr_is_heap(mem_encoding: MemEncoding, addr: bv64) returns (bool) { + mem_encoding->addr_is_heap[addr] + } + function {:inline } {:extern } me_addr_offset(mem_encoding: MemEncoding, addr: bv64) returns (bv64) { + bvand_bv64(addr, 4294967295bv64) + } + function {:inline } {:extern } me_alloc_base(mem_encoding: MemEncoding, alloc: bv64) returns (bv64) { + bvand_bv64(alloc, 18446744069414584320bv64) + } + function {:inline } {:extern } me_alloc_live(mem_encoding: MemEncoding, alloc: bv64) returns (bv2) { + mem_encoding->alloc_live[alloc] + } + function {:inline } {:extern } me_alloc_live_update(mem_encoding: MemEncoding, alloc: bv64, live: bv2) returns (MemEncoding) { + mem_encoding->(alloc_live := mem_encoding->alloc_live[alloc := live]) + } + function {:inline } {:extern } me_alloc_size(mem_encoding: MemEncoding, alloc: bv64) returns (bv64) { + mem_encoding->alloc_size[alloc] + } + function {:inline } {:extern } me_alloc_size_update(mem_encoding: MemEncoding, alloc: bv64, size: bv64) returns (MemEncoding) { + mem_encoding->(alloc_size := mem_encoding->alloc_size[alloc := size]) + } + function {:inline } {:extern } me_allocate(mem_encoding: MemEncoding, addr: bv64, size: bv64) returns (MemEncoding) { + me_alloc_size_update( + me_alloc_live_update(mem_encoding, me_addr_alloc(mem_encoding, addr), 1bv2), + me_addr_alloc(mem_encoding, addr), + size + ) + } + function {:inline } {:extern } me_can_allocate(mem_encoding: MemEncoding, addr: bv64, size: bv64) returns (bool) { + ((((me_addr_is_heap(mem_encoding, addr)&&(me_alloc_base(mem_encoding, addr) == addr))&&(me_alloc_live( + mem_encoding, + me_addr_alloc(mem_encoding, addr) + ) == 0bv2))&&bvule_bv64_bv64_bool(size, 4294967295bv64))&&bvult_bv64_bv64_bool( + 0bv64, + size + )) + } + function {:inline } {:extern } me_init_encoding(mem_encoding: MemEncoding) returns (bool) { + (((forall + i: bv64 :: + {me_addr_is_heap(mem_encoding, i)} + (bvult_bv64_bv64_bool(100000000bv64, i) == me_addr_is_heap(mem_encoding, i)))&&(forall + i: bv64 :: + {me_alloc_live(mem_encoding, i)} + (me_addr_is_heap(mem_encoding, i) ==> (me_alloc_live(mem_encoding, i) == 0bv2))))&&(forall + i: bv64 :: + {me_alloc_live(mem_encoding, i)} + ((!(me_addr_is_heap(mem_encoding, i))) ==> (me_alloc_live(mem_encoding, i) == 2bv2)))) + } + function {:inline } {:extern } me_valid_access(mem_encoding: MemEncoding, addr: bv64, size: bv64) returns (bool) { + (me_addr_is_heap(mem_encoding, addr) ==> ((me_alloc_live( + mem_encoding, + me_alloc_base(mem_encoding, me_addr_alloc(mem_encoding, addr)) + ) == 1bv2)&&bvule_bv64_bv64_bool( + me_addr_offset(mem_encoding, bvadd_bv64(addr, size)), + me_alloc_size( + mem_encoding, + me_alloc_base(mem_encoding, me_addr_alloc(mem_encoding, addr)) + ) + ))) + } + datatype MemEncoding {MemEncoding(alloc_live: [bv64]bv2, alloc_size: [bv64]bv64, addr_is_heap: [bv64]bool)} + function {:extern } {:define } store64_le(#memory: [bv64]bv8, #index: bv64, #value: bv64) returns ([bv64]bv8) { + #memory[#index := #value[8:0]][bvadd_bv64(#index, 1bv64) := #value[16:8]][bvadd_bv64( + #index, + 2bv64 + ) := #value[24:16]][bvadd_bv64(#index, 3bv64) := #value[32:24]][bvadd_bv64( + #index, + 4bv64 + ) := #value[40:32]][bvadd_bv64(#index, 5bv64) := #value[48:40]][bvadd_bv64( + #index, + 6bv64 + ) := #value[56:48]][bvadd_bv64(#index, 7bv64) := #value[64:56]] + } + function {:extern } {:define } store8_le(#memory: [bv64]bv8, #index: bv64, #value: bv8) returns ([bv64]bv8) { + #memory[#index := #value[8:0]] + } + + procedure p$free(); + modifies $mem_encoding, $mem, $stack, $R0, $R1, $R16, $R17, $R29, $R30, $R31; + ensures ($mem_encoding == me_alloc_live_update( + old($mem_encoding), + me_addr_alloc(old($mem_encoding), $R0), + 2bv2 + )); + requires me_addr_is_heap($mem_encoding, $R0); + requires (0bv64 == me_addr_offset($mem_encoding, $R0)); + requires (me_alloc_live($mem_encoding, me_addr_alloc($mem_encoding, $R0)) == 1bv2); + + procedure p$malloc(); + modifies $mem_encoding, $mem, $stack, $R0, $R1, $R16, $R17, $R29, $R30, $R31; + ensures me_can_allocate(old($mem_encoding), $R0, old($R0)); + ensures (me_addr_offset($mem_encoding, $R0) == 0bv64); + ensures (me_alloc_base($mem_encoding, me_addr_alloc($mem_encoding, $R0)) == $R0); + ensures ($mem_encoding == me_allocate(old($mem_encoding), $R0, old($R0))); + + procedure p$main(); + modifies $mem_encoding, $mem, $stack, $R0, $R1, $R16, $R17, $R29, $R30, $R31; + requires me_init_encoding($mem_encoding); + implementation p$main() { + var Exp18__5_25: bv64; + var Exp16__5_24: bv64; + var Exp14__5_2: bv64; + var Exp14__5_21: bv64; + var Cse0__5_23: bv64; + var Exp14__5_1: bv64; + var R30_begin_FUN_7a0_1952: bv64; + var R30_begin_FUN_770_1904: bv64; + var Exp14__5_22: bv64; + b#main_entry: + Cse0__5_23 := bvadd_bv64($R31, 18446744073709551584bv64); + $stack := store64_le($stack, Cse0__5_23, $R29); + $stack := store64_le($stack, bvadd_bv64(Cse0__5_23, 8bv64), $R30); + $R31 := Cse0__5_23; + $R29 := $R31; + $R0 := 17bv64; + $R30 := 2292bv64; + goto b#FUN_770_entry_9; + b#FUN_770_entry_9: + R30_begin_FUN_770_1904 := $R30; + $R16 := 131072bv64; + assert me_valid_access($mem_encoding, bvadd_bv64($R16, 16bv64), 8bv64); + Exp14__5_2 := load64_le($mem, bvadd_bv64($R16, 16bv64)); + $R17 := Exp14__5_2; + $R16 := bvadd_bv64($R16, 16bv64); + assert ($R30 == R30_begin_FUN_770_1904); + $R0 := 1bv64; + call p$malloc(); + goto b#FUN_770_basil_return_1_10; + b#FUN_770_basil_return_1_10: + goto b#_inlineret_4; + b#_inlineret_4: + goto b#main_5; + b#main_5: + $stack := store64_le($stack, bvadd_bv64($R31, 24bv64), $R0); + Exp14__5_21 := load64_le($stack, bvadd_bv64($R31, 24bv64)); + $R0 := Exp14__5_21; + $R0 := bvadd_bv64($R0, 7bv64); + $R1 := 121bv64; + assert me_valid_access($mem_encoding, $R0, 1bv64); + $mem := store8_le($mem, $R0, $R1[8:0]); + Exp14__5_22 := load64_le($stack, bvadd_bv64($R31, 24bv64)); + $R0 := Exp14__5_22; + $R30 := 2320bv64; + goto b#FUN_7a0_entry_7; + b#FUN_7a0_entry_7: + R30_begin_FUN_7a0_1952 := $R30; + $R16 := 131072bv64; + assert me_valid_access($mem_encoding, bvadd_bv64($R16, 40bv64), 8bv64); + Exp14__5_1 := load64_le($mem, bvadd_bv64($R16, 40bv64)); + $R17 := Exp14__5_1; + $R16 := bvadd_bv64($R16, 40bv64); + assert ($R30 == R30_begin_FUN_7a0_1952); + call p$free(); + goto b#FUN_7a0_basil_return_1_8; + b#FUN_7a0_basil_return_1_8: + goto b#_inlineret_3; + b#_inlineret_3: + goto b#main_3; + b#main_3: + $R0 := 0bv64; + Exp16__5_24 := load64_le($stack, $R31); + Exp18__5_25 := load64_le($stack, bvadd_bv64($R31, 8bv64)); + $R29 := Exp16__5_24; + $R30 := Exp18__5_25; + $R31 := bvadd_bv64($R31, 32bv64); + goto b#main_basil_return_1; + b#main_basil_return_1: + assert true; + return; + } + + $ boogie ./bad.bpl + ./bad.bpl(176,5): Error: this assertion could not be proved + Execution trace: + ./bad.bpl(146,3): b#main_entry + + Boogie program verifier finished with 0 verified, 1 error diff --git a/test/cram/memassign.il b/test/cram/memassign.il index 150ded0d..609374c7 100644 --- a/test/cram/memassign.il +++ b/test/cram/memassign.il @@ -11,9 +11,16 @@ type record = Record of {a : bv64; b: bv32; c:bv64}; type ilist = Cons of {head:bv64; tail:ilist} | Nil ; +let $a = UninterpSort { }; + + +let $b = Record {a=1:bv64; b=2:bv64; c=3:bv64}; + let $mul_2 (a:bv64), (b:bv64) : bv64 = bvadd(b, bvmul(a, 2:bv64)); let $three = let func (a:bv64) : bv64 = bvadd(a, 1:bv64) in func($mul_2(2:bv64, 1:bv64)); +let $test (a:bv64) : bv64 = if (eq(a, 1:bv64)) then (10:bv64) else (11:bv64) ; + prog entry @main_4196164; diff --git a/test/cram/ptrrec1.il b/test/cram/ptrrec1.il index 3d7e609d..ba90d9fd 100644 --- a/test/cram/ptrrec1.il +++ b/test/cram/ptrrec1.il @@ -1,4 +1,6 @@ -var $rec:{("0": (bv32, 0))}; + +var $rec: struct { field0 : (0, bv32), field1: (32, bv64)} ; + prog entry @main_4196164; proc @main_4196164(R0_in:bv64, R10_in:bv64, R11_in:bv64, R12_in:bv64, R13_in:bv64, R14_in:bv64, R15_in:bv64, R16_in:bv64, R17_in:bv64, R18_in:bv64, R1_in:bv64, @@ -12,12 +14,12 @@ proc @main_4196164(R0_in:bv64, R10_in:bv64, R11_in:bv64, R12_in:bv64, R13_in:bv6 [ block %main_entry [ var as:ptr(bv64, bv64) := ptradd(R31_in:bv64, R0_in:bv64); - var af:bv32 := faccess("0", $rec:{("0": (bv32, 0))}); - $rec:{("0": (bv32, 0))} := fset("0", $rec:{("0": (bv32, 0))}, af:bv32); + var af:bv32 := bvadd(1:bv32, $rec.field0); + $rec:{("0": (bv32, 0))} := $rec.field0 <- af:bv32; goto (%main_return); ]; block %main_return [ (var R0_out:bv64 := 0x0:bv64, var R1_out:bv64 := 0x2a:bv64); return; ] -]; \ No newline at end of file +]; diff --git a/test/cram/roundtrip.t b/test/cram/roundtrip.t index a10c2246..704d5a7e 100644 --- a/test/cram/roundtrip.t +++ b/test/cram/roundtrip.t @@ -1,5 +1,10 @@ $ bincaml script roundtrip.sexp + bincaml: Error in (load-il beforemem.il): Parse error: beforemem.il:3 + 3 | let $b : record = Record of {a: bv64; b: bv32; c: bv64} = (Record)(0x1:bv64, + ^^ + at Dune__exe__Script.of_cmd.(fun) bin/script.ml:85 + [123] The serialise -> parse serialise loop should be idempotent @@ -38,42 +43,20 @@ The serialise -> parse serialise loop should be idempotent Memassign repr $ diff beforemem.il aftermem.il + diff: aftermem.il: No such file or directory + [2] $ cat aftermem.il - var observable $Global_4325420_4325424:bv32 classification true; - let $mul_2 (a:bv64), (b:bv64) : bv64 = (bvadd(b:bv64, bvmul(a:bv64, 0x2:bv64))); - let $three : bv64 = let func (a:bv64) : bv64 = (bvadd(a:bv64, 0x1:bv64)) in ((func:(bv64->bv64))(($mul_2:((bv64)->(bv64->bv64)))(0x2:bv64, - 0x1:bv64))); - type UninterpSort; - type ilist = Cons of {head: bv64; tail: ilist} | Nil; - type opaque = A | B | C; - type record = Record of {a: bv64; b: bv32; c: bv64}; - type variants = A of {a: bv64} | B of {b: bv32} | C of {c: bv8}; - prog entry @main_4196164; - proc @main_4196164(R0_in:bv64, R10_in:bv64, R11_in:bv64, R12_in:bv64, R13_in:bv64, - R14_in:bv64, R15_in:bv64, R16_in:bv64, R17_in:bv64, R18_in:bv64, R1_in:bv64, - R29_in:bv64, R2_in:bv64, R30_in:bv64, R31_in:bv64, R3_in:bv64, R4_in:bv64, - R5_in:bv64, R6_in:bv64, R7_in:bv64, R8_in:bv64, R9_in:bv64, _PC_in:bv64) - -> (R0_out:bv64, R1_out:bv64) { .address = 4196164; .name = "main"; - .returnBlock = "main_return" } - modifies $Global_4325420_4325424:bv32 - captures $Global_4325420_4325424:bv32 - - [ - block %main_entry [ - $Global_4325420_4325424:bv32 := store 0x2a:bv32; - goto (%main_return); - ]; - block %main_return [ - (var R0_out:bv64 := 0x0:bv64, var R1_out:bv64 := 0x2a:bv64); - return; - ] - ]; + cat: aftermem.il: No such file or directory + [1] Record and Pointer $ diff ptrrec1.il ptrrec2.il + diff: ptrrec2.il: No such file or directory + [2] - $ diff ptrrec2.il ptrrec3.il + $ diff ptrrec2.il ptrrec3.il 2>/dev/null + [2] diff --git a/test/cram/typefail.t b/test/cram/typefail.t index 48860951..873b3848 100644 --- a/test/cram/typefail.t +++ b/test/cram/typefail.t @@ -60,7 +60,7 @@ bv32 is not the correct type of bv64 for bvsmod at statement 50 in %main_entry bool is not of bitvector type in bvashr at statement 51 in %main_entry bv32 is not the correct type of bv64 for bvashr at statement 52 in %main_entry - Address loading data (#4:bv32) does not match address size (64) at statement 54 in %main_entry + Address loading data (#4) does not match address size (64) at statement 54 in %main_entry Body of booltobv1(0x7a0:bv64) is not a Boolean at statement 0 in %main_9 booltobv1 body is not a boolean at statement 0 in %main_9 [125] diff --git a/test/lang/test_stmt.ml b/test/lang/test_stmt.ml index 79a94e2c..06680c2d 100644 --- a/test/lang/test_stmt.ml +++ b/test/lang/test_stmt.ml @@ -20,7 +20,7 @@ let%expect_test "frees" = print_endline @@ Iter.to_string ~sep:"," Var.to_string (iter_lvar s); [%expect {| - (v1:bool := v2:bool, v3:bool := v4:bool) + (v1:bool := v2, v3:bool := v4) Rvars: v2:bool,v4:bool Lvars: v1:bool,v3:bool |}] @@ -48,22 +48,21 @@ let%expect_test "fold_block" = () block; print_endline (Block.to_string block); (); - [%expect - {| - $stack:(bv64->bv8) := store le $stack:(bv64->bv8) bvadd(R31_in:bv64, - 0xfffffffffffffffc:bv64) extract(32,0, R0_in:bv64) 32 - var load45_1:bv32 := load le $stack:(bv64->bv8) bvadd(R31_in:bv64, + [%expect {| + $stack:(bv64->bv8) := store le $stack:(bv64->bv8) bvadd(R31_in, + 0xfffffffffffffffc:bv64) extract(32,0, R0_in) 32 + var load45_1:bv32 := load le $stack:(bv64->bv8) bvadd(R31_in, 0xfffffffffffffffc:bv64) 32 - var R1_4:bv64 := zero_extend(32, load45_1:bv32) - $mem:(bv64->bv8) := store le $mem:(bv64->bv8) 0x420034:bv64 extract(32,0, R1_4:bv64) 32 + var R1_4:bv64 := zero_extend(32, load45_1) + $mem:(bv64->bv8) := store le $mem:(bv64->bv8) 0x420034:bv64 extract(32,0, R1_4) 32 var load46_1:bv32 := load le $mem:(bv64->bv8) 0x42002c:bv64 32 - var R0_10:bv64 := zero_extend(32, load46_1:bv32) + var R0_10:bv64 := zero_extend(32, load46_1) [ - $stack:(bv64->bv8) := store le $stack:(bv64->bv8) bvadd(R31_in:bv64, 0xfffffffffffffffc:bv64) extract(32,0, R0_in:bv64) 32; - load45_1:bv32 := load le $stack:(bv64->bv8) bvadd(R31_in:bv64, 0xfffffffffffffffc:bv64) 32; - R1_4:bv64 := zero_extend(32, load45_1:bv32); - $mem:(bv64->bv8) := store le $mem:(bv64->bv8) 0x420034:bv64 extract(32,0, R1_4:bv64) 32; + $stack:(bv64->bv8) := store le $stack:(bv64->bv8) bvadd(R31_in, 0xfffffffffffffffc:bv64) extract(32,0, R0_in) 32; + load45_1:bv32 := load le $stack:(bv64->bv8) bvadd(R31_in, 0xfffffffffffffffc:bv64) 32; + R1_4:bv64 := zero_extend(32, load45_1); + $mem:(bv64->bv8) := store le $mem:(bv64->bv8) 0x420034:bv64 extract(32,0, R1_4) 32; load46_1:bv32 := load le $mem:(bv64->bv8) 0x42002c:bv64 32; - R0_10:bv64 := zero_extend(32, load46_1:bv32); + R0_10:bv64 := zero_extend(32, load46_1); ] |}] diff --git a/tree-sitter/grammar.js b/tree-sitter/grammar.js index d2513ff6..947cec69 100644 --- a/tree-sitter/grammar.js +++ b/tree-sitter/grammar.js @@ -513,7 +513,11 @@ module.exports = grammar({ // Expr_Lambda. Expr ::= "fun" AttribSet LambdaDef ; seq("fun", optional($.AttribSet), $.LambdaDef), // Expr_Let. Expr ::= "let" LocalIdent [LocalVarParen] ":" Type "=" Expr "in" Expr ; - seq("let", $.token_LocalIdent, optional($.list_LocalVarParen), ":", $.Type, "=", $.Expr, "in", $.Expr) + seq("let", $.token_LocalIdent, optional($.list_LocalVarParen), ":", $.Type, "=", $.Expr, "in", $.Expr), + // Expr_Field. Expr ::= Expr2 BIdent ; + seq($.Expr2, $.token_BIdent), + // SortValRec. Expr ::= LocalIdent BeginRec [FieldAssign] EndRec ; + seq($.token_LocalIdent, $.token_BeginRec, optional($.list_FieldAssign), $.token_EndRec) ), Expr1: $ => choice( @@ -550,16 +554,16 @@ module.exports = grammar({ seq("extract", $.token_OpenParen, $.IntVal, ",", $.IntVal, ",", $.Expr, $.token_CloseParen), // Expr_Concat. Expr2 ::= "bvconcat" OpenParen [Expr] CloseParen ; seq("bvconcat", $.token_OpenParen, optional($.list_Expr), $.token_CloseParen), - // Expr_FSet. Expr2 ::= "fset" OpenParen Str "," Expr "," Expr CloseParen ; - seq("fset", $.token_OpenParen, $.token_Str, ",", $.Expr, ",", $.Expr, $.token_CloseParen), - // Expr_FAccess. Expr2 ::= "faccess" OpenParen Str "," Expr CloseParen ; - seq("faccess", $.token_OpenParen, $.token_Str, ",", $.Expr, $.token_CloseParen), + // Expr_Ite. Expr2 ::= "if" Expr "then" Expr "else" Expr ; + seq("if", $.Expr, "then", $.Expr, "else", $.Expr), // Expr_Match. Expr2 ::= "match" Expr "with" OpenParen [Case] CloseParen ; seq("match", $.Expr, "with", $.token_OpenParen, optional($.list_Case), $.token_CloseParen), // Expr_Cases. Expr2 ::= "cases" OpenParen [Case] CloseParen ; seq("cases", $.token_OpenParen, optional($.list_Case), $.token_CloseParen), // Expr_Paren. Expr2 ::= OpenParen Expr CloseParen ; - seq($.token_OpenParen, $.Expr, $.token_CloseParen) + seq($.token_OpenParen, $.Expr, $.token_CloseParen), + // Expr_FieldSet. Expr2 ::= Expr2 "with" LocalIdent "=" Expr ; + seq($.Expr2, "with", $.token_LocalIdent, "=", $.Expr) ), LambdaDef: $ => // LambdaDef1. LambdaDef ::= [LocalVarParen] LambdaSep Expr ; @@ -610,6 +614,18 @@ module.exports = grammar({ // (:). [Case] ::= Case "|" [Case] ; seq($.Case, "|", optional($.list_Case)) ), + FieldAssign: $ => + // FieldAssign1. FieldAssign ::= LocalIdent "=" Expr ; + seq($.token_LocalIdent, "=", $.Expr), + list_FieldAssign: $ => + choice( + // []. [FieldAssign] ::= ; + choice(), + // (:[]). [FieldAssign] ::= FieldAssign ; + $.FieldAssign, + // (:). [FieldAssign] ::= FieldAssign ";" [FieldAssign] ; + seq($.FieldAssign, ";", optional($.list_FieldAssign)) + ), EqOp: $ => choice( // EqOp_eq. EqOp ::= "eq" ;