diff --git a/dune-project b/dune-project index 64916cdc..60ab08b3 100644 --- a/dune-project +++ b/dune-project @@ -8,6 +8,9 @@ (generate_opam_files true) +(formatting + (enabled_for dune)) + (source (github username/reponame)) diff --git a/examples/cat.il b/examples/cat.il index d6b0c07c..27fd0e5b 100644 --- a/examples/cat.il +++ b/examples/cat.il @@ -48,8 +48,8 @@ prog entry @main_4197696; proc @main_4197696 () -> () { .name = "main"; .address = 0x400d40; .returnBlock = "main_basil_return_1" } - require eq($_PC:bv64, 0x400d40:bv64); - ensures eq($_PC:bv64, old($R30:bv64)); + require eq($_PC:bv64, 0x400d40:bv64) + ensures eq($_PC:bv64, old($R30:bv64)) [ block %main_entry {.address = 0x400d40; .originalLabel = "KXhc9Fe2Qva4qWVLC1eV+w=="} [ assert eq($_PC:bv64, 0x400d40:bv64); @@ -86,8 +86,8 @@ proc @exit () -> () proc @exitcode_4198816 () -> () { .name = "exitcode"; .address = 0x4011a0; .returnBlock = "exitcode_basil_return_1" } - require eq($_PC:bv64, 0x4011a0:bv64); - ensures eq($_PC:bv64, old($R30:bv64)); + require eq($_PC:bv64, 0x4011a0:bv64) + ensures eq($_PC:bv64, old($R30:bv64)) [ block %exitcode_entry {.address = 0x4011a0; .originalLabel = "Hr3XvFHLQ62ROxw2L+L+kg=="} [ assert eq($_PC:bv64, 0x4011a0:bv64); @@ -109,8 +109,8 @@ proc @exitcode_4198816 () -> () proc @exits_4198688 () -> () { .name = "exits"; .address = 0x401120; .returnBlock = "exits_basil_return_1" } - require eq($_PC:bv64, 0x401120:bv64); - ensures eq($_PC:bv64, old($R30:bv64)); + require eq($_PC:bv64, 0x401120:bv64) + ensures eq($_PC:bv64, old($R30:bv64)) [ block %exits_entry {.address = 0x401120; .originalLabel = "OamxgWkAT5S7lYhJLb34Bw=="} [ var R30_begin_exits_4198688: bv64 := $R30:bv64; @@ -449,8 +449,8 @@ proc @exits_4198688 () -> () proc @fmtlocaleinit_4209552 () -> () { .name = "fmtlocaleinit"; .address = 0x403b90; .returnBlock = "fmtlocaleinit_basil_return_1" } - require eq($_PC:bv64, 0x403b90:bv64); - ensures eq($_PC:bv64, old($R30:bv64)); + require eq($_PC:bv64, 0x403b90:bv64) + ensures eq($_PC:bv64, old($R30:bv64)) [ block %fmtlocaleinit_entry {.address = 0x403b90; .originalLabel = "LJeXYGqvSDa8MTgV+KKKNg=="} [ assert eq($_PC:bv64, 0x403b90:bv64); @@ -611,8 +611,8 @@ proc @fmtlocaleinit_4209552 () -> () proc @fmtfdinit_4209364 () -> () { .name = "fmtfdinit"; .address = 0x403ad4; .returnBlock = "fmtfdinit_basil_return_1" } - require eq($_PC:bv64, 0x403ad4:bv64); - ensures eq($_PC:bv64, old($R30:bv64)); + require eq($_PC:bv64, 0x403ad4:bv64) + ensures eq($_PC:bv64, old($R30:bv64)) [ block %fmtfdinit_entry {.address = 0x403ad4; .originalLabel = "Ase3rrH2SOSuhunVYXYBhg=="} [ assert eq($_PC:bv64, 0x403ad4:bv64); @@ -715,8 +715,8 @@ proc @write () -> () proc @__fmtFdFlush_4209456 () -> () { .name = "__fmtFdFlush"; .address = 0x403b30; .returnBlock = "__fmtFdFlush_basil_return_1" } - require eq($_PC:bv64, 0x403b30:bv64); - ensures eq($_PC:bv64, old($R30:bv64)); + require eq($_PC:bv64, 0x403b30:bv64) + ensures eq($_PC:bv64, old($R30:bv64)) [ block %__fmtFdFlush_entry {.address = 0x403b30; .originalLabel = "I+YOj/gGRqS87EwafUF4WA=="} [ assert eq($_PC:bv64, 0x403b30:bv64); @@ -914,8 +914,8 @@ proc @__fmtFdFlush_4209456 () -> () proc @__flagfmt_4208112 () -> () { .name = "__flagfmt"; .address = 0x4035f0; .returnBlock = "__flagfmt_basil_return_1" } - require eq($_PC:bv64, 0x4035f0:bv64); - ensures eq($_PC:bv64, old($R30:bv64)); + require eq($_PC:bv64, 0x4035f0:bv64) + ensures eq($_PC:bv64, old($R30:bv64)) [ block %__flagfmt_entry {.address = 0x4035f0; .originalLabel = "Md5qE+eiRf+m/NPBkVuT3g=="} [ assert eq($_PC:bv64, 0x4035f0:bv64); @@ -1454,8 +1454,8 @@ proc @__flagfmt_4208112 () -> () proc @__rfmtpad_4203024 () -> () { .name = "__rfmtpad"; .address = 0x402210; .returnBlock = "__rfmtpad_basil_return_1" } - require eq($_PC:bv64, 0x402210:bv64); - ensures eq($_PC:bv64, old($R30:bv64)); + require eq($_PC:bv64, 0x402210:bv64) + ensures eq($_PC:bv64, old($R30:bv64)) [ block %__rfmtpad_entry {.address = 0x402210; .originalLabel = "FnHqSK+lTxq6YDUq7NvnJg=="} [ assert eq($_PC:bv64, 0x402210:bv64); @@ -1940,8 +1940,8 @@ proc @__rfmtpad_4203024 () -> () proc @runelen_4210048 () -> () { .name = "runelen"; .address = 0x403d80; .returnBlock = "runelen_basil_return_1" } - require eq($_PC:bv64, 0x403d80:bv64); - ensures eq($_PC:bv64, old($R30:bv64)); + require eq($_PC:bv64, 0x403d80:bv64) + ensures eq($_PC:bv64, old($R30:bv64)) [ block %runelen_entry {.address = 0x403d80; .originalLabel = "o0lVyZ2GT4mJNVkb5e5Vuw=="} [ assert eq($_PC:bv64, 0x403d80:bv64); @@ -2022,8 +2022,8 @@ proc @runelen_4210048 () -> () proc @fullrune_4210160 () -> () { .name = "fullrune"; .address = 0x403df0; .returnBlock = "fullrune_basil_return_1" } - require eq($_PC:bv64, 0x403df0:bv64); - ensures eq($_PC:bv64, old($R30:bv64)); + require eq($_PC:bv64, 0x403df0:bv64) + ensures eq($_PC:bv64, old($R30:bv64)) [ block %fullrune_entry {.address = 0x403df0; .originalLabel = "ycUhyOy1TNW1hp1YrdP0uw=="} [ assert eq($_PC:bv64, 0x403df0:bv64); @@ -2178,8 +2178,8 @@ proc @fullrune_4210160 () -> () proc @__fmtpad_4202756 () -> () { .name = "__fmtpad"; .address = 0x402104; .returnBlock = "__fmtpad_basil_return_1" } - require eq($_PC:bv64, 0x402104:bv64); - ensures eq($_PC:bv64, old($R30:bv64)); + require eq($_PC:bv64, 0x402104:bv64) + ensures eq($_PC:bv64, old($R30:bv64)) [ block %__fmtpad_entry {.address = 0x402104; .originalLabel = "DS7w57znRnmBsFkYW6cA+Q=="} [ assert eq($_PC:bv64, 0x402104:bv64); @@ -2663,8 +2663,8 @@ proc @__fmtpad_4202756 () -> () proc @runetochar_4209936 () -> () { .name = "runetochar"; .address = 0x403d10; .returnBlock = "runetochar_basil_return_1" } - require eq($_PC:bv64, 0x403d10:bv64); - ensures eq($_PC:bv64, old($R30:bv64)); + require eq($_PC:bv64, 0x403d10:bv64) + ensures eq($_PC:bv64, old($R30:bv64)) [ block %runetochar_entry {.address = 0x403d10; .originalLabel = "Rkek/d08TK2mkJ7PEcm6mg=="} [ assert eq($_PC:bv64, 0x403d10:bv64); @@ -2816,8 +2816,8 @@ proc @runetochar_4209936 () -> () proc @__fmtflush_4202032 () -> () { .name = "__fmtflush"; .address = 0x401e30; .returnBlock = "__fmtflush_basil_return_1" } - require eq($_PC:bv64, 0x401e30:bv64); - ensures eq($_PC:bv64, old($R30:bv64)); + require eq($_PC:bv64, 0x401e30:bv64) + ensures eq($_PC:bv64, old($R30:bv64)) [ block %__fmtflush_entry {.address = 0x401e30; .originalLabel = "Osy3QCRQRpSd5aY0vW+qkQ=="} [ assert eq($_PC:bv64, 0x401e30:bv64); @@ -3092,8 +3092,8 @@ proc @__fmtflush_4202032 () -> () proc @chartorune_4209760 () -> () { .name = "chartorune"; .address = 0x403c60; .returnBlock = "chartorune_basil_return_1" } - require eq($_PC:bv64, 0x403c60:bv64); - ensures eq($_PC:bv64, old($R30:bv64)); + require eq($_PC:bv64, 0x403c60:bv64) + ensures eq($_PC:bv64, old($R30:bv64)) [ block %chartorune_entry {.address = 0x403c60; .originalLabel = "+s65+r9uRzKHgPS/OxqX3g=="} [ assert eq($_PC:bv64, 0x403c60:bv64); @@ -3398,8 +3398,8 @@ proc @chartorune_4209760 () -> () proc @__fmtcpy_4203296 () -> () { .name = "__fmtcpy"; .address = 0x402320; .returnBlock = "__fmtcpy_basil_return_1" } - require eq($_PC:bv64, 0x402320:bv64); - ensures eq($_PC:bv64, old($R30:bv64)); + require eq($_PC:bv64, 0x402320:bv64) + ensures eq($_PC:bv64, old($R30:bv64)) [ block %__fmtcpy_entry {.address = 0x402320; .originalLabel = "onW0wUQSS+CWRE3FG7sZVA=="} [ assert eq($_PC:bv64, 0x402320:bv64); @@ -4774,8 +4774,8 @@ proc @__fmtcpy_4203296 () -> () proc @__badfmt_4208400 () -> () { .name = "__badfmt"; .address = 0x403710; .returnBlock = "__badfmt_basil_return_1" } - require eq($_PC:bv64, 0x403710:bv64); - ensures eq($_PC:bv64, old($R30:bv64)); + require eq($_PC:bv64, 0x403710:bv64) + ensures eq($_PC:bv64, old($R30:bv64)) [ block %__badfmt_entry {.address = 0x403710; .originalLabel = "VsS7dlFoQ3et0t9jIUUtyw=="} [ assert eq($_PC:bv64, 0x403710:bv64); @@ -4852,8 +4852,8 @@ proc @__badfmt_4208400 () -> () proc @getcallerpc_4201920 () -> () { .name = "getcallerpc"; .address = 0x401dc0; .returnBlock = "getcallerpc_basil_return_1" } - require eq($_PC:bv64, 0x401dc0:bv64); - ensures eq($_PC:bv64, old($R30:bv64)); + require eq($_PC:bv64, 0x401dc0:bv64) + ensures eq($_PC:bv64, old($R30:bv64)) [ block %getcallerpc_entry {.address = 0x401dc0; .originalLabel = "/lgI4FfjS+yfGYqEtnuiGw=="} [ assert eq($_PC:bv64, 0x401dc0:bv64); @@ -4879,8 +4879,8 @@ proc @getcallerpc_4201920 () -> () proc @unlock_4199332 () -> () { .name = "unlock"; .address = 0x4013a4; .returnBlock = "unlock_basil_return_1" } - require eq($_PC:bv64, 0x4013a4:bv64); - ensures eq($_PC:bv64, old($R30:bv64)); + require eq($_PC:bv64, 0x4013a4:bv64) + ensures eq($_PC:bv64, old($R30:bv64)) [ block %unlock_entry {.address = 0x4013a4; .originalLabel = "V0jFzXuITMiNHr/kb8xG4g=="} [ assert eq($_PC:bv64, 0x4013a4:bv64); @@ -5022,8 +5022,8 @@ proc @unlock_4199332 () -> () proc @__fmtunlock_4209744 () -> () { .name = "__fmtunlock"; .address = 0x403c50; .returnBlock = "__fmtunlock_basil_return_1" } - require eq($_PC:bv64, 0x403c50:bv64); - ensures eq($_PC:bv64, old($R30:bv64)); + require eq($_PC:bv64, 0x403c50:bv64) + ensures eq($_PC:bv64, old($R30:bv64)) [ block %__fmtunlock_entry {.address = 0x403c50; .originalLabel = "LHWtkP5rQmqxTbinnC1hLw=="} [ var R30_begin___fmtunlock_4209744: bv64 := $R30:bv64; @@ -5051,8 +5051,8 @@ proc @__fmtunlock_4209744 () -> () proc @lock_4199120 () -> () { .name = "lock"; .address = 0x4012d0; .returnBlock = "lock_basil_return_1" } - require eq($_PC:bv64, 0x4012d0:bv64); - ensures eq($_PC:bv64, old($R30:bv64)); + require eq($_PC:bv64, 0x4012d0:bv64) + ensures eq($_PC:bv64, old($R30:bv64)) [ block %lock_entry {.address = 0x4012d0; .originalLabel = "EL5Ky+1GSIeJ6nw6JbZnPg=="} [ assert eq($_PC:bv64, 0x4012d0:bv64); @@ -5204,8 +5204,8 @@ proc @lock_4199120 () -> () proc @__fmtlock_4209728 () -> () { .name = "__fmtlock"; .address = 0x403c40; .returnBlock = "__fmtlock_basil_return_1" } - require eq($_PC:bv64, 0x403c40:bv64); - ensures eq($_PC:bv64, old($R30:bv64)); + require eq($_PC:bv64, 0x403c40:bv64) + ensures eq($_PC:bv64, old($R30:bv64)) [ block %__fmtlock_entry {.address = 0x403c40; .originalLabel = "n9+4iNtqRLu7+3FBjvBlSg=="} [ var R30_begin___fmtlock_4209728: bv64 := $R30:bv64; @@ -5233,8 +5233,8 @@ proc @__fmtlock_4209728 () -> () proc @__fmtinstall_4208464 () -> () { .name = "__fmtinstall"; .address = 0x403750; .returnBlock = "__fmtinstall_basil_return_1" } - require eq($_PC:bv64, 0x403750:bv64); - ensures eq($_PC:bv64, old($R30:bv64)); + require eq($_PC:bv64, 0x403750:bv64) + ensures eq($_PC:bv64, old($R30:bv64)) [ block %__fmtinstall_entry {.address = 0x403750; .originalLabel = "4vz6BXioRXa/LaTzSs8GSg=="} [ assert eq($_PC:bv64, 0x403750:bv64); @@ -5516,8 +5516,8 @@ proc @__fmtinstall_4208464 () -> () proc @__fmtdispatch_4208688 () -> () { .name = "__fmtdispatch"; .address = 0x403830; .returnBlock = "__fmtdispatch_basil_return_1" } - require eq($_PC:bv64, 0x403830:bv64); - ensures eq($_PC:bv64, old($R30:bv64)); + require eq($_PC:bv64, 0x403830:bv64) + ensures eq($_PC:bv64, old($R30:bv64)) [ block %__fmtdispatch_entry {.address = 0x403830; .originalLabel = "J5JvET/ORDyFBY1+xoNLkA=="} [ assert eq($_PC:bv64, 0x403830:bv64); @@ -6659,8 +6659,8 @@ proc @__fmtdispatch_4208688 () -> () proc @dofmt_4202176 () -> () { .name = "dofmt"; .address = 0x401ec0; .returnBlock = "dofmt_basil_return_1" } - require eq($_PC:bv64, 0x401ec0:bv64); - ensures eq($_PC:bv64, old($R30:bv64)); + require eq($_PC:bv64, 0x401ec0:bv64) + ensures eq($_PC:bv64, old($R30:bv64)) [ block %dofmt_entry {.address = 0x401ec0; .originalLabel = "ptCQBLyvTM22JSPE/cK18w=="} [ assert eq($_PC:bv64, 0x401ec0:bv64); @@ -7699,8 +7699,8 @@ proc @dofmt_4202176 () -> () proc @vfprint_4201072 () -> () { .name = "vfprint"; .address = 0x401a70; .returnBlock = "vfprint_basil_return_1" } - require eq($_PC:bv64, 0x401a70:bv64); - ensures eq($_PC:bv64, old($R30:bv64)); + require eq($_PC:bv64, 0x401a70:bv64) + ensures eq($_PC:bv64, old($R30:bv64)) [ block %vfprint_entry {.address = 0x401a70; .originalLabel = "kh4iUxoKQMenD77ljouyEQ=="} [ assert eq($_PC:bv64, 0x401a70:bv64); @@ -7882,8 +7882,8 @@ proc @vfprint_4201072 () -> () proc @fprint_4200960 () -> () { .name = "fprint"; .address = 0x401a00; .returnBlock = "fprint_basil_return_1" } - require eq($_PC:bv64, 0x401a00:bv64); - ensures eq($_PC:bv64, old($R30:bv64)); + require eq($_PC:bv64, 0x401a00:bv64) + ensures eq($_PC:bv64, old($R30:bv64)) [ block %fprint_entry {.address = 0x401a00; .originalLabel = "fQteMOadSm+stHHR3jx4Qw=="} [ assert eq($_PC:bv64, 0x401a00:bv64); @@ -7986,8 +7986,8 @@ proc @fprint_4200960 () -> () proc @__fixargv0_4198400 () -> () { .name = "__fixargv0"; .address = 0x401000; .returnBlock = "__fixargv0_basil_return_1" } - require eq($_PC:bv64, 0x401000:bv64); - ensures eq($_PC:bv64, old($R30:bv64)); + require eq($_PC:bv64, 0x401000:bv64) + ensures eq($_PC:bv64, old($R30:bv64)) [ block %__fixargv0_entry {.address = 0x401000; .originalLabel = "78skE39ZS92hlwuQoG/N1g=="} [ assert eq($_PC:bv64, 0x401000:bv64); @@ -8007,8 +8007,8 @@ proc @__fixargv0_4198400 () -> () proc @vseprint_4201184 () -> () { .name = "vseprint"; .address = 0x401ae0; .returnBlock = "vseprint_basil_return_1" } - require eq($_PC:bv64, 0x401ae0:bv64); - ensures eq($_PC:bv64, old($R30:bv64)); + require eq($_PC:bv64, 0x401ae0:bv64) + ensures eq($_PC:bv64, old($R30:bv64)) [ block %vseprint_entry {.address = 0x401ae0; .originalLabel = "xuA0Edh9S8yFZV1Qu/Jgqw=="} [ assert eq($_PC:bv64, 0x401ae0:bv64); @@ -8169,8 +8169,8 @@ proc @vseprint_4201184 () -> () proc @sysfatal_4200560 () -> () { .name = "sysfatal"; .address = 0x401870; .returnBlock = "sysfatal_basil_return_1" } - require eq($_PC:bv64, 0x401870:bv64); - ensures eq($_PC:bv64, old($R30:bv64)); + require eq($_PC:bv64, 0x401870:bv64) + ensures eq($_PC:bv64, old($R30:bv64)) [ block %sysfatal_entry {.address = 0x401870; .originalLabel = "HN8ZNDP1RUKhvFhL/Qx3ng=="} [ var R30_begin_sysfatal_4200560: bv64 := $R30:bv64; @@ -8471,8 +8471,8 @@ proc @memccpy () -> () proc @strecpy_4201936 () -> () { .name = "strecpy"; .address = 0x401dd0; .returnBlock = "strecpy_basil_return_1" } - require eq($_PC:bv64, 0x401dd0:bv64); - ensures eq($_PC:bv64, old($R30:bv64)); + require eq($_PC:bv64, 0x401dd0:bv64) + ensures eq($_PC:bv64, old($R30:bv64)) [ block %strecpy_entry {.address = 0x401dd0; .originalLabel = "gS9qAucpRMKJD8TibWbm5A=="} [ assert eq($_PC:bv64, 0x401dd0:bv64); @@ -8680,8 +8680,8 @@ proc @strerror () -> () proc @rerrstr_4201312 () -> () { .name = "rerrstr"; .address = 0x401b60; .returnBlock = "rerrstr_basil_return_1" } - require eq($_PC:bv64, 0x401b60:bv64); - ensures eq($_PC:bv64, old($R30:bv64)); + require eq($_PC:bv64, 0x401b60:bv64) + ensures eq($_PC:bv64, old($R30:bv64)) [ block %rerrstr_entry {.address = 0x401b60; .originalLabel = "ldWhLOMYSKyYFGShQwXqIg=="} [ var R30_begin_rerrstr_4201312: bv64 := $R30:bv64; @@ -9214,8 +9214,8 @@ proc @rerrstr_4201312 () -> () proc @errstr_4201540 () -> () { .name = "errstr"; .address = 0x401c44; .returnBlock = "errstr_basil_return_1" } - require eq($_PC:bv64, 0x401c44:bv64); - ensures eq($_PC:bv64, old($R30:bv64)); + require eq($_PC:bv64, 0x401c44:bv64) + ensures eq($_PC:bv64, old($R30:bv64)) [ block %errstr_entry {.address = 0x401c44; .originalLabel = "3ReV3l3lTEWXlI8dRV4Pcw=="} [ assert eq($_PC:bv64, 0x401c44:bv64); @@ -9454,8 +9454,8 @@ proc @errstr_4201540 () -> () proc @werrstr_4201780 () -> () { .name = "werrstr"; .address = 0x401d34; .returnBlock = "werrstr_basil_return_1" } - require eq($_PC:bv64, 0x401d34:bv64); - ensures eq($_PC:bv64, old($R30:bv64)); + require eq($_PC:bv64, 0x401d34:bv64) + ensures eq($_PC:bv64, old($R30:bv64)) [ block %werrstr_entry {.address = 0x401d34; .originalLabel = "EsiP/3+hSbS6DhsMqrwxFA=="} [ assert eq($_PC:bv64, 0x401d34:bv64); @@ -9607,8 +9607,8 @@ proc @open64 () -> () proc @p9open_4198832 () -> () { .name = "p9open"; .address = 0x4011b0; .returnBlock = "p9open_basil_return_1" } - require eq($_PC:bv64, 0x4011b0:bv64); - ensures eq($_PC:bv64, old($R30:bv64)); + require eq($_PC:bv64, 0x4011b0:bv64) + ensures eq($_PC:bv64, old($R30:bv64)) [ block %p9open_entry {.address = 0x4011b0; .originalLabel = "DYW7Gbw6QwK5DzhE/cGL7w=="} [ assert eq($_PC:bv64, 0x4011b0:bv64); @@ -10273,8 +10273,8 @@ proc @p9open_4198832 () -> () proc @p9write_4200816 () -> () { .name = "p9write"; .address = 0x401970; .returnBlock = "p9write_basil_return_1" } - require eq($_PC:bv64, 0x401970:bv64); - ensures eq($_PC:bv64, old($R30:bv64)); + require eq($_PC:bv64, 0x401970:bv64) + ensures eq($_PC:bv64, old($R30:bv64)) [ block %p9write_entry {.address = 0x401970; .originalLabel = "qVvzznzaToayt5BQelE/sg=="} [ assert eq($_PC:bv64, 0x401970:bv64); @@ -10571,8 +10571,8 @@ proc @read () -> () proc @cat_4198032 () -> () { .name = "cat"; .address = 0x400e90; .returnBlock = "cat_basil_return_1" } - require eq($_PC:bv64, 0x400e90:bv64); - ensures eq($_PC:bv64, old($R30:bv64)); + require eq($_PC:bv64, 0x400e90:bv64) + ensures eq($_PC:bv64, old($R30:bv64)) [ block %cat_entry {.address = 0x400e90; .originalLabel = "OMO2ysIfSmeORBpBsr5OIQ=="} [ var R30_begin_cat_4198032: bv64 := $R30:bv64; @@ -10826,8 +10826,8 @@ proc @cat_4198032 () -> () proc @p9main_4198208 () -> () { .name = "p9main"; .address = 0x400f40; .returnBlock = "p9main_basil_return_1" } - require eq($_PC:bv64, 0x400f40:bv64); - ensures eq($_PC:bv64, old($R30:bv64)); + require eq($_PC:bv64, 0x400f40:bv64) + ensures eq($_PC:bv64, old($R30:bv64)) [ block %p9main_entry {.address = 0x400f40; .originalLabel = "FGQT8qmESb6FIwl/znG8jA=="} [ var R30_begin_p9main_4198208: bv64 := $R30:bv64; diff --git a/examples/conds.il b/examples/conds.il index 1125b6d6..0428a536 100644 --- a/examples/conds.il +++ b/examples/conds.il @@ -14,8 +14,8 @@ prog entry @main_4196260; proc @main_4196260 () -> () { .name = "main"; .address = 0x4007a4; .returnBlock = "main_basil_return_1" } - require eq($_PC:bv64, 0x4007a4:bv64); - ensures eq($_PC:bv64, old($R30:bv64)); + require eq($_PC:bv64, 0x4007a4:bv64) + ensures eq($_PC:bv64, old($R30:bv64)) [ block %main_entry {.address = 0x4007a4; .originalLabel = "rlVqjjqoR6uHwOYvPCS15g=="} [ assert eq($_PC:bv64, 0x4007a4:bv64); diff --git a/examples/x-output.il b/examples/x-output.il index acccac91..8d649379 100644 --- a/examples/x-output.il +++ b/examples/x-output.il @@ -7,7 +7,7 @@ proc @main_4196164 (R0_in:bv64, R1_in:bv64, R30_in:bv64, R31_in:bv64, _PC_in:bv64) -> (R0_out:bv64, R1_out:bv64, _PC_out:bv64) { .name = "main"; .address = 0x400744 } - require bvsge(R31_in:bv64, bvsub(R31_in:bv64, 0x10:bv64)); + require bvsge(R31_in:bv64, bvsub(R31_in:bv64, 0x10:bv64)) [ block %main_entry {.address = 0x400744; .originalLabel = "G8B0Q6XuSneDgqpNFr1sUQ=="} [ store le $stack bvadd(R31_in:bv64, 0xfffffffffffffffc:bv64) extract(32, 0, R0_in:bv64) 32 { .label = "4196168_0" }; diff --git a/lib/fe/AbsBasilIR.ml b/lib/fe/AbsBasilIR.ml index 6868acb7..ad9eb9bf 100644 --- a/lib/fe/AbsBasilIR.ml +++ b/lib/fe/AbsBasilIR.ml @@ -1,4 +1,4 @@ -(* File generated by the BNF Converter (bnfc 2.9.6.1). *) +(* File generated by the BNF Converter (bnfc 2.9.6.2). *) type bVTYPE = BVTYPE of ((int * int) * string) and iNTTYPE = INTTYPE of ((int * int) * string) @@ -24,10 +24,6 @@ and lambdaSep = LambdaSep1 | LambdaSep2 -and semicolons = - Semicolons_Empty - | Semicolons_Some of semicolons - and varModifiers = Shared | Observable @@ -53,18 +49,18 @@ and intType = and boolType = BoolType1 of bOOLTYPE -and mapType = - MapType1 of typeT * typeT - and bVType = BVType1 of bVTYPE +and mapType = + MapType1 of typeT * typeT + and typeT = TypeIntType of intType | TypeBoolType of boolType - | TypeMapType of mapType | TypeBVType of bVType - | Type1 of openParen * typeT * closeParen + | TypeParen of openParen * typeT * closeParen + | TypeMapType of mapType and intVal = IntVal_Hex of integerHex @@ -87,10 +83,9 @@ and stmt = | Stmt_ScalarStore of lVar * expr | Stmt_ScalarLoad of lVar * var | Stmt_MultiAssign of openParen * assignment list * closeParen - | Stmt_Load of lVar * endian * globalIdent * expr * intVal - | Stmt_Store of endian * globalIdent * expr * expr * intVal | Stmt_Load_Var of lVar * endian * var * expr * intVal | Stmt_Store_Var of lVar * endian * var * expr * expr * intVal + | Stmt_Store of endian * globalIdent * expr * expr * intVal | Stmt_DirectCall of lVars * procIdent * openParen * callParams * closeParen | Stmt_IndirectCall of expr | Stmt_Assume of expr @@ -109,6 +104,14 @@ and var = VarLocalVar of localVar | VarGlobalVar of globalVar +and localVarParen = + LocalVarParenLocalVar of localVar + | LocalVarParen1 of openParen * localIdent * typeT * closeParen + +and globalVarParen = + GlobalVarParenGlobalVar of globalVar + | GlobalVarParen1 of openParen * globalIdent * typeT * closeParen + and namedCallReturn = NamedCallReturn1 of lVar * localIdent @@ -149,29 +152,24 @@ and phiAssign = and block = Block_NoPhi of blockIdent * attribSet * beginList * stmtWithAttrib list * jumpWithAttrib * endList - | Block_Phi of blockIdent * attribSet * beginList * openParen * phiAssign list * closeParen * stmtWithAttrib list * jumpWithAttrib * endList + | Block_Phi of blockIdent * attribSet * openParen * phiAssign list * closeParen * beginList * stmtWithAttrib list * jumpWithAttrib * endList and attrKeyValue = AttrKeyValue1 of bIdent * attr and attribSet = - AttribSet_Some of beginRec * attrKeyValue list * semicolons * endRec + AttribSet_Some of beginRec * attrKeyValue list * endRec | AttribSet_Empty and attr = - Attr_Map of beginRec * attrKeyValue list * semicolons * endRec + Attr_Map of beginRec * attrKeyValue list * endRec | Attr_List of beginList * attr list * endList - | Attr_Lit of value | Attr_Expr of expr | Attr_Str of str and params = Params1 of localIdent * typeT -and funParams = - FunParams1 of localIdent * typeT - | FunParams2 of openParen * localIdent * typeT * closeParen - and value = Value_BV of bVVal | Value_Int of intVal @@ -180,15 +178,13 @@ and value = and expr = Expr_Literal of value - | Expr_Paren of openParen * expr * closeParen | Expr_Local of localVar | Expr_Global of globalVar | Expr_Forall of attribSet * lambdaDef | Expr_Exists of attribSet * lambdaDef | Expr_Lambda of attribSet * lambdaDef | Expr_Old of openParen * expr * closeParen - | Expr_FunctionOp of globalIdent * openParen * expr list * closeParen - | Expr_Apply of expr * expr + | Expr_FunctionOp of expr * openParen * expr list * closeParen | Expr_Binary of binOp * openParen * expr * expr * closeParen | Expr_Assoc of boolBinOp * openParen * expr list * closeParen | Expr_Unary of unOp * openParen * expr * closeParen @@ -200,18 +196,14 @@ and expr = | Expr_Concat of openParen * expr list * closeParen | Expr_Match of expr * openParen * case list * closeParen | Expr_Cases of openParen * case list * closeParen - -and lParen = - LParenLocalVar of localVar - | LParen1 of openParen * localVar * closeParen + | Expr_Paren of openParen * expr * closeParen and lambdaDef = - LambdaDef1 of lParen list * lambdaSep * expr + LambdaDef1 of localVarParen list * lambdaSep * expr and binOp = BinOpBVBinOp of bVBinOp | BinOpBVLogicalBinOp of bVLogicalBinOp - | BinOpBoolBinOp of boolBinOp | BinOpIntLogicalBinOp of intLogicalBinOp | BinOpIntBinOp of intBinOp | BinOpEqOp of eqOp @@ -297,7 +289,7 @@ and relyTok = | RelyTok_relies and guarTok = - GuarTok_guarnatee + GuarTok_guarantee | GuarTok_guarantees and funSpec = @@ -314,6 +306,6 @@ and varSpec = | VarSpec_Empty and progSpec = - ProgSpec_Rely of expr - | ProgSpec_Guarantee of expr + ProgSpec_Rely of relyTok * expr + | ProgSpec_Guarantee of guarTok * expr diff --git a/lib/fe/BNFC_Util.ml b/lib/fe/BNFC_Util.ml index 6d3bb604..19303111 100644 --- a/lib/fe/BNFC_Util.ml +++ b/lib/fe/BNFC_Util.ml @@ -1,4 +1,4 @@ -(* File generated by the BNF Converter (bnfc 2.9.6.1). *) +(* File generated by the BNF Converter (bnfc 2.9.6.2). *) open Lexing diff --git a/lib/fe/BasilIR.cf b/lib/fe/BasilIR.cf index 0c320284..2db43f36 100644 --- a/lib/fe/BasilIR.cf +++ b/lib/fe/BasilIR.cf @@ -36,10 +36,6 @@ token Str '"' ((char - ["\"\\"]) | ('\\' ["\"\\tnrf"]))* '"' ; position token IntegerHex ('0' 'x' (digit | ["abcdef"])+); position token IntegerDec (digit+); --- gobble extra semicolons -Semicolons_Empty . Semicolons ::= ""; -Semicolons_Some . Semicolons ::= Semicolons ";" ; - comment "//" ; comment "/*" "*/" ; @@ -63,17 +59,21 @@ Decl_ProgEmpty . Decl ::= "prog" "entry" ProcIdent AttribSet ; Decl_ProgWithSpec . Decl ::= "prog" "entry" ProcIdent AttribSet [ ProgSpec ] ; Decl_Proc . Decl ::= "proc" ProcIdent OpenParen [Params] CloseParen "->" OpenParen [Params] CloseParen AttribSet [ FunSpec ] ProcDef ; -ProcDef_Empty . ProcDef ::= ""; +ProcDef_Empty . ProcDef ::= ; ProcDef_Some . ProcDef ::= BeginList [Block] EndList ; IntType1 . IntType ::= INTTYPE ; BoolType1. BoolType ::= BOOLTYPE ; -MapType1 . MapType ::= Type "->" Type ; BVType1 . BVType ::= BVTYPE ; +-- map types are right associative. left of -> cannot be another MapType. +MapType1 . MapType ::= Type1 "->" Type ; -rules Type ::= IntType | BoolType | MapType | BVType | OpenParen Type CloseParen; - -separator Expr "," ; +TypeIntType . Type1 ::= IntType ; +TypeBoolType . Type1 ::= BoolType ; +TypeBVType . Type1 ::= BVType ; +TypeParen . Type1 ::= OpenParen Type CloseParen; +TypeMapType . Type ::= MapType; +_ . Type ::= Type1; IntVal_Hex . IntVal ::= IntegerHex ; IntVal_Dec . IntVal ::= IntegerDec ; @@ -95,33 +95,40 @@ separator nonempty Assignment ","; Stmt_MultiAssign . Stmt ::= OpenParen [Assignment] CloseParen ; -LocalTyped . LocalVar ::= LocalIdent ":" Type ; +LocalTyped . LocalVar ::= LocalIdent ":" Type1 ; LocalUntyped . LocalVar ::= LocalIdent ; +separator nonempty LocalVar ","; -GlobalTyped . GlobalVar ::= GlobalIdent ":" Type ; +GlobalTyped . GlobalVar ::= GlobalIdent ":" Type1 ; GlobalUntyped . GlobalVar ::= GlobalIdent; -separator nonempty LocalVar ","; +separator GlobalVar ","; + rules Var ::= LocalVar | GlobalVar ; -separator GlobalVar ","; +-- Variant of LocalVar / GlobalVar which can be wrapped in parens and +-- can contain any type. +rules LocalVarParen ::= LocalVar | OpenParen LocalIdent ":" Type CloseParen ; +rules GlobalVarParen ::= GlobalVar | OpenParen GlobalIdent ":" Type CloseParen ; +separator LocalVarParen ","; -Stmt_Load . Stmt ::= LVar ":=" "load" Endian GlobalIdent Expr IntVal; -Stmt_Store . Stmt ::= "store" Endian GlobalIdent Expr Expr IntVal; +-- lvar endian mem addr size +Stmt_Load_Var . Stmt ::= LVar ":=" "load" Endian Var Expr IntVal; -Stmt_Load_Var . Stmt ::= LVar ":=" "load" Endian Var Expr IntVal; -Stmt_Store_Var . Stmt ::= LVar ":=" "store" Endian Var Expr Expr IntVal; +-- lhs endian rhs addr value size +Stmt_Store_Var . Stmt ::= LVar ":=" "store" Endian Var Expr2 Expr IntVal; +Stmt_Store . Stmt ::= "store" Endian GlobalIdent Expr2 Expr IntVal; rules NamedCallReturn ::= LVar "=" LocalIdent; separator NamedCallReturn "," ; -LVars_Empty . LVars ::= ""; +LVars_Empty . LVars ::= ; LVars_LocalList . LVars ::= "var" OpenParen [ LocalVar ] CloseParen ":=" ; LVars_List . LVars ::= OpenParen [ LVar ] CloseParen ":="; NamedLVars_List . LVars ::= OpenParen [NamedCallReturn] CloseParen ":="; rules NamedCallArg ::= LocalIdent "=" Expr; -separator NamedCallArg "," ; +separator nonempty NamedCallArg "," ; CallParams_Exprs . CallParams ::= [Expr]; CallParams_Named . CallParams ::= [NamedCallArg]; @@ -161,31 +168,29 @@ Block_NoPhi . Block ::= "block" BlockIdent AttribSet BeginList [StmtWithAttrib] JumpWithAttrib ";" EndList ; -Block_Phi . Block ::= "block" BlockIdent AttribSet BeginList - OpenParen [PhiAssign] CloseParen ";" +Block_Phi . Block ::= "block" BlockIdent AttribSet + OpenParen [PhiAssign] CloseParen + BeginList [StmtWithAttrib] JumpWithAttrib ";" EndList ; rules AttrKeyValue ::= BIdent "=" Attr ; separator AttrKeyValue ";"; +-- in BNFC, `separator` also allows trailing -AttribSet_Some . AttribSet ::= BeginRec [ AttrKeyValue ] Semicolons EndRec; -AttribSet_Empty . AttribSet ::= "" ; +AttribSet_Some . AttribSet ::= BeginRec [ AttrKeyValue ] EndRec; +AttribSet_Empty . AttribSet ::= ; separator Attr ";" ; -Attr_Map . Attr ::= BeginRec [ AttrKeyValue ] Semicolons EndRec ; +Attr_Map . Attr ::= BeginRec [ AttrKeyValue ] EndRec ; Attr_List . Attr ::= BeginList [ Attr ] EndList; -Attr_Lit . Attr ::= Value ; Attr_Expr . Attr ::= Expr; Attr_Str . Attr ::= Str ; rules Params ::= LocalIdent ":" Type ; separator Params "," ; -rules FunParams ::= LocalIdent ":" Type | OpenParen LocalIdent ":" Type CloseParen ; -separator FunParams " " ; - {- EXPRESSIONS -} Value_BV . Value ::= BVVal; @@ -193,51 +198,56 @@ Value_Int . Value ::= IntVal; Value_True . Value ::= "true" ; Value_False . Value ::= "false" ; -Expr_Literal . Expr ::= Value; +-- Expressions have precedence. Expr2 is highest precedence/strongest/indivisible, +-- Expr1 is function application, and Expr is the lowest precedence. +-- Intuitively, lowest precedence things will capture more things, e.g., the +-- quantified statements continue to the end of the expression or paren. +-- In certain places, only stronger precedence things are allowed. +separator Expr "," ; -Expr_Paren . Expr ::= OpenParen Expr CloseParen; +_ . Expr ::= Expr1; +_ . Expr1 ::= Expr2; -Expr_Local . Expr ::= LocalVar; -Expr_Global . Expr ::= GlobalVar; +Expr_Literal . Expr2 ::= Value; --- quantifiers +Expr_Local . Expr2 ::= LocalVar; +Expr_Global . Expr2 ::= GlobalVar; -rules LParen ::= LocalVar | OpenParen LocalVar CloseParen ; -separator LParen ","; +-- quantifiers -rules LambdaDef ::= [LParen] LambdaSep Expr ; -Expr_Forall . Expr ::= "forall" AttribSet LambdaDef ; -Expr_Exists . Expr ::= "exists" AttribSet LambdaDef ; -Expr_Lambda . Expr ::= "fun" AttribSet LambdaDef ; -Expr_Old . Expr ::= "old" OpenParen Expr CloseParen ; +rules LambdaDef ::= [LocalVarParen] LambdaSep Expr ; +Expr_Forall . Expr ::= "forall" AttribSet LambdaDef ; +Expr_Exists . Expr ::= "exists" AttribSet LambdaDef ; +Expr_Lambda . Expr ::= "fun" AttribSet LambdaDef ; +Expr_Old . Expr2 ::= "old" OpenParen Expr CloseParen ; -- uninterpreted functions -Expr_FunctionOp . Expr ::= GlobalIdent OpenParen [Expr] CloseParen; -Expr_Apply . Expr ::= Expr Expr; +Expr_FunctionOp . Expr1 ::= Expr1 OpenParen [Expr] CloseParen; -- binary expr -rules BinOp ::= BVBinOp | BVLogicalBinOp | BoolBinOp | IntLogicalBinOp | IntBinOp | EqOp ; -Expr_Binary . Expr ::= BinOp OpenParen Expr "," Expr CloseParen ; -Expr_Assoc . Expr ::= BoolBinOp OpenParen [Expr] CloseParen ; +rules BinOp ::= BVBinOp | BVLogicalBinOp | IntLogicalBinOp | IntBinOp | EqOp ; +Expr_Binary . Expr2 ::= BinOp OpenParen Expr "," Expr CloseParen ; +Expr_Assoc . Expr2 ::= BoolBinOp OpenParen [Expr] CloseParen ; rules UnOp ::= BVUnOp | "boolnot" | "intneg" | "booltobv1" | "gamma" | "classification"; -Expr_Unary . Expr ::= UnOp OpenParen Expr CloseParen ; +Expr_Unary . Expr2 ::= UnOp OpenParen Expr CloseParen ; -Expr_LoadBe . Expr ::= "load_be" OpenParen IntVal "," Expr "," Expr CloseParen ; -Expr_LoadLe . Expr ::= "load_le" OpenParen IntVal "," Expr "," Expr CloseParen ; +Expr_LoadBe . Expr2 ::= "load_be" OpenParen IntVal "," Expr "," Expr CloseParen ; +Expr_LoadLe . Expr2 ::= "load_le" OpenParen IntVal "," Expr "," Expr CloseParen ; -Expr_ZeroExtend . Expr ::= "zero_extend" OpenParen IntVal "," Expr CloseParen ; -Expr_SignExtend . Expr ::= "sign_extend" OpenParen IntVal "," Expr CloseParen ; -Expr_Extract . Expr ::= "extract" OpenParen IntVal "," IntVal "," Expr CloseParen ; -Expr_Concat . Expr ::= "bvconcat" OpenParen [Expr] CloseParen ; +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 ; CaseCase . Case ::= Expr "->" Expr ; CaseDefault . Case ::= "_" "->" Expr ; separator Case "|" ; -Expr_Match . Expr ::= "match" Expr "with" OpenParen [Case] CloseParen ; -Expr_Cases . Expr ::= "cases" OpenParen [Case] CloseParen ; +Expr_Match . Expr2 ::= "match" Expr "with" OpenParen [Case] CloseParen ; +Expr_Cases . Expr2 ::= "cases" OpenParen [Case] CloseParen ; +Expr_Paren . Expr2 ::= OpenParen Expr CloseParen ; -- operators @@ -257,7 +267,7 @@ rules BoolBinOp ::= "booland" | "boolor" | "boolimplies" ; rules RequireTok ::= "require" | "requires" ; rules EnsureTok ::= "ensure" | "ensures" ; rules RelyTok ::= "rely" | "relies"; -rules GuarTok ::= "guarnatee" | "guarantees"; +rules GuarTok ::= "guarantee" | "guarantees"; FunSpec_Require . FunSpec ::= RequireTok Expr; FunSpec_Ensure . FunSpec ::= EnsureTok Expr; @@ -268,18 +278,18 @@ FunSpec_Modifies . FunSpec ::= "modifies" [GlobalVar]; VarSpec_Classification . VarSpec ::= "classification" Expr; -VarSpec_Empty . VarSpec ::= ""; +VarSpec_Empty . VarSpec ::= ; FunSpec_Invariant . FunSpec ::= "invariant" BlockIdent Expr; -ProgSpec_Rely . ProgSpec ::= "rely" Expr; -ProgSpec_Guarantee . ProgSpec ::= "guarantee" Expr; +ProgSpec_Rely . ProgSpec ::= RelyTok Expr; +ProgSpec_Guarantee . ProgSpec ::= GuarTok Expr; -terminator FunSpec ";"; +terminator FunSpec "\n"; {- last semicolon terminates the prog definitino -} -separator ProgSpec ";"; +terminator nonempty ProgSpec "\n"; diff --git a/lib/fe/LexBasilIR.mll b/lib/fe/LexBasilIR.mll index 03c476e0..879eb028 100644 --- a/lib/fe/LexBasilIR.mll +++ b/lib/fe/LexBasilIR.mll @@ -1,4 +1,4 @@ -(* File generated by the BNF Converter (bnfc 2.9.6.1). *) +(* File generated by the BNF Converter (bnfc 2.9.6.2). *) (* Lexer definition for ocamllex. *) @@ -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);("mem:=", SYMB8);("_", SYMB9);("|", SYMB10)] -let resword_table = Hashtbl.create 99 +let resword_table = Hashtbl.create 98 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);("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);("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);("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);("require", KW_require);("requires", KW_requires);("ensure", KW_ensure);("ensures", KW_ensures);("rely", KW_rely);("relies", KW_relies);("guarnatee", KW_guarnatee);("guarantees", KW_guarantees);("captures", KW_captures);("modifies", KW_modifies);("invariant", KW_invariant);("guarantee", KW_guarantee)] + [("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);("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);("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);("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);("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 bd2211fc..375804f1 100644 --- a/lib/fe/ParBasilIR.mly +++ b/lib/fe/ParBasilIR.mly @@ -1,4 +1,4 @@ -/* File generated by the BNF Converter (bnfc 2.9.6.1). */ +/* File generated by the BNF Converter (bnfc 2.9.6.2). */ /* Parser definition for use with menhir */ @@ -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_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_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_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_require KW_requires KW_ensure KW_ensures KW_rely KW_relies KW_guarnatee KW_guarantees KW_captures KW_modifies KW_invariant KW_guarantee +%token KW_shared KW_observable KW_axiom KW_memory KW_var KW_val KW_let KW_prog KW_entry KW_proc 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_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_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_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 /* , */ @@ -44,12 +44,11 @@ open Lexing %token <(int * int) * string> TOK_IntegerHex %token <(int * int) * string> TOK_IntegerDec -%start pModuleT pDecl_list pBlockIdent_list pLambdaSep pSemicolons pVarModifiers pVarModifiers_list pDecl pTypeT_list pProcDef pIntType pBoolType pMapType pBVType pTypeT pExpr_list pIntVal pBVVal pEndian pAssignment pStmt pAssignment_list pLocalVar pGlobalVar pLocalVar_list pVar pGlobalVar_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 pFunParams pFunParams_list pValue pExpr pLParen pLParen_list pLambdaDef pBinOp pUnOp pCase pCase_list pEqOp pBVUnOp pBVBinOp pBVLogicalBinOp pIntBinOp pIntLogicalBinOp pBoolBinOp pRequireTok pEnsureTok pRelyTok pGuarTok pFunSpec pVarSpec pProgSpec pFunSpec_list pProgSpec_list +%start pModuleT pDecl_list pBlockIdent_list pLambdaSep pVarModifiers pVarModifiers_list pDecl pTypeT_list pProcDef pIntType pBoolType pBVType pMapType pType1 pTypeT pIntVal pBVVal 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 pRequireTok pEnsureTok pRelyTok pGuarTok pFunSpec pVarSpec pProgSpec pFunSpec_list pProgSpec_list %type pModuleT %type pDecl_list %type pBlockIdent_list %type pLambdaSep -%type pSemicolons %type pVarModifiers %type pVarModifiers_list %type pDecl @@ -57,10 +56,10 @@ open Lexing %type pProcDef %type pIntType %type pBoolType -%type pMapType %type pBVType +%type pMapType +%type pType1 %type pTypeT -%type pExpr_list %type pIntVal %type pBVVal %type pEndian @@ -68,10 +67,13 @@ open Lexing %type pStmt %type pAssignment_list %type pLocalVar -%type pGlobalVar %type pLocalVar_list -%type pVar +%type pGlobalVar %type pGlobalVar_list +%type pVar +%type pLocalVarParen +%type pGlobalVarParen +%type pLocalVarParen_list %type pNamedCallReturn %type pNamedCallReturn_list %type pLVars @@ -97,12 +99,11 @@ open Lexing %type pAttr %type pParams %type pParams_list -%type pFunParams -%type pFunParams_list %type pValue +%type pExpr_list %type pExpr -%type pLParen -%type pLParen_list +%type pExpr1 +%type pExpr2 %type pLambdaDef %type pBinOp %type pUnOp @@ -129,7 +130,6 @@ open Lexing %type decl_list %type blockIdent_list %type lambdaSep -%type semicolons %type varModifiers %type varModifiers_list %type decl @@ -137,10 +137,10 @@ open Lexing %type procDef %type intType %type boolType -%type mapType %type bVType +%type mapType +%type type1 %type typeT -%type expr_list %type intVal %type bVVal %type endian @@ -148,10 +148,13 @@ open Lexing %type stmt %type assignment_list %type localVar -%type globalVar %type localVar_list -%type var +%type globalVar %type globalVar_list +%type var +%type localVarParen +%type globalVarParen +%type localVarParen_list %type namedCallReturn %type namedCallReturn_list %type lVars @@ -177,12 +180,11 @@ open Lexing %type attr %type params %type params_list -%type funParams -%type funParams_list %type value +%type expr_list %type expr -%type lParen -%type lParen_list +%type expr1 +%type expr2 %type lambdaDef %type binOp %type unOp @@ -233,8 +235,6 @@ pBlockIdent_list : blockIdent_list TOK_EOF { $1 }; pLambdaSep : lambdaSep TOK_EOF { $1 }; -pSemicolons : semicolons TOK_EOF { $1 }; - pVarModifiers : varModifiers TOK_EOF { $1 }; pVarModifiers_list : varModifiers_list TOK_EOF { $1 }; @@ -249,14 +249,14 @@ pIntType : intType TOK_EOF { $1 }; pBoolType : boolType TOK_EOF { $1 }; +pBVType : bVType TOK_EOF { $1 }; + pMapType : mapType TOK_EOF { $1 }; -pBVType : bVType TOK_EOF { $1 }; +pType1 : type1 TOK_EOF { $1 }; pTypeT : typeT TOK_EOF { $1 }; -pExpr_list : expr_list TOK_EOF { $1 }; - pIntVal : intVal TOK_EOF { $1 }; pBVVal : bVVal TOK_EOF { $1 }; @@ -271,13 +271,19 @@ pAssignment_list : assignment_list TOK_EOF { $1 }; pLocalVar : localVar TOK_EOF { $1 }; +pLocalVar_list : localVar_list TOK_EOF { $1 }; + pGlobalVar : globalVar TOK_EOF { $1 }; -pLocalVar_list : localVar_list TOK_EOF { $1 }; +pGlobalVar_list : globalVar_list TOK_EOF { $1 }; pVar : var TOK_EOF { $1 }; -pGlobalVar_list : globalVar_list TOK_EOF { $1 }; +pLocalVarParen : localVarParen TOK_EOF { $1 }; + +pGlobalVarParen : globalVarParen TOK_EOF { $1 }; + +pLocalVarParen_list : localVarParen_list TOK_EOF { $1 }; pNamedCallReturn : namedCallReturn TOK_EOF { $1 }; @@ -329,17 +335,15 @@ pParams : params TOK_EOF { $1 }; pParams_list : params_list TOK_EOF { $1 }; -pFunParams : funParams TOK_EOF { $1 }; - -pFunParams_list : funParams_list TOK_EOF { $1 }; - pValue : value TOK_EOF { $1 }; +pExpr_list : expr_list TOK_EOF { $1 }; + pExpr : expr TOK_EOF { $1 }; -pLParen : lParen TOK_EOF { $1 }; +pExpr1 : expr1 TOK_EOF { $1 }; -pLParen_list : lParen_list TOK_EOF { $1 }; +pExpr2 : expr2 TOK_EOF { $1 }; pLambdaDef : lambdaDef TOK_EOF { $1 }; @@ -399,10 +403,6 @@ lambdaSep : SYMB3 { LambdaSep1 } | SYMB4 { LambdaSep2 } ; -semicolons : /* empty */ { Semicolons_Empty } - | semicolons SYMB1 { Semicolons_Some $1 } - ; - varModifiers : KW_shared { Shared } | KW_observable { Observable } ; @@ -437,22 +437,20 @@ intType : iNTTYPE { IntType1 $1 } boolType : bOOLTYPE { BoolType1 $1 } ; -mapType : typeT SYMB3 typeT { MapType1 ($1, $3) } +bVType : bVTYPE { BVType1 $1 } ; -bVType : bVTYPE { BVType1 $1 } +mapType : type1 SYMB3 typeT { MapType1 ($1, $3) } ; -typeT : intType { TypeIntType $1 } +type1 : intType { TypeIntType $1 } | boolType { TypeBoolType $1 } - | mapType { TypeMapType $1 } | bVType { TypeBVType $1 } - | openParen typeT closeParen { Type1 ($1, $2, $3) } + | openParen typeT closeParen { TypeParen ($1, $2, $3) } ; -expr_list : /* empty */ { [] } - | expr { (fun x -> [x]) $1 } - | expr SYMB2 expr_list { (fun (x,xs) -> x::xs) ($1, $3) } +typeT : mapType { TypeMapType $1 } + | type1 { $1 } ; intVal : integerHex { IntVal_Hex $1 } @@ -475,10 +473,9 @@ stmt : KW_nop { Stmt_Nop } | lVar SYMB7 KW_store expr { Stmt_ScalarStore ($1, $4) } | lVar SYMB7 KW_load var { Stmt_ScalarLoad ($1, $4) } | openParen assignment_list closeParen { Stmt_MultiAssign ($1, $2, $3) } - | lVar SYMB7 KW_load endian globalIdent expr intVal { Stmt_Load ($1, $4, $5, $6, $7) } - | KW_store endian globalIdent expr expr intVal { Stmt_Store ($2, $3, $4, $5, $6) } | lVar SYMB7 KW_load endian var expr intVal { Stmt_Load_Var ($1, $4, $5, $6, $7) } - | lVar SYMB7 KW_store endian var expr expr intVal { Stmt_Store_Var ($1, $4, $5, $6, $7, $8) } + | lVar SYMB7 KW_store endian var expr2 expr intVal { Stmt_Store_Var ($1, $4, $5, $6, $7, $8) } + | KW_store endian globalIdent expr2 expr intVal { Stmt_Store ($2, $3, $4, $5, $6) } | lVars KW_call procIdent openParen callParams closeParen { Stmt_DirectCall ($1, $3, $4, $5, $6) } | KW_indirect KW_call expr { Stmt_IndirectCall $3 } | KW_assume expr { Stmt_Assume $2 } @@ -490,20 +487,16 @@ assignment_list : assignment { (fun x -> [x]) $1 } | assignment SYMB2 assignment_list { (fun (x,xs) -> x::xs) ($1, $3) } ; -localVar : localIdent SYMB5 typeT { LocalTyped ($1, $3) } +localVar : localIdent SYMB5 type1 { LocalTyped ($1, $3) } | localIdent { LocalUntyped $1 } ; -globalVar : globalIdent SYMB5 typeT { GlobalTyped ($1, $3) } - | globalIdent { GlobalUntyped $1 } - ; - localVar_list : localVar { (fun x -> [x]) $1 } | localVar SYMB2 localVar_list { (fun (x,xs) -> x::xs) ($1, $3) } ; -var : localVar { VarLocalVar $1 } - | globalVar { VarGlobalVar $1 } +globalVar : globalIdent SYMB5 type1 { GlobalTyped ($1, $3) } + | globalIdent { GlobalUntyped $1 } ; globalVar_list : /* empty */ { [] } @@ -511,6 +504,23 @@ globalVar_list : /* empty */ { [] } | globalVar SYMB2 globalVar_list { (fun (x,xs) -> x::xs) ($1, $3) } ; +var : localVar { VarLocalVar $1 } + | globalVar { VarGlobalVar $1 } + ; + +localVarParen : localVar { LocalVarParenLocalVar $1 } + | openParen localIdent SYMB5 typeT closeParen { LocalVarParen1 ($1, $2, $4, $5) } + ; + +globalVarParen : globalVar { GlobalVarParenGlobalVar $1 } + | openParen globalIdent SYMB5 typeT closeParen { GlobalVarParen1 ($1, $2, $4, $5) } + ; + +localVarParen_list : /* empty */ { [] } + | localVarParen { (fun x -> [x]) $1 } + | localVarParen SYMB2 localVarParen_list { (fun (x,xs) -> x::xs) ($1, $3) } + ; + namedCallReturn : lVar SYMB6 localIdent { NamedCallReturn1 ($1, $3) } ; @@ -528,8 +538,7 @@ lVars : /* empty */ { LVars_Empty } namedCallArg : localIdent SYMB6 expr { NamedCallArg1 ($1, $3) } ; -namedCallArg_list : /* empty */ { [] } - | namedCallArg { (fun x -> [x]) $1 } +namedCallArg_list : namedCallArg { (fun x -> [x]) $1 } | namedCallArg SYMB2 namedCallArg_list { (fun (x,xs) -> x::xs) ($1, $3) } ; @@ -583,7 +592,7 @@ phiAssign_list : /* empty */ { [] } ; block : KW_block blockIdent attribSet beginList stmtWithAttrib_list jumpWithAttrib SYMB1 endList { Block_NoPhi ($2, $3, $4, $5, $6, $8) } - | KW_block blockIdent attribSet beginList openParen phiAssign_list closeParen SYMB1 stmtWithAttrib_list jumpWithAttrib SYMB1 endList { Block_Phi ($2, $3, $4, $5, $6, $7, $9, $10, $12) } + | KW_block blockIdent attribSet openParen phiAssign_list closeParen beginList stmtWithAttrib_list jumpWithAttrib SYMB1 endList { Block_Phi ($2, $3, $4, $5, $6, $7, $8, $9, $11) } ; attrKeyValue : bIdent SYMB6 attr { AttrKeyValue1 ($1, $3) } @@ -594,7 +603,7 @@ attrKeyValue_list : /* empty */ { [] } | attrKeyValue SYMB1 attrKeyValue_list { (fun (x,xs) -> x::xs) ($1, $3) } ; -attribSet : beginRec attrKeyValue_list semicolons endRec { AttribSet_Some ($1, $2, $3, $4) } +attribSet : beginRec attrKeyValue_list endRec { AttribSet_Some ($1, $2, $3) } | /* empty */ { AttribSet_Empty } ; @@ -603,9 +612,8 @@ attr_list : /* empty */ { [] } | attr SYMB1 attr_list { (fun (x,xs) -> x::xs) ($1, $3) } ; -attr : beginRec attrKeyValue_list semicolons endRec { Attr_Map ($1, $2, $3, $4) } +attr : beginRec attrKeyValue_list endRec { Attr_Map ($1, $2, $3) } | beginList attr_list endList { Attr_List ($1, $2, $3) } - | value { Attr_Lit $1 } | expr { Attr_Expr $1 } | str { Attr_Str $1 } ; @@ -618,30 +626,31 @@ params_list : /* empty */ { [] } | params SYMB2 params_list { (fun (x,xs) -> x::xs) ($1, $3) } ; -funParams : localIdent SYMB5 typeT { FunParams1 ($1, $3) } - | openParen localIdent SYMB5 typeT closeParen { FunParams2 ($1, $2, $4, $5) } - ; - -funParams_list : /* empty */ { [] } - | funParams funParams_list { (fun (x,xs) -> x::xs) ($1, $2) } - ; - value : bVVal { Value_BV $1 } | intVal { Value_Int $1 } | KW_true { Value_True } | KW_false { Value_False } ; -expr : value { Expr_Literal $1 } - | openParen expr closeParen { Expr_Paren ($1, $2, $3) } - | localVar { Expr_Local $1 } - | globalVar { Expr_Global $1 } +expr_list : /* empty */ { [] } + | expr { (fun x -> [x]) $1 } + | expr SYMB2 expr_list { (fun (x,xs) -> x::xs) ($1, $3) } + ; + +expr : expr1 { $1 } | KW_forall attribSet lambdaDef { Expr_Forall ($2, $3) } | KW_exists attribSet lambdaDef { Expr_Exists ($2, $3) } | KW_fun attribSet lambdaDef { Expr_Lambda ($2, $3) } + ; + +expr1 : expr2 { $1 } + | expr1 openParen expr_list closeParen { Expr_FunctionOp ($1, $2, $3, $4) } + ; + +expr2 : value { Expr_Literal $1 } + | localVar { Expr_Local $1 } + | globalVar { Expr_Global $1 } | KW_old openParen expr closeParen { Expr_Old ($2, $3, $4) } - | globalIdent openParen expr_list closeParen { Expr_FunctionOp ($1, $2, $3, $4) } - | expr expr { Expr_Apply ($1, $2) } | binOp openParen expr SYMB2 expr closeParen { Expr_Binary ($1, $2, $3, $5, $6) } | boolBinOp openParen expr_list closeParen { Expr_Assoc ($1, $2, $3, $4) } | unOp openParen expr closeParen { Expr_Unary ($1, $2, $3, $4) } @@ -653,23 +662,14 @@ expr : value { Expr_Literal $1 } | KW_bvconcat openParen expr_list closeParen { Expr_Concat ($2, $3, $4) } | 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) } ; -lParen : localVar { LParenLocalVar $1 } - | openParen localVar closeParen { LParen1 ($1, $2, $3) } - ; - -lParen_list : /* empty */ { [] } - | lParen { (fun x -> [x]) $1 } - | lParen SYMB2 lParen_list { (fun (x,xs) -> x::xs) ($1, $3) } - ; - -lambdaDef : lParen_list lambdaSep expr { LambdaDef1 ($1, $2, $3) } +lambdaDef : localVarParen_list lambdaSep expr { LambdaDef1 ($1, $2, $3) } ; binOp : bVBinOp { BinOpBVBinOp $1 } | bVLogicalBinOp { BinOpBVLogicalBinOp $1 } - | boolBinOp { BinOpBoolBinOp $1 } | intLogicalBinOp { BinOpIntLogicalBinOp $1 } | intBinOp { BinOpIntBinOp $1 } | eqOp { BinOpEqOp $1 } @@ -760,7 +760,7 @@ relyTok : KW_rely { RelyTok_rely } | KW_relies { RelyTok_relies } ; -guarTok : KW_guarnatee { GuarTok_guarnatee } +guarTok : KW_guarantee { GuarTok_guarantee } | KW_guarantees { GuarTok_guarantees } ; @@ -777,17 +777,16 @@ varSpec : KW_classification expr { VarSpec_Classification $2 } | /* empty */ { VarSpec_Empty } ; -progSpec : KW_rely expr { ProgSpec_Rely $2 } - | KW_guarantee expr { ProgSpec_Guarantee $2 } +progSpec : relyTok expr { ProgSpec_Rely ($1, $2) } + | guarTok expr { ProgSpec_Guarantee ($1, $2) } ; funSpec_list : /* empty */ { [] } - | funSpec SYMB1 funSpec_list { (fun (x,xs) -> x::xs) ($1, $3) } + | funSpec funSpec_list { (fun (x,xs) -> x::xs) ($1, $2) } ; -progSpec_list : /* empty */ { [] } - | progSpec { (fun x -> [x]) $1 } - | progSpec SYMB1 progSpec_list { (fun (x,xs) -> x::xs) ($1, $3) } +progSpec_list : progSpec { (fun x -> [x]) $1 } + | progSpec progSpec_list { (fun (x,xs) -> x::xs) ($1, $2) } ; bVTYPE : TOK_BVTYPE { BVTYPE ($1)}; diff --git a/lib/fe/PrintBasilIR.ml b/lib/fe/PrintBasilIR.ml index 71da2133..a10cc9e1 100644 --- a/lib/fe/PrintBasilIR.ml +++ b/lib/fe/PrintBasilIR.ml @@ -1,4 +1,4 @@ -(* File generated by the BNF Converter (bnfc 2.9.6.1). *) +(* File generated by the BNF Converter (bnfc 2.9.6.2). *) (* pretty-printer *) @@ -145,11 +145,6 @@ and prtLambdaSep (i:int) (e : AbsBasilIR.lambdaSep) : doc = match e with | AbsBasilIR.LambdaSep2 -> prPrec i 0 (concatD [render "::"]) -and prtSemicolons (i:int) (e : AbsBasilIR.semicolons) : doc = match e with - AbsBasilIR.Semicolons_Empty -> prPrec i 0 (concatD []) - | AbsBasilIR.Semicolons_Some semicolons -> prPrec i 0 (concatD [prtSemicolons 0 semicolons ; render ";"]) - - and prtVarModifiers (i:int) (e : AbsBasilIR.varModifiers) : doc = match e with AbsBasilIR.Shared -> prPrec i 0 (concatD [render "shared"]) | AbsBasilIR.Observable -> prPrec i 0 (concatD [render "observable"]) @@ -184,20 +179,20 @@ and prtBoolType (i:int) (e : AbsBasilIR.boolType) : doc = match e with AbsBasilIR.BoolType1 booltype -> prPrec i 0 (concatD [prtBOOLTYPE 0 booltype]) -and prtMapType (i:int) (e : AbsBasilIR.mapType) : doc = match e with - AbsBasilIR.MapType1 (type_1, type_2) -> prPrec i 0 (concatD [prtTypeT 0 type_1 ; render "->" ; prtTypeT 0 type_2]) - - and prtBVType (i:int) (e : AbsBasilIR.bVType) : doc = match e with AbsBasilIR.BVType1 bvtype -> prPrec i 0 (concatD [prtBVTYPE 0 bvtype]) +and prtMapType (i:int) (e : AbsBasilIR.mapType) : doc = match e with + AbsBasilIR.MapType1 (type_1, type_2) -> prPrec i 0 (concatD [prtTypeT 1 type_1 ; render "->" ; prtTypeT 0 type_2]) + + and prtTypeT (i:int) (e : AbsBasilIR.typeT) : doc = match e with - AbsBasilIR.TypeIntType inttype -> prPrec i 0 (concatD [prtIntType 0 inttype]) - | AbsBasilIR.TypeBoolType booltype -> prPrec i 0 (concatD [prtBoolType 0 booltype]) + AbsBasilIR.TypeIntType inttype -> prPrec i 1 (concatD [prtIntType 0 inttype]) + | AbsBasilIR.TypeBoolType booltype -> prPrec i 1 (concatD [prtBoolType 0 booltype]) + | AbsBasilIR.TypeBVType bvtype -> prPrec i 1 (concatD [prtBVType 0 bvtype]) + | AbsBasilIR.TypeParen (openparen, type_, closeparen) -> prPrec i 1 (concatD [prtOpenParen 0 openparen ; prtTypeT 0 type_ ; prtCloseParen 0 closeparen]) | AbsBasilIR.TypeMapType maptype -> prPrec i 0 (concatD [prtMapType 0 maptype]) - | AbsBasilIR.TypeBVType bvtype -> prPrec i 0 (concatD [prtBVType 0 bvtype]) - | AbsBasilIR.Type1 (openparen, type_, closeparen) -> prPrec i 0 (concatD [prtOpenParen 0 openparen ; prtTypeT 0 type_ ; prtCloseParen 0 closeparen]) and prtTypeTListBNFC i es : doc = match (i, es) with (_,[]) -> (concatD []) @@ -231,10 +226,9 @@ and prtStmt (i:int) (e : AbsBasilIR.stmt) : doc = match e with | AbsBasilIR.Stmt_ScalarStore (lvar, expr) -> prPrec i 0 (concatD [prtLVar 0 lvar ; render ":=" ; render "store" ; prtExpr 0 expr]) | AbsBasilIR.Stmt_ScalarLoad (lvar, var) -> prPrec i 0 (concatD [prtLVar 0 lvar ; render ":=" ; render "load" ; prtVar 0 var]) | AbsBasilIR.Stmt_MultiAssign (openparen, assignments, closeparen) -> prPrec i 0 (concatD [prtOpenParen 0 openparen ; prtAssignmentListBNFC 0 assignments ; prtCloseParen 0 closeparen]) - | AbsBasilIR.Stmt_Load (lvar, endian, globalident, expr, intval) -> prPrec i 0 (concatD [prtLVar 0 lvar ; render ":=" ; render "load" ; prtEndian 0 endian ; prtGlobalIdent 0 globalident ; prtExpr 0 expr ; prtIntVal 0 intval]) - | AbsBasilIR.Stmt_Store (endian, globalident, expr1, expr2, intval) -> prPrec i 0 (concatD [render "store" ; prtEndian 0 endian ; prtGlobalIdent 0 globalident ; prtExpr 0 expr1 ; prtExpr 0 expr2 ; prtIntVal 0 intval]) | AbsBasilIR.Stmt_Load_Var (lvar, endian, var, expr, intval) -> prPrec i 0 (concatD [prtLVar 0 lvar ; render ":=" ; render "load" ; prtEndian 0 endian ; prtVar 0 var ; prtExpr 0 expr ; prtIntVal 0 intval]) - | AbsBasilIR.Stmt_Store_Var (lvar, endian, var, expr1, expr2, intval) -> prPrec i 0 (concatD [prtLVar 0 lvar ; render ":=" ; render "store" ; prtEndian 0 endian ; prtVar 0 var ; prtExpr 0 expr1 ; prtExpr 0 expr2 ; prtIntVal 0 intval]) + | AbsBasilIR.Stmt_Store_Var (lvar, endian, var, expr1, expr2, intval) -> prPrec i 0 (concatD [prtLVar 0 lvar ; render ":=" ; render "store" ; prtEndian 0 endian ; prtVar 0 var ; prtExpr 2 expr1 ; prtExpr 0 expr2 ; prtIntVal 0 intval]) + | AbsBasilIR.Stmt_Store (endian, globalident, expr1, expr2, intval) -> prPrec i 0 (concatD [render "store" ; prtEndian 0 endian ; prtGlobalIdent 0 globalident ; prtExpr 2 expr1 ; prtExpr 0 expr2 ; prtIntVal 0 intval]) | AbsBasilIR.Stmt_DirectCall (lvars, procident, openparen, callparams, closeparen) -> prPrec i 0 (concatD [prtLVars 0 lvars ; render "call" ; prtProcIdent 0 procident ; prtOpenParen 0 openparen ; prtCallParams 0 callparams ; prtCloseParen 0 closeparen]) | AbsBasilIR.Stmt_IndirectCall expr -> prPrec i 0 (concatD [render "indirect" ; render "call" ; prtExpr 0 expr]) | AbsBasilIR.Stmt_Assume expr -> prPrec i 0 (concatD [render "assume" ; prtExpr 0 expr]) @@ -243,7 +237,7 @@ and prtStmt (i:int) (e : AbsBasilIR.stmt) : doc = match e with and prtLocalVar (i:int) (e : AbsBasilIR.localVar) : doc = match e with - AbsBasilIR.LocalTyped (localident, type_) -> prPrec i 0 (concatD [prtLocalIdent 0 localident ; render ":" ; prtTypeT 0 type_]) + AbsBasilIR.LocalTyped (localident, type_) -> prPrec i 0 (concatD [prtLocalIdent 0 localident ; render ":" ; prtTypeT 1 type_]) | AbsBasilIR.LocalUntyped localident -> prPrec i 0 (concatD [prtLocalIdent 0 localident]) and prtLocalVarListBNFC i es : doc = match (i, es) with @@ -251,7 +245,7 @@ and prtLocalVarListBNFC i es : doc = match (i, es) with | (_,[x]) -> (concatD [prtLocalVar 0 x]) | (_,x::xs) -> (concatD [prtLocalVar 0 x ; render "," ; prtLocalVarListBNFC 0 xs]) and prtGlobalVar (i:int) (e : AbsBasilIR.globalVar) : doc = match e with - AbsBasilIR.GlobalTyped (globalident, type_) -> prPrec i 0 (concatD [prtGlobalIdent 0 globalident ; render ":" ; prtTypeT 0 type_]) + AbsBasilIR.GlobalTyped (globalident, type_) -> prPrec i 0 (concatD [prtGlobalIdent 0 globalident ; render ":" ; prtTypeT 1 type_]) | AbsBasilIR.GlobalUntyped globalident -> prPrec i 0 (concatD [prtGlobalIdent 0 globalident]) and prtGlobalVarListBNFC i es : doc = match (i, es) with @@ -263,6 +257,19 @@ and prtVar (i:int) (e : AbsBasilIR.var) : doc = match e with | AbsBasilIR.VarGlobalVar globalvar -> prPrec i 0 (concatD [prtGlobalVar 0 globalvar]) +and prtLocalVarParen (i:int) (e : AbsBasilIR.localVarParen) : doc = match e with + AbsBasilIR.LocalVarParenLocalVar localvar -> prPrec i 0 (concatD [prtLocalVar 0 localvar]) + | AbsBasilIR.LocalVarParen1 (openparen, localident, type_, closeparen) -> prPrec i 0 (concatD [prtOpenParen 0 openparen ; prtLocalIdent 0 localident ; render ":" ; prtTypeT 0 type_ ; prtCloseParen 0 closeparen]) + +and prtLocalVarParenListBNFC i es : doc = match (i, es) with + (_,[]) -> (concatD []) + | (_,[x]) -> (concatD [prtLocalVarParen 0 x]) + | (_,x::xs) -> (concatD [prtLocalVarParen 0 x ; render "," ; prtLocalVarParenListBNFC 0 xs]) +and prtGlobalVarParen (i:int) (e : AbsBasilIR.globalVarParen) : doc = match e with + AbsBasilIR.GlobalVarParenGlobalVar globalvar -> prPrec i 0 (concatD [prtGlobalVar 0 globalvar]) + | AbsBasilIR.GlobalVarParen1 (openparen, globalident, type_, closeparen) -> prPrec i 0 (concatD [prtOpenParen 0 openparen ; prtGlobalIdent 0 globalident ; render ":" ; prtTypeT 0 type_ ; prtCloseParen 0 closeparen]) + + and prtNamedCallReturn (i:int) (e : AbsBasilIR.namedCallReturn) : doc = match e with AbsBasilIR.NamedCallReturn1 (lvar, localident) -> prPrec i 0 (concatD [prtLVar 0 lvar ; render "=" ; prtLocalIdent 0 localident]) @@ -330,7 +337,7 @@ and prtPhiAssignListBNFC i es : doc = match (i, es) with | (_,x::xs) -> (concatD [prtPhiAssign 0 x ; render "," ; prtPhiAssignListBNFC 0 xs]) and prtBlock (i:int) (e : AbsBasilIR.block) : doc = match e with AbsBasilIR.Block_NoPhi (blockident, attribset, beginlist, stmtwithattribs, jumpwithattrib, endlist) -> prPrec i 0 (concatD [render "block" ; prtBlockIdent 0 blockident ; prtAttribSet 0 attribset ; prtBeginList 0 beginlist ; prtStmtWithAttribListBNFC 0 stmtwithattribs ; prtJumpWithAttrib 0 jumpwithattrib ; render ";" ; prtEndList 0 endlist]) - | AbsBasilIR.Block_Phi (blockident, attribset, beginlist, openparen, phiassigns, closeparen, stmtwithattribs, jumpwithattrib, endlist) -> prPrec i 0 (concatD [render "block" ; prtBlockIdent 0 blockident ; prtAttribSet 0 attribset ; prtBeginList 0 beginlist ; prtOpenParen 0 openparen ; prtPhiAssignListBNFC 0 phiassigns ; prtCloseParen 0 closeparen ; render ";" ; prtStmtWithAttribListBNFC 0 stmtwithattribs ; prtJumpWithAttrib 0 jumpwithattrib ; render ";" ; prtEndList 0 endlist]) + | AbsBasilIR.Block_Phi (blockident, attribset, openparen, phiassigns, closeparen, beginlist, stmtwithattribs, jumpwithattrib, endlist) -> prPrec i 0 (concatD [render "block" ; prtBlockIdent 0 blockident ; prtAttribSet 0 attribset ; prtOpenParen 0 openparen ; prtPhiAssignListBNFC 0 phiassigns ; prtCloseParen 0 closeparen ; prtBeginList 0 beginlist ; prtStmtWithAttribListBNFC 0 stmtwithattribs ; prtJumpWithAttrib 0 jumpwithattrib ; render ";" ; prtEndList 0 endlist]) and prtBlockListBNFC i es : doc = match (i, es) with (_,[]) -> (concatD []) @@ -344,14 +351,13 @@ and prtAttrKeyValueListBNFC i es : doc = match (i, es) with | (_,[x]) -> (concatD [prtAttrKeyValue 0 x]) | (_,x::xs) -> (concatD [prtAttrKeyValue 0 x ; render ";" ; prtAttrKeyValueListBNFC 0 xs]) and prtAttribSet (i:int) (e : AbsBasilIR.attribSet) : doc = match e with - AbsBasilIR.AttribSet_Some (beginrec, attrkeyvalues, semicolons, endrec) -> prPrec i 0 (concatD [prtBeginRec 0 beginrec ; prtAttrKeyValueListBNFC 0 attrkeyvalues ; prtSemicolons 0 semicolons ; prtEndRec 0 endrec]) + AbsBasilIR.AttribSet_Some (beginrec, attrkeyvalues, endrec) -> prPrec i 0 (concatD [prtBeginRec 0 beginrec ; prtAttrKeyValueListBNFC 0 attrkeyvalues ; prtEndRec 0 endrec]) | AbsBasilIR.AttribSet_Empty -> prPrec i 0 (concatD []) and prtAttr (i:int) (e : AbsBasilIR.attr) : doc = match e with - AbsBasilIR.Attr_Map (beginrec, attrkeyvalues, semicolons, endrec) -> prPrec i 0 (concatD [prtBeginRec 0 beginrec ; prtAttrKeyValueListBNFC 0 attrkeyvalues ; prtSemicolons 0 semicolons ; prtEndRec 0 endrec]) + AbsBasilIR.Attr_Map (beginrec, attrkeyvalues, endrec) -> prPrec i 0 (concatD [prtBeginRec 0 beginrec ; prtAttrKeyValueListBNFC 0 attrkeyvalues ; prtEndRec 0 endrec]) | AbsBasilIR.Attr_List (beginlist, attrs, endlist) -> prPrec i 0 (concatD [prtBeginList 0 beginlist ; prtAttrListBNFC 0 attrs ; prtEndList 0 endlist]) - | AbsBasilIR.Attr_Lit value -> prPrec i 0 (concatD [prtValue 0 value]) | AbsBasilIR.Attr_Expr expr -> prPrec i 0 (concatD [prtExpr 0 expr]) | AbsBasilIR.Attr_Str str -> prPrec i 0 (concatD [prtStr 0 str]) @@ -366,13 +372,6 @@ and prtParamsListBNFC i es : doc = match (i, es) with (_,[]) -> (concatD []) | (_,[x]) -> (concatD [prtParams 0 x]) | (_,x::xs) -> (concatD [prtParams 0 x ; render "," ; prtParamsListBNFC 0 xs]) -and prtFunParams (i:int) (e : AbsBasilIR.funParams) : doc = match e with - AbsBasilIR.FunParams1 (localident, type_) -> prPrec i 0 (concatD [prtLocalIdent 0 localident ; render ":" ; prtTypeT 0 type_]) - | AbsBasilIR.FunParams2 (openparen, localident, type_, closeparen) -> prPrec i 0 (concatD [prtOpenParen 0 openparen ; prtLocalIdent 0 localident ; render ":" ; prtTypeT 0 type_ ; prtCloseParen 0 closeparen]) - -and prtFunParamsListBNFC i es : doc = match (i, es) with - (_,[]) -> (concatD []) - | (_,x::xs) -> (concatD [prtFunParams 0 x ; render " " ; prtFunParamsListBNFC 0 xs]) and prtValue (i:int) (e : AbsBasilIR.value) : doc = match e with AbsBasilIR.Value_BV bvval -> prPrec i 0 (concatD [prtBVVal 0 bvval]) | AbsBasilIR.Value_Int intval -> prPrec i 0 (concatD [prtIntVal 0 intval]) @@ -381,48 +380,38 @@ and prtValue (i:int) (e : AbsBasilIR.value) : doc = match e with and prtExpr (i:int) (e : AbsBasilIR.expr) : doc = match e with - AbsBasilIR.Expr_Literal value -> prPrec i 0 (concatD [prtValue 0 value]) - | AbsBasilIR.Expr_Paren (openparen, expr, closeparen) -> prPrec i 0 (concatD [prtOpenParen 0 openparen ; prtExpr 0 expr ; prtCloseParen 0 closeparen]) - | AbsBasilIR.Expr_Local localvar -> prPrec i 0 (concatD [prtLocalVar 0 localvar]) - | AbsBasilIR.Expr_Global globalvar -> prPrec i 0 (concatD [prtGlobalVar 0 globalvar]) + AbsBasilIR.Expr_Literal value -> prPrec i 2 (concatD [prtValue 0 value]) + | AbsBasilIR.Expr_Local localvar -> prPrec i 2 (concatD [prtLocalVar 0 localvar]) + | AbsBasilIR.Expr_Global globalvar -> prPrec i 2 (concatD [prtGlobalVar 0 globalvar]) | AbsBasilIR.Expr_Forall (attribset, lambdadef) -> prPrec i 0 (concatD [render "forall" ; prtAttribSet 0 attribset ; prtLambdaDef 0 lambdadef]) | AbsBasilIR.Expr_Exists (attribset, lambdadef) -> prPrec i 0 (concatD [render "exists" ; prtAttribSet 0 attribset ; prtLambdaDef 0 lambdadef]) | AbsBasilIR.Expr_Lambda (attribset, lambdadef) -> prPrec i 0 (concatD [render "fun" ; prtAttribSet 0 attribset ; prtLambdaDef 0 lambdadef]) - | AbsBasilIR.Expr_Old (openparen, expr, closeparen) -> prPrec i 0 (concatD [render "old" ; prtOpenParen 0 openparen ; prtExpr 0 expr ; prtCloseParen 0 closeparen]) - | AbsBasilIR.Expr_FunctionOp (globalident, openparen, exprs, closeparen) -> prPrec i 0 (concatD [prtGlobalIdent 0 globalident ; prtOpenParen 0 openparen ; prtExprListBNFC 0 exprs ; prtCloseParen 0 closeparen]) - | AbsBasilIR.Expr_Apply (expr1, expr2) -> prPrec i 0 (concatD [prtExpr 0 expr1 ; prtExpr 0 expr2]) - | AbsBasilIR.Expr_Binary (binop, openparen, expr1, expr2, closeparen) -> prPrec i 0 (concatD [prtBinOp 0 binop ; prtOpenParen 0 openparen ; prtExpr 0 expr1 ; render "," ; prtExpr 0 expr2 ; prtCloseParen 0 closeparen]) - | AbsBasilIR.Expr_Assoc (boolbinop, openparen, exprs, closeparen) -> prPrec i 0 (concatD [prtBoolBinOp 0 boolbinop ; prtOpenParen 0 openparen ; prtExprListBNFC 0 exprs ; prtCloseParen 0 closeparen]) - | AbsBasilIR.Expr_Unary (unop, openparen, expr, closeparen) -> prPrec i 0 (concatD [prtUnOp 0 unop ; prtOpenParen 0 openparen ; prtExpr 0 expr ; prtCloseParen 0 closeparen]) - | AbsBasilIR.Expr_LoadBe (openparen, intval, expr1, expr2, closeparen) -> prPrec i 0 (concatD [render "load_be" ; prtOpenParen 0 openparen ; prtIntVal 0 intval ; render "," ; prtExpr 0 expr1 ; render "," ; prtExpr 0 expr2 ; prtCloseParen 0 closeparen]) - | AbsBasilIR.Expr_LoadLe (openparen, intval, expr1, expr2, closeparen) -> prPrec i 0 (concatD [render "load_le" ; prtOpenParen 0 openparen ; prtIntVal 0 intval ; render "," ; prtExpr 0 expr1 ; render "," ; prtExpr 0 expr2 ; prtCloseParen 0 closeparen]) - | AbsBasilIR.Expr_ZeroExtend (openparen, intval, expr, closeparen) -> prPrec i 0 (concatD [render "zero_extend" ; prtOpenParen 0 openparen ; prtIntVal 0 intval ; render "," ; prtExpr 0 expr ; prtCloseParen 0 closeparen]) - | AbsBasilIR.Expr_SignExtend (openparen, intval, expr, closeparen) -> prPrec i 0 (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 0 (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 0 (concatD [render "bvconcat" ; prtOpenParen 0 openparen ; prtExprListBNFC 0 exprs ; prtCloseParen 0 closeparen]) - | AbsBasilIR.Expr_Match (expr, openparen, cases, closeparen) -> prPrec i 0 (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 0 (concatD [render "cases" ; prtOpenParen 0 openparen ; prtCaseListBNFC 0 cases ; prtCloseParen 0 closeparen]) + | AbsBasilIR.Expr_Old (openparen, expr, closeparen) -> prPrec i 2 (concatD [render "old" ; prtOpenParen 0 openparen ; prtExpr 0 expr ; prtCloseParen 0 closeparen]) + | AbsBasilIR.Expr_FunctionOp (expr, openparen, exprs, closeparen) -> prPrec i 1 (concatD [prtExpr 1 expr ; prtOpenParen 0 openparen ; prtExprListBNFC 0 exprs ; prtCloseParen 0 closeparen]) + | AbsBasilIR.Expr_Binary (binop, openparen, expr1, expr2, closeparen) -> prPrec i 2 (concatD [prtBinOp 0 binop ; prtOpenParen 0 openparen ; prtExpr 0 expr1 ; render "," ; prtExpr 0 expr2 ; prtCloseParen 0 closeparen]) + | AbsBasilIR.Expr_Assoc (boolbinop, openparen, exprs, closeparen) -> prPrec i 2 (concatD [prtBoolBinOp 0 boolbinop ; prtOpenParen 0 openparen ; prtExprListBNFC 0 exprs ; prtCloseParen 0 closeparen]) + | AbsBasilIR.Expr_Unary (unop, openparen, expr, closeparen) -> prPrec i 2 (concatD [prtUnOp 0 unop ; prtOpenParen 0 openparen ; prtExpr 0 expr ; prtCloseParen 0 closeparen]) + | AbsBasilIR.Expr_LoadBe (openparen, intval, expr1, expr2, closeparen) -> prPrec i 2 (concatD [render "load_be" ; prtOpenParen 0 openparen ; prtIntVal 0 intval ; render "," ; prtExpr 0 expr1 ; render "," ; prtExpr 0 expr2 ; prtCloseParen 0 closeparen]) + | AbsBasilIR.Expr_LoadLe (openparen, intval, expr1, expr2, closeparen) -> prPrec i 2 (concatD [render "load_le" ; prtOpenParen 0 openparen ; prtIntVal 0 intval ; render "," ; prtExpr 0 expr1 ; render "," ; prtExpr 0 expr2 ; prtCloseParen 0 closeparen]) + | AbsBasilIR.Expr_ZeroExtend (openparen, intval, expr, closeparen) -> prPrec i 2 (concatD [render "zero_extend" ; prtOpenParen 0 openparen ; prtIntVal 0 intval ; render "," ; prtExpr 0 expr ; prtCloseParen 0 closeparen]) + | 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_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]) and prtExprListBNFC i es : doc = match (i, es) with (_,[]) -> (concatD []) | (_,[x]) -> (concatD [prtExpr 0 x]) | (_,x::xs) -> (concatD [prtExpr 0 x ; render "," ; prtExprListBNFC 0 xs]) -and prtLParen (i:int) (e : AbsBasilIR.lParen) : doc = match e with - AbsBasilIR.LParenLocalVar localvar -> prPrec i 0 (concatD [prtLocalVar 0 localvar]) - | AbsBasilIR.LParen1 (openparen, localvar, closeparen) -> prPrec i 0 (concatD [prtOpenParen 0 openparen ; prtLocalVar 0 localvar ; prtCloseParen 0 closeparen]) - -and prtLParenListBNFC i es : doc = match (i, es) with - (_,[]) -> (concatD []) - | (_,[x]) -> (concatD [prtLParen 0 x]) - | (_,x::xs) -> (concatD [prtLParen 0 x ; render "," ; prtLParenListBNFC 0 xs]) and prtLambdaDef (i:int) (e : AbsBasilIR.lambdaDef) : doc = match e with - AbsBasilIR.LambdaDef1 (lparens, lambdasep, expr) -> prPrec i 0 (concatD [prtLParenListBNFC 0 lparens ; prtLambdaSep 0 lambdasep ; prtExpr 0 expr]) + AbsBasilIR.LambdaDef1 (localvarparens, lambdasep, expr) -> prPrec i 0 (concatD [prtLocalVarParenListBNFC 0 localvarparens ; prtLambdaSep 0 lambdasep ; prtExpr 0 expr]) and prtBinOp (i:int) (e : AbsBasilIR.binOp) : doc = match e with AbsBasilIR.BinOpBVBinOp bvbinop -> prPrec i 0 (concatD [prtBVBinOp 0 bvbinop]) | AbsBasilIR.BinOpBVLogicalBinOp bvlogicalbinop -> prPrec i 0 (concatD [prtBVLogicalBinOp 0 bvlogicalbinop]) - | AbsBasilIR.BinOpBoolBinOp boolbinop -> prPrec i 0 (concatD [prtBoolBinOp 0 boolbinop]) | AbsBasilIR.BinOpIntLogicalBinOp intlogicalbinop -> prPrec i 0 (concatD [prtIntLogicalBinOp 0 intlogicalbinop]) | AbsBasilIR.BinOpIntBinOp intbinop -> prPrec i 0 (concatD [prtIntBinOp 0 intbinop]) | AbsBasilIR.BinOpEqOp eqop -> prPrec i 0 (concatD [prtEqOp 0 eqop]) @@ -524,7 +513,7 @@ and prtRelyTok (i:int) (e : AbsBasilIR.relyTok) : doc = match e with and prtGuarTok (i:int) (e : AbsBasilIR.guarTok) : doc = match e with - AbsBasilIR.GuarTok_guarnatee -> prPrec i 0 (concatD [render "guarnatee"]) + AbsBasilIR.GuarTok_guarantee -> prPrec i 0 (concatD [render "guarantee"]) | AbsBasilIR.GuarTok_guarantees -> prPrec i 0 (concatD [render "guarantees"]) @@ -539,18 +528,21 @@ and prtFunSpec (i:int) (e : AbsBasilIR.funSpec) : doc = match e with and prtFunSpecListBNFC i es : doc = match (i, es) with (_,[]) -> (concatD []) - | (_,x::xs) -> (concatD [prtFunSpec 0 x ; render ";" ; prtFunSpecListBNFC 0 xs]) + | (_,x::xs) -> (concatD [prtFunSpec 0 x ; render " +" ; prtFunSpecListBNFC 0 xs]) and prtVarSpec (i:int) (e : AbsBasilIR.varSpec) : doc = match e with AbsBasilIR.VarSpec_Classification expr -> prPrec i 0 (concatD [render "classification" ; prtExpr 0 expr]) | AbsBasilIR.VarSpec_Empty -> prPrec i 0 (concatD []) and prtProgSpec (i:int) (e : AbsBasilIR.progSpec) : doc = match e with - AbsBasilIR.ProgSpec_Rely expr -> prPrec i 0 (concatD [render "rely" ; prtExpr 0 expr]) - | AbsBasilIR.ProgSpec_Guarantee expr -> prPrec i 0 (concatD [render "guarantee" ; prtExpr 0 expr]) + AbsBasilIR.ProgSpec_Rely (relytok, expr) -> prPrec i 0 (concatD [prtRelyTok 0 relytok ; prtExpr 0 expr]) + | AbsBasilIR.ProgSpec_Guarantee (guartok, expr) -> prPrec i 0 (concatD [prtGuarTok 0 guartok ; prtExpr 0 expr]) and prtProgSpecListBNFC i es : doc = match (i, es) with (_,[]) -> (concatD []) - | (_,[x]) -> (concatD [prtProgSpec 0 x]) - | (_,x::xs) -> (concatD [prtProgSpec 0 x ; render ";" ; prtProgSpecListBNFC 0 xs]) + | (_,[x]) -> (concatD [prtProgSpec 0 x ; render " +"]) + | (_,x::xs) -> (concatD [prtProgSpec 0 x ; render " +" ; prtProgSpecListBNFC 0 xs]) diff --git a/lib/fe/ShowBasilIR.ml b/lib/fe/ShowBasilIR.ml index 4e8e4d74..263d6c83 100644 --- a/lib/fe/ShowBasilIR.ml +++ b/lib/fe/ShowBasilIR.ml @@ -1,4 +1,4 @@ -(* File generated by the BNF Converter (bnfc 2.9.6.1). *) +(* File generated by the BNF Converter (bnfc 2.9.6.2). *) (* show functions *) @@ -65,11 +65,6 @@ and showLambdaSep (e : AbsBasilIR.lambdaSep) : showable = match e with | AbsBasilIR.LambdaSep2 -> s2s "LambdaSep2" -and showSemicolons (e : AbsBasilIR.semicolons) : showable = match e with - AbsBasilIR.Semicolons_Empty -> s2s "Semicolons_Empty" - | AbsBasilIR.Semicolons_Some semicolons -> s2s "Semicolons_Some" >> c2s ' ' >> c2s '(' >> showSemicolons semicolons >> c2s ')' - - and showVarModifiers (e : AbsBasilIR.varModifiers) : showable = match e with AbsBasilIR.Shared -> s2s "Shared" | AbsBasilIR.Observable -> s2s "Observable" @@ -100,20 +95,20 @@ and showBoolType (e : AbsBasilIR.boolType) : showable = match e with AbsBasilIR.BoolType1 booltype -> s2s "BoolType1" >> c2s ' ' >> c2s '(' >> showBOOLTYPE booltype >> c2s ')' -and showMapType (e : AbsBasilIR.mapType) : showable = match e with - AbsBasilIR.MapType1 (type'0, type') -> s2s "MapType1" >> c2s ' ' >> c2s '(' >> showTypeT type'0 >> s2s ", " >> showTypeT type' >> c2s ')' - - and showBVType (e : AbsBasilIR.bVType) : showable = match e with AbsBasilIR.BVType1 bvtype -> s2s "BVType1" >> c2s ' ' >> c2s '(' >> showBVTYPE bvtype >> c2s ')' +and showMapType (e : AbsBasilIR.mapType) : showable = match e with + AbsBasilIR.MapType1 (type'0, type') -> s2s "MapType1" >> c2s ' ' >> c2s '(' >> showTypeT type'0 >> s2s ", " >> showTypeT type' >> c2s ')' + + and showTypeT (e : AbsBasilIR.typeT) : showable = match e with AbsBasilIR.TypeIntType inttype -> s2s "TypeIntType" >> c2s ' ' >> c2s '(' >> showIntType inttype >> c2s ')' | AbsBasilIR.TypeBoolType booltype -> s2s "TypeBoolType" >> c2s ' ' >> c2s '(' >> showBoolType booltype >> c2s ')' - | AbsBasilIR.TypeMapType maptype -> s2s "TypeMapType" >> c2s ' ' >> c2s '(' >> showMapType maptype >> c2s ')' | AbsBasilIR.TypeBVType bvtype -> s2s "TypeBVType" >> c2s ' ' >> c2s '(' >> showBVType bvtype >> c2s ')' - | AbsBasilIR.Type1 (openparen, type', closeparen) -> s2s "Type1" >> c2s ' ' >> c2s '(' >> showOpenParen openparen >> s2s ", " >> showTypeT type' >> s2s ", " >> showCloseParen closeparen >> c2s ')' + | AbsBasilIR.TypeParen (openparen, type', closeparen) -> s2s "TypeParen" >> c2s ' ' >> c2s '(' >> showOpenParen openparen >> s2s ", " >> showTypeT type' >> s2s ", " >> showCloseParen closeparen >> c2s ')' + | AbsBasilIR.TypeMapType maptype -> s2s "TypeMapType" >> c2s ' ' >> c2s '(' >> showMapType maptype >> c2s ')' and showIntVal (e : AbsBasilIR.intVal) : showable = match e with @@ -141,10 +136,9 @@ and showStmt (e : AbsBasilIR.stmt) : showable = match e with | AbsBasilIR.Stmt_ScalarStore (lvar, expr) -> s2s "Stmt_ScalarStore" >> c2s ' ' >> c2s '(' >> showLVar lvar >> s2s ", " >> showExpr expr >> c2s ')' | AbsBasilIR.Stmt_ScalarLoad (lvar, var) -> s2s "Stmt_ScalarLoad" >> c2s ' ' >> c2s '(' >> showLVar lvar >> s2s ", " >> showVar var >> c2s ')' | AbsBasilIR.Stmt_MultiAssign (openparen, assignments, closeparen) -> s2s "Stmt_MultiAssign" >> c2s ' ' >> c2s '(' >> showOpenParen openparen >> s2s ", " >> showList showAssignment assignments >> s2s ", " >> showCloseParen closeparen >> c2s ')' - | AbsBasilIR.Stmt_Load (lvar, endian, globalident, expr, intval) -> s2s "Stmt_Load" >> c2s ' ' >> c2s '(' >> showLVar lvar >> s2s ", " >> showEndian endian >> s2s ", " >> showGlobalIdent globalident >> s2s ", " >> showExpr expr >> s2s ", " >> showIntVal intval >> c2s ')' - | AbsBasilIR.Stmt_Store (endian, globalident, expr0, expr, intval) -> s2s "Stmt_Store" >> c2s ' ' >> c2s '(' >> showEndian endian >> s2s ", " >> showGlobalIdent globalident >> s2s ", " >> showExpr expr0 >> s2s ", " >> showExpr expr >> s2s ", " >> showIntVal intval >> c2s ')' | AbsBasilIR.Stmt_Load_Var (lvar, endian, var, expr, intval) -> s2s "Stmt_Load_Var" >> c2s ' ' >> c2s '(' >> showLVar lvar >> s2s ", " >> showEndian endian >> s2s ", " >> showVar var >> s2s ", " >> showExpr expr >> s2s ", " >> showIntVal intval >> c2s ')' | AbsBasilIR.Stmt_Store_Var (lvar, endian, var, expr0, expr, intval) -> s2s "Stmt_Store_Var" >> c2s ' ' >> c2s '(' >> showLVar lvar >> s2s ", " >> showEndian endian >> s2s ", " >> showVar var >> s2s ", " >> showExpr expr0 >> s2s ", " >> showExpr expr >> s2s ", " >> showIntVal intval >> c2s ')' + | AbsBasilIR.Stmt_Store (endian, globalident, expr0, expr, intval) -> s2s "Stmt_Store" >> c2s ' ' >> c2s '(' >> showEndian endian >> s2s ", " >> showGlobalIdent globalident >> s2s ", " >> showExpr expr0 >> s2s ", " >> showExpr expr >> s2s ", " >> showIntVal intval >> c2s ')' | AbsBasilIR.Stmt_DirectCall (lvars, procident, openparen, callparams, closeparen) -> s2s "Stmt_DirectCall" >> c2s ' ' >> c2s '(' >> showLVars lvars >> s2s ", " >> showProcIdent procident >> s2s ", " >> showOpenParen openparen >> s2s ", " >> showCallParams callparams >> s2s ", " >> showCloseParen closeparen >> c2s ')' | AbsBasilIR.Stmt_IndirectCall expr -> s2s "Stmt_IndirectCall" >> c2s ' ' >> c2s '(' >> showExpr expr >> c2s ')' | AbsBasilIR.Stmt_Assume expr -> s2s "Stmt_Assume" >> c2s ' ' >> c2s '(' >> showExpr expr >> c2s ')' @@ -167,6 +161,16 @@ and showVar (e : AbsBasilIR.var) : showable = match e with | AbsBasilIR.VarGlobalVar globalvar -> s2s "VarGlobalVar" >> c2s ' ' >> c2s '(' >> showGlobalVar globalvar >> c2s ')' +and showLocalVarParen (e : AbsBasilIR.localVarParen) : showable = match e with + AbsBasilIR.LocalVarParenLocalVar localvar -> s2s "LocalVarParenLocalVar" >> c2s ' ' >> c2s '(' >> showLocalVar localvar >> c2s ')' + | AbsBasilIR.LocalVarParen1 (openparen, localident, type', closeparen) -> s2s "LocalVarParen1" >> c2s ' ' >> c2s '(' >> showOpenParen openparen >> s2s ", " >> showLocalIdent localident >> s2s ", " >> showTypeT type' >> s2s ", " >> showCloseParen closeparen >> c2s ')' + + +and showGlobalVarParen (e : AbsBasilIR.globalVarParen) : showable = match e with + AbsBasilIR.GlobalVarParenGlobalVar globalvar -> s2s "GlobalVarParenGlobalVar" >> c2s ' ' >> c2s '(' >> showGlobalVar globalvar >> c2s ')' + | AbsBasilIR.GlobalVarParen1 (openparen, globalident, type', closeparen) -> s2s "GlobalVarParen1" >> c2s ' ' >> c2s '(' >> showOpenParen openparen >> s2s ", " >> showGlobalIdent globalident >> s2s ", " >> showTypeT type' >> s2s ", " >> showCloseParen closeparen >> c2s ')' + + and showNamedCallReturn (e : AbsBasilIR.namedCallReturn) : showable = match e with AbsBasilIR.NamedCallReturn1 (lvar, localident) -> s2s "NamedCallReturn1" >> c2s ' ' >> c2s '(' >> showLVar lvar >> s2s ", " >> showLocalIdent localident >> c2s ')' @@ -217,7 +221,7 @@ and showPhiAssign (e : AbsBasilIR.phiAssign) : showable = match e with and showBlock (e : AbsBasilIR.block) : showable = match e with AbsBasilIR.Block_NoPhi (blockident, attribset, beginlist, stmtwithattribs, jumpwithattrib, endlist) -> s2s "Block_NoPhi" >> c2s ' ' >> c2s '(' >> showBlockIdent blockident >> s2s ", " >> showAttribSet attribset >> s2s ", " >> showBeginList beginlist >> s2s ", " >> showList showStmtWithAttrib stmtwithattribs >> s2s ", " >> showJumpWithAttrib jumpwithattrib >> s2s ", " >> showEndList endlist >> c2s ')' - | AbsBasilIR.Block_Phi (blockident, attribset, beginlist, openparen, phiassigns, closeparen, stmtwithattribs, jumpwithattrib, endlist) -> s2s "Block_Phi" >> c2s ' ' >> c2s '(' >> showBlockIdent blockident >> s2s ", " >> showAttribSet attribset >> s2s ", " >> showBeginList beginlist >> s2s ", " >> showOpenParen openparen >> s2s ", " >> showList showPhiAssign phiassigns >> s2s ", " >> showCloseParen closeparen >> s2s ", " >> showList showStmtWithAttrib stmtwithattribs >> s2s ", " >> showJumpWithAttrib jumpwithattrib >> s2s ", " >> showEndList endlist >> c2s ')' + | AbsBasilIR.Block_Phi (blockident, attribset, openparen, phiassigns, closeparen, beginlist, stmtwithattribs, jumpwithattrib, endlist) -> s2s "Block_Phi" >> c2s ' ' >> c2s '(' >> showBlockIdent blockident >> s2s ", " >> showAttribSet attribset >> s2s ", " >> showOpenParen openparen >> s2s ", " >> showList showPhiAssign phiassigns >> s2s ", " >> showCloseParen closeparen >> s2s ", " >> showBeginList beginlist >> s2s ", " >> showList showStmtWithAttrib stmtwithattribs >> s2s ", " >> showJumpWithAttrib jumpwithattrib >> s2s ", " >> showEndList endlist >> c2s ')' and showAttrKeyValue (e : AbsBasilIR.attrKeyValue) : showable = match e with @@ -225,14 +229,13 @@ and showAttrKeyValue (e : AbsBasilIR.attrKeyValue) : showable = match e with and showAttribSet (e : AbsBasilIR.attribSet) : showable = match e with - AbsBasilIR.AttribSet_Some (beginrec, attrkeyvalues, semicolons, endrec) -> s2s "AttribSet_Some" >> c2s ' ' >> c2s '(' >> showBeginRec beginrec >> s2s ", " >> showList showAttrKeyValue attrkeyvalues >> s2s ", " >> showSemicolons semicolons >> s2s ", " >> showEndRec endrec >> c2s ')' + AbsBasilIR.AttribSet_Some (beginrec, attrkeyvalues, endrec) -> s2s "AttribSet_Some" >> c2s ' ' >> c2s '(' >> showBeginRec beginrec >> s2s ", " >> showList showAttrKeyValue attrkeyvalues >> s2s ", " >> showEndRec endrec >> c2s ')' | AbsBasilIR.AttribSet_Empty -> s2s "AttribSet_Empty" and showAttr (e : AbsBasilIR.attr) : showable = match e with - AbsBasilIR.Attr_Map (beginrec, attrkeyvalues, semicolons, endrec) -> s2s "Attr_Map" >> c2s ' ' >> c2s '(' >> showBeginRec beginrec >> s2s ", " >> showList showAttrKeyValue attrkeyvalues >> s2s ", " >> showSemicolons semicolons >> s2s ", " >> showEndRec endrec >> c2s ')' + AbsBasilIR.Attr_Map (beginrec, attrkeyvalues, endrec) -> s2s "Attr_Map" >> c2s ' ' >> c2s '(' >> showBeginRec beginrec >> s2s ", " >> showList showAttrKeyValue attrkeyvalues >> s2s ", " >> showEndRec endrec >> c2s ')' | AbsBasilIR.Attr_List (beginlist, attrs, endlist) -> s2s "Attr_List" >> c2s ' ' >> c2s '(' >> showBeginList beginlist >> s2s ", " >> showList showAttr attrs >> s2s ", " >> showEndList endlist >> c2s ')' - | AbsBasilIR.Attr_Lit value -> s2s "Attr_Lit" >> c2s ' ' >> c2s '(' >> showValue value >> c2s ')' | AbsBasilIR.Attr_Expr expr -> s2s "Attr_Expr" >> c2s ' ' >> c2s '(' >> showExpr expr >> c2s ')' | AbsBasilIR.Attr_Str str -> s2s "Attr_Str" >> c2s ' ' >> c2s '(' >> showStr str >> c2s ')' @@ -241,11 +244,6 @@ and showParams (e : AbsBasilIR.params) : showable = match e with AbsBasilIR.Params1 (localident, type') -> s2s "Params1" >> c2s ' ' >> c2s '(' >> showLocalIdent localident >> s2s ", " >> showTypeT type' >> c2s ')' -and showFunParams (e : AbsBasilIR.funParams) : showable = match e with - AbsBasilIR.FunParams1 (localident, type') -> s2s "FunParams1" >> c2s ' ' >> c2s '(' >> showLocalIdent localident >> s2s ", " >> showTypeT type' >> c2s ')' - | AbsBasilIR.FunParams2 (openparen, localident, type', closeparen) -> s2s "FunParams2" >> c2s ' ' >> c2s '(' >> showOpenParen openparen >> s2s ", " >> showLocalIdent localident >> s2s ", " >> showTypeT type' >> s2s ", " >> showCloseParen closeparen >> c2s ')' - - and showValue (e : AbsBasilIR.value) : showable = match e with AbsBasilIR.Value_BV bvval -> s2s "Value_BV" >> c2s ' ' >> c2s '(' >> showBVVal bvval >> c2s ')' | AbsBasilIR.Value_Int intval -> s2s "Value_Int" >> c2s ' ' >> c2s '(' >> showIntVal intval >> c2s ')' @@ -255,15 +253,13 @@ and showValue (e : AbsBasilIR.value) : showable = match e with and showExpr (e : AbsBasilIR.expr) : showable = match e with AbsBasilIR.Expr_Literal value -> s2s "Expr_Literal" >> c2s ' ' >> c2s '(' >> showValue value >> c2s ')' - | AbsBasilIR.Expr_Paren (openparen, expr, closeparen) -> s2s "Expr_Paren" >> c2s ' ' >> c2s '(' >> showOpenParen openparen >> s2s ", " >> showExpr expr >> s2s ", " >> showCloseParen closeparen >> c2s ')' | AbsBasilIR.Expr_Local localvar -> s2s "Expr_Local" >> c2s ' ' >> c2s '(' >> showLocalVar localvar >> c2s ')' | AbsBasilIR.Expr_Global globalvar -> s2s "Expr_Global" >> c2s ' ' >> c2s '(' >> showGlobalVar globalvar >> c2s ')' | AbsBasilIR.Expr_Forall (attribset, lambdadef) -> s2s "Expr_Forall" >> c2s ' ' >> c2s '(' >> showAttribSet attribset >> s2s ", " >> showLambdaDef lambdadef >> c2s ')' | AbsBasilIR.Expr_Exists (attribset, lambdadef) -> s2s "Expr_Exists" >> c2s ' ' >> c2s '(' >> showAttribSet attribset >> s2s ", " >> showLambdaDef lambdadef >> c2s ')' | AbsBasilIR.Expr_Lambda (attribset, lambdadef) -> s2s "Expr_Lambda" >> c2s ' ' >> c2s '(' >> showAttribSet attribset >> s2s ", " >> showLambdaDef lambdadef >> c2s ')' | AbsBasilIR.Expr_Old (openparen, expr, closeparen) -> s2s "Expr_Old" >> c2s ' ' >> c2s '(' >> showOpenParen openparen >> s2s ", " >> showExpr expr >> s2s ", " >> showCloseParen closeparen >> c2s ')' - | AbsBasilIR.Expr_FunctionOp (globalident, openparen, exprs, closeparen) -> s2s "Expr_FunctionOp" >> c2s ' ' >> c2s '(' >> showGlobalIdent globalident >> s2s ", " >> showOpenParen openparen >> s2s ", " >> showList showExpr exprs >> s2s ", " >> showCloseParen closeparen >> c2s ')' - | AbsBasilIR.Expr_Apply (expr0, expr) -> s2s "Expr_Apply" >> c2s ' ' >> c2s '(' >> showExpr expr0 >> s2s ", " >> showExpr expr >> c2s ')' + | AbsBasilIR.Expr_FunctionOp (expr, openparen, exprs, closeparen) -> s2s "Expr_FunctionOp" >> c2s ' ' >> c2s '(' >> showExpr expr >> s2s ", " >> showOpenParen openparen >> s2s ", " >> showList showExpr exprs >> s2s ", " >> showCloseParen closeparen >> c2s ')' | AbsBasilIR.Expr_Binary (binop, openparen, expr0, expr, closeparen) -> s2s "Expr_Binary" >> c2s ' ' >> c2s '(' >> showBinOp binop >> s2s ", " >> showOpenParen openparen >> s2s ", " >> showExpr expr0 >> s2s ", " >> showExpr expr >> s2s ", " >> showCloseParen closeparen >> c2s ')' | AbsBasilIR.Expr_Assoc (boolbinop, openparen, exprs, closeparen) -> s2s "Expr_Assoc" >> c2s ' ' >> c2s '(' >> showBoolBinOp boolbinop >> s2s ", " >> showOpenParen openparen >> s2s ", " >> showList showExpr exprs >> s2s ", " >> showCloseParen closeparen >> c2s ')' | AbsBasilIR.Expr_Unary (unop, openparen, expr, closeparen) -> s2s "Expr_Unary" >> c2s ' ' >> c2s '(' >> showUnOp unop >> s2s ", " >> showOpenParen openparen >> s2s ", " >> showExpr expr >> s2s ", " >> showCloseParen closeparen >> c2s ')' @@ -275,21 +271,16 @@ and showExpr (e : AbsBasilIR.expr) : showable = match e with | AbsBasilIR.Expr_Concat (openparen, exprs, closeparen) -> s2s "Expr_Concat" >> c2s ' ' >> c2s '(' >> showOpenParen openparen >> s2s ", " >> showList showExpr exprs >> s2s ", " >> showCloseParen closeparen >> 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 ')' - - -and showLParen (e : AbsBasilIR.lParen) : showable = match e with - AbsBasilIR.LParenLocalVar localvar -> s2s "LParenLocalVar" >> c2s ' ' >> c2s '(' >> showLocalVar localvar >> c2s ')' - | AbsBasilIR.LParen1 (openparen, localvar, closeparen) -> s2s "LParen1" >> c2s ' ' >> c2s '(' >> showOpenParen openparen >> s2s ", " >> showLocalVar localvar >> s2s ", " >> showCloseParen closeparen >> c2s ')' + | AbsBasilIR.Expr_Paren (openparen, expr, closeparen) -> s2s "Expr_Paren" >> c2s ' ' >> c2s '(' >> showOpenParen openparen >> s2s ", " >> showExpr expr >> s2s ", " >> showCloseParen closeparen >> c2s ')' and showLambdaDef (e : AbsBasilIR.lambdaDef) : showable = match e with - AbsBasilIR.LambdaDef1 (lparens, lambdasep, expr) -> s2s "LambdaDef1" >> c2s ' ' >> c2s '(' >> showList showLParen lparens >> s2s ", " >> showLambdaSep lambdasep >> s2s ", " >> showExpr expr >> c2s ')' + AbsBasilIR.LambdaDef1 (localvarparens, lambdasep, expr) -> s2s "LambdaDef1" >> c2s ' ' >> c2s '(' >> showList showLocalVarParen localvarparens >> s2s ", " >> showLambdaSep lambdasep >> s2s ", " >> showExpr expr >> c2s ')' and showBinOp (e : AbsBasilIR.binOp) : showable = match e with AbsBasilIR.BinOpBVBinOp bvbinop -> s2s "BinOpBVBinOp" >> c2s ' ' >> c2s '(' >> showBVBinOp bvbinop >> c2s ')' | AbsBasilIR.BinOpBVLogicalBinOp bvlogicalbinop -> s2s "BinOpBVLogicalBinOp" >> c2s ' ' >> c2s '(' >> showBVLogicalBinOp bvlogicalbinop >> c2s ')' - | AbsBasilIR.BinOpBoolBinOp boolbinop -> s2s "BinOpBoolBinOp" >> c2s ' ' >> c2s '(' >> showBoolBinOp boolbinop >> c2s ')' | AbsBasilIR.BinOpIntLogicalBinOp intlogicalbinop -> s2s "BinOpIntLogicalBinOp" >> c2s ' ' >> c2s '(' >> showIntLogicalBinOp intlogicalbinop >> c2s ')' | AbsBasilIR.BinOpIntBinOp intbinop -> s2s "BinOpIntBinOp" >> c2s ' ' >> c2s '(' >> showIntBinOp intbinop >> c2s ')' | AbsBasilIR.BinOpEqOp eqop -> s2s "BinOpEqOp" >> c2s ' ' >> c2s '(' >> showEqOp eqop >> c2s ')' @@ -388,7 +379,7 @@ and showRelyTok (e : AbsBasilIR.relyTok) : showable = match e with and showGuarTok (e : AbsBasilIR.guarTok) : showable = match e with - AbsBasilIR.GuarTok_guarnatee -> s2s "GuarTok_guarnatee" + AbsBasilIR.GuarTok_guarantee -> s2s "GuarTok_guarantee" | AbsBasilIR.GuarTok_guarantees -> s2s "GuarTok_guarantees" @@ -408,8 +399,8 @@ and showVarSpec (e : AbsBasilIR.varSpec) : showable = match e with and showProgSpec (e : AbsBasilIR.progSpec) : showable = match e with - AbsBasilIR.ProgSpec_Rely expr -> s2s "ProgSpec_Rely" >> c2s ' ' >> c2s '(' >> showExpr expr >> c2s ')' - | AbsBasilIR.ProgSpec_Guarantee expr -> s2s "ProgSpec_Guarantee" >> c2s ' ' >> c2s '(' >> showExpr expr >> c2s ')' + AbsBasilIR.ProgSpec_Rely (relytok, expr) -> s2s "ProgSpec_Rely" >> c2s ' ' >> c2s '(' >> showRelyTok relytok >> s2s ", " >> showExpr expr >> c2s ')' + | AbsBasilIR.ProgSpec_Guarantee (guartok, expr) -> s2s "ProgSpec_Guarantee" >> c2s ' ' >> c2s '(' >> showGuarTok guartok >> s2s ", " >> showExpr expr >> c2s ')' diff --git a/lib/fe/SkelBasilIR.ml b/lib/fe/SkelBasilIR.ml index 1c6203ff..bd941473 100644 --- a/lib/fe/SkelBasilIR.ml +++ b/lib/fe/SkelBasilIR.ml @@ -1,4 +1,4 @@ -(* File generated by the BNF Converter (bnfc 2.9.6.1). *) +(* File generated by the BNF Converter (bnfc 2.9.6.2). *) module SkelBasilIR = struct @@ -85,11 +85,6 @@ and transLambdaSep (x : lambdaSep) : result = match x with | LambdaSep2 -> failure x -and transSemicolons (x : semicolons) : result = match x with - Semicolons_Empty -> failure x - | Semicolons_Some semicolons -> failure x - - and transVarModifiers (x : varModifiers) : result = match x with Shared -> failure x | Observable -> failure x @@ -120,20 +115,20 @@ and transBoolType (x : boolType) : result = match x with BoolType1 booltype -> failure x -and transMapType (x : mapType) : result = match x with - MapType1 (type'0, type') -> failure x - - and transBVType (x : bVType) : result = match x with BVType1 bvtype -> failure x +and transMapType (x : mapType) : result = match x with + MapType1 (type'0, type') -> failure x + + and transType (x : typeT) : result = match x with TypeIntType inttype -> failure x | TypeBoolType booltype -> failure x - | TypeMapType maptype -> failure x | TypeBVType bvtype -> failure x - | Type1 (openparen, type', closeparen) -> failure x + | TypeParen (openparen, type', closeparen) -> failure x + | TypeMapType maptype -> failure x and transIntVal (x : intVal) : result = match x with @@ -161,10 +156,9 @@ and transStmt (x : stmt) : result = match x with | Stmt_ScalarStore (lvar, expr) -> failure x | Stmt_ScalarLoad (lvar, var) -> failure x | Stmt_MultiAssign (openparen, assignments, closeparen) -> failure x - | Stmt_Load (lvar, endian, globalident, expr, intval) -> failure x - | Stmt_Store (endian, globalident, expr0, expr, intval) -> failure x | Stmt_Load_Var (lvar, endian, var, expr, intval) -> failure x | Stmt_Store_Var (lvar, endian, var, expr0, expr, intval) -> failure x + | Stmt_Store (endian, globalident, expr0, expr, intval) -> failure x | Stmt_DirectCall (lvars, procident, openparen, callparams, closeparen) -> failure x | Stmt_IndirectCall expr -> failure x | Stmt_Assume expr -> failure x @@ -187,6 +181,16 @@ and transVar (x : var) : result = match x with | VarGlobalVar globalvar -> failure x +and transLocalVarParen (x : localVarParen) : result = match x with + LocalVarParenLocalVar localvar -> failure x + | LocalVarParen1 (openparen, localident, type', closeparen) -> failure x + + +and transGlobalVarParen (x : globalVarParen) : result = match x with + GlobalVarParenGlobalVar globalvar -> failure x + | GlobalVarParen1 (openparen, globalident, type', closeparen) -> failure x + + and transNamedCallReturn (x : namedCallReturn) : result = match x with NamedCallReturn1 (lvar, localident) -> failure x @@ -237,7 +241,7 @@ and transPhiAssign (x : phiAssign) : result = match x with and transBlock (x : block) : result = match x with Block_NoPhi (blockident, attribset, beginlist, stmtwithattribs, jumpwithattrib, endlist) -> failure x - | Block_Phi (blockident, attribset, beginlist, openparen, phiassigns, closeparen, stmtwithattribs, jumpwithattrib, endlist) -> failure x + | Block_Phi (blockident, attribset, openparen, phiassigns, closeparen, beginlist, stmtwithattribs, jumpwithattrib, endlist) -> failure x and transAttrKeyValue (x : attrKeyValue) : result = match x with @@ -245,14 +249,13 @@ and transAttrKeyValue (x : attrKeyValue) : result = match x with and transAttribSet (x : attribSet) : result = match x with - AttribSet_Some (beginrec, attrkeyvalues, semicolons, endrec) -> failure x + AttribSet_Some (beginrec, attrkeyvalues, endrec) -> failure x | AttribSet_Empty -> failure x and transAttr (x : attr) : result = match x with - Attr_Map (beginrec, attrkeyvalues, semicolons, endrec) -> failure x + Attr_Map (beginrec, attrkeyvalues, endrec) -> failure x | Attr_List (beginlist, attrs, endlist) -> failure x - | Attr_Lit value -> failure x | Attr_Expr expr -> failure x | Attr_Str str -> failure x @@ -261,11 +264,6 @@ and transParams (x : params) : result = match x with Params1 (localident, type') -> failure x -and transFunParams (x : funParams) : result = match x with - FunParams1 (localident, type') -> failure x - | FunParams2 (openparen, localident, type', closeparen) -> failure x - - and transValue (x : value) : result = match x with Value_BV bvval -> failure x | Value_Int intval -> failure x @@ -275,15 +273,13 @@ and transValue (x : value) : result = match x with and transExpr (x : expr) : result = match x with Expr_Literal value -> failure x - | Expr_Paren (openparen, expr, closeparen) -> failure x | Expr_Local localvar -> failure x | Expr_Global globalvar -> failure x | Expr_Forall (attribset, lambdadef) -> failure x | Expr_Exists (attribset, lambdadef) -> failure x | Expr_Lambda (attribset, lambdadef) -> failure x | Expr_Old (openparen, expr, closeparen) -> failure x - | Expr_FunctionOp (globalident, openparen, exprs, closeparen) -> failure x - | Expr_Apply (expr0, expr) -> failure x + | Expr_FunctionOp (expr, openparen, exprs, closeparen) -> failure x | Expr_Binary (binop, openparen, expr0, expr, closeparen) -> failure x | Expr_Assoc (boolbinop, openparen, exprs, closeparen) -> failure x | Expr_Unary (unop, openparen, expr, closeparen) -> failure x @@ -295,21 +291,16 @@ and transExpr (x : expr) : result = match x with | Expr_Concat (openparen, exprs, closeparen) -> failure x | Expr_Match (expr, openparen, cases, closeparen) -> failure x | Expr_Cases (openparen, cases, closeparen) -> failure x - - -and transLParen (x : lParen) : result = match x with - LParenLocalVar localvar -> failure x - | LParen1 (openparen, localvar, closeparen) -> failure x + | Expr_Paren (openparen, expr, closeparen) -> failure x and transLambdaDef (x : lambdaDef) : result = match x with - LambdaDef1 (lparens, lambdasep, expr) -> failure x + LambdaDef1 (localvarparens, lambdasep, expr) -> failure x and transBinOp (x : binOp) : result = match x with BinOpBVBinOp bvbinop -> failure x | BinOpBVLogicalBinOp bvlogicalbinop -> failure x - | BinOpBoolBinOp boolbinop -> failure x | BinOpIntLogicalBinOp intlogicalbinop -> failure x | BinOpIntBinOp intbinop -> failure x | BinOpEqOp eqop -> failure x @@ -408,7 +399,7 @@ and transRelyTok (x : relyTok) : result = match x with and transGuarTok (x : guarTok) : result = match x with - GuarTok_guarnatee -> failure x + GuarTok_guarantee -> failure x | GuarTok_guarantees -> failure x @@ -428,8 +419,8 @@ and transVarSpec (x : varSpec) : result = match x with and transProgSpec (x : progSpec) : result = match x with - ProgSpec_Rely expr -> failure x - | ProgSpec_Guarantee expr -> failure x + ProgSpec_Rely (relytok, expr) -> failure x + | ProgSpec_Guarantee (guartok, expr) -> failure x diff --git a/lib/fe/TestBasilIR.ml b/lib/fe/TestBasilIR.ml index db9dbc6e..e3da9490 100644 --- a/lib/fe/TestBasilIR.ml +++ b/lib/fe/TestBasilIR.ml @@ -1,4 +1,4 @@ -(* File generated by the BNF Converter (bnfc 2.9.6.1). *) +(* File generated by the BNF Converter (bnfc 2.9.6.2). *) open Lexing diff --git a/lib/fe/dune b/lib/fe/dune index 0ccb4aee..9771b1ac 100644 --- a/lib/fe/dune +++ b/lib/fe/dune @@ -33,4 +33,15 @@ ParBasilIR.mly) (mode promote) (action - (run bnfc --ocaml-menhir -o . BasilIR.cf))) + (progn + (run bnfc --ocaml-menhir -o . BasilIR.cf)))) + +(executable + (name TestBasilIR) + (public_name TestBasilIR) + (package bincaml) + (modes exe byte) + (modules TestBasilIR) + (flags + (:standard -open BasilIR)) + (libraries bincaml.basilir)) diff --git a/lib/lang/block.ml b/lib/lang/block.ml index b5538caa..c7bf5f10 100644 --- a/lib/lang/block.ml +++ b/lib/lang/block.ml @@ -42,22 +42,22 @@ let pretty show_lvar show_var show_expr ?(terminator = []) ?block_id b = Trace_core.with_span ~__FILE__ ~__LINE__ "pretty-block" @@ fun _ -> let open Containers_pp in let open Containers_pp.Infix in + let bracket' ~n l d r : t = group (text l ^ nest n (nl ^ d) ^ nl ^ text r) in let phi = match b.phis with - | [] -> [] + | [] -> nil | o -> let phi = List.map (pretty_phi show_lvar show_var) o in - [ bracket "(" (fill (text "," ^ newline) phi) ")" ] + bracket' ~n:2 "(" + (append_l ~sep:(text "," ^ nl) (List.map group phi)) + ") " in let stmts = Vector.to_list b.stmts |> List.map (Stmt.pretty show_lvar show_var show_expr) in - let stmts = phi @ stmts @ terminator |> List.map (fun i -> i ^ text ";") in - let bracket' l d r : t = - group (text l ^ nest (String.length l) d ^ nl ^ text r) - in - let stmts = bracket' "[" (nest 2 @@ nl ^ append_nl stmts) "]" in + let stmts = stmts @ terminator |> List.map (fun i -> i ^ text ";") in + let stmts = phi ^ bracket' ~n:2 "[" (append_nl stmts) "]" in let name = Option.map (fun id -> text "block " ^ text (ID.to_string id) ^ text " ") diff --git a/lib/lang/expr.ml b/lib/lang/expr.ml index 017f179b..3ba9b12c 100644 --- a/lib/lang/expr.ml +++ b/lib/lang/expr.ml @@ -386,7 +386,10 @@ module BasilExpr = struct ] | ApplyFun { func = n; args = es } -> fill nil - [ n ^ a ^ bracket "(" (nest 2 (fill (text "," ^ newline) es)) ")" ] + [ + bracket "(" n ")" ^ a + ^ bracket "(" (nest 2 (fill (text "," ^ newline) es)) ")"; + ] | Binding { bound = vs; in_body = b } -> fill (text " ") (List.map (fun v -> bracket "(" (Var.pretty v) ")") vs) ^ text " :: " ^ a ^ bracket "(" b ")" diff --git a/lib/lang/procedure.ml b/lib/lang/procedure.ml index 777bd11c..c3f8c77e 100644 --- a/lib/lang/procedure.ml +++ b/lib/lang/procedure.ml @@ -496,7 +496,7 @@ let iter_blocks_topo_rev p = let pretty_spec show_var show_expr (p : ('a, 'b) proc_spec) = let open Containers_pp in - let ml f v = if List.is_empty v then [] else [ f v ^ text ";" ] in + let ml f v = if List.is_empty v then [] else [ f v ] in nest 2 (newline ^ append_nl @@ -513,25 +513,25 @@ let pretty_spec show_var show_expr (p : ('a, 'b) proc_spec) = @ ml (fun x -> append_l - ~sep:(text ";" ^ newline) + ~sep:newline (List.map (fun v -> text "requires " ^ show_expr v) x)) p.requires @ ml (fun x -> append_l - ~sep:(text ";" ^ newline) + ~sep:newline (List.map (fun v -> text "ensures " ^ show_expr v) x)) p.ensures @ ml (fun x -> append_l - ~sep:(text ";" ^ newline) + ~sep:newline (List.map (fun v -> text "rely " ^ show_expr v) x)) p.rely @ ml (fun x -> append_l - ~sep:(text ";" ^ newline) + ~sep:newline (List.map (fun v -> text "guarantee " ^ show_expr v) x)) p.guarantee)) diff --git a/lib/loadir.ml b/lib/loadir.ml index 2805a554..ba88009b 100644 --- a/lib/loadir.ml +++ b/lib/loadir.ml @@ -232,12 +232,12 @@ module BasilASTLoader = struct |> map_prog (fun prog -> let spec = prog.spec in match p with - | ProgSpec_Rely b -> + | ProgSpec_Rely (_, b) -> { prog with spec = { spec with rely = trans_expr p_st b :: spec.rely }; } - | ProgSpec_Guarantee b -> + | ProgSpec_Guarantee (_, b) -> { prog with spec = @@ -413,7 +413,7 @@ module BasilASTLoader = struct | TypeBoolType booltype -> Boolean | TypeMapType maptype -> transMapType maptype | TypeBVType (BVType1 bvtype) -> transBVTYPE bvtype - | Type1 (_, typeT, _) -> trans_type typeT + | TypeParen (_, typeT, _) -> trans_type typeT and transIntVal (x : intVal) : PrimInt.t = match x with @@ -450,9 +450,8 @@ module BasilASTLoader = struct and trans_attr p_st ~binds (attr : attr) : [> Expr.BasilExpr.t Attrib.t ] = match attr with - | Attr_Map (_, keyvals, _, _) -> `Assoc (trans_attr_kv ~binds p_st keyvals) + | Attr_Map (_, keyvals, _) -> `Assoc (trans_attr_kv ~binds p_st keyvals) | Attr_List (_, ls, _) -> `List (List.map (trans_attr ~binds p_st) ls) - | Attr_Lit v -> ( match trans_value v with #Ops.AllOps.const as v -> v) | Attr_Expr expr -> `Expr (trans_expr ~binds p_st expr) | Attr_Str s -> `String (trans_str s) @@ -460,7 +459,7 @@ module BasilASTLoader = struct Expr.BasilExpr.t Attrib.attrib_map = match atrs with | AttribSet_Empty -> StringMap.empty - | AttribSet_Some (_, attrKeyValue, _, _) -> + | AttribSet_Some (_, attrKeyValue, _) -> trans_attr_kv ~binds p_st attrKeyValue and trans_stmt (p_st : load_st) (x : BasilIR.AbsBasilIR.stmtWithAttrib) : @@ -499,6 +498,19 @@ module BasilASTLoader = struct value = trans_expr p_st value; addr = Addr { addr = trans_expr p_st addr; size; endian }; }) ) + | Stmt_Store (endian, bident, addr, value, intval) -> + let endian = trans_endian endian in + let size = transIntVal intval |> Z.to_int in + let mem = lookup_global_decl bident p_st in + ( p_st, + `Stmt + (Instr_Store + { + lhs = mem; + rhs = mem; + value = trans_expr p_st value; + addr = Addr { addr = trans_expr p_st addr; size; endian }; + }) ) | Stmt_SingleAssign (Assignment1 (lvar, expr)) -> let expr = trans_expr p_st expr in let p_st, lv = trans_lvar p_st lvar in @@ -529,27 +541,6 @@ module BasilASTLoader = struct in let p_st, assigns = List.fold_left f (p_st, []) assigns in (p_st, `Stmt (Instr_Assign (List.rev assigns))) - | Stmt_Load (lvar, endian, bident, expr, intval) -> - let endian = trans_endian endian in - let rhs = lookup_global_decl bident p_st in - let addr = trans_expr p_st expr in - let p_st, lhs = trans_lvar p_st lvar in - let size = transIntVal intval |> Z.to_int in - ( p_st, - `Stmt (Instr_Load { lhs; rhs; addr = Addr { addr; endian; size } }) ) - | Stmt_Store (endian, bident, addr, value, intval) -> - let endian = trans_endian endian in - let size = transIntVal intval |> Z.to_int in - let mem = lookup_global_decl bident p_st in - ( p_st, - `Stmt - (Instr_Store - { - lhs = mem; - rhs = mem; - value = trans_expr p_st value; - addr = Addr { addr = trans_expr p_st addr; size; endian }; - }) ) | Stmt_DirectCall (calllvars, bident, o, exprs, c) -> let n = unsafe_unsigil (`Proc bident) in let procid = @@ -625,7 +616,11 @@ module BasilASTLoader = struct and unpac_lambdaparen ?(bound = StringMap.empty) p_st lvs = unpack_local_lvars ~bound p_st - @@ List.map (function LParenLocalVar v -> v | LParen1 (o, v, c) -> v) lvs + @@ List.map + (function + | LocalVarParenLocalVar v -> v + | LocalVarParen1 (_, i, t, _) -> LocalTyped (i, t)) + lvs and trans_jump p_st (x : BasilIR.AbsBasilIR.jumpWithAttrib) = let jump = match x with JumpWithAttrib1 (jump, _) -> jump in @@ -725,21 +720,21 @@ module BasilASTLoader = struct | Block_NoPhi ( BlockIdent (text_range, name), addrattr, - beginlist, + BeginList _, statements, jump, - endlist ) -> + EndList _ ) -> tx name [] statements jump | Block_Phi ( BlockIdent (text_range, name), addrattr, - beginlist, - _, + OpenParen _, phi, - _, + CloseParen _, + BeginList _, statements, jump, - endlist ) -> + EndList _ ) -> tx name phi statements jump and param_to_lvar (pp : params) : Var.t = @@ -750,12 +745,6 @@ module BasilASTLoader = struct match pp with | Params1 (LocalIdent (pos, id), t) -> (id, Var.create id (trans_type t)) - and fun_param_to_formal pp : string * Var.t = - match pp with - | FunParams1 (LocalIdent (pos, id), t) -> (id, Var.create id (trans_type t)) - | FunParams2 (_, LocalIdent (pos, id), t, _) -> - (id, Var.create id (trans_type t)) - and trans_funspec prog bound_post (spec : (Var.t, BasilExpr.t) Procedure.proc_spec) (s : funSpec) : (Var.t, BasilExpr.t) Procedure.proc_spec = @@ -978,23 +967,15 @@ module BasilASTLoader = struct in let attrib = `Assoc (trans_attrib_set ~binds p_st attrs) in BasilExpr.exists ~attrib ~bound (trans_expr ~nbinds:bound e) - | Expr_FunctionOp (gi, o, args, c) -> - BasilExpr.apply_fun ~attrib:(expr_range_attr o c) - ~func:(BasilExpr.rvar @@ lookup_global_decl gi p_st) - (List.map trans_expr args) - | Expr_Apply (func, arg) -> + | Expr_FunctionOp (func, o, args, c) -> let func = trans_expr func in - let arg = trans_expr arg in - let attrib = - join_ranges (BasilExpr.attrib func) (BasilExpr.attrib arg) - in - BasilExpr.apply_fun ~attrib ~func [ arg ] + BasilExpr.apply_fun ~func ~attrib:(expr_range_attr o c) + (List.map trans_expr args) and transBinOp (x : BasilIR.AbsBasilIR.binOp) = match x with | BinOpBVBinOp bvbinop -> transBVBinOp bvbinop | BinOpBVLogicalBinOp bvlogicalbinop -> transBVLogicalBinOp bvlogicalbinop - | BinOpBoolBinOp boolbinop -> transBoolBinOp boolbinop | BinOpIntLogicalBinOp intlogicalbinop -> transIntLogicalBinOp intlogicalbinop | BinOpIntBinOp intbinop -> transIntBinOp intbinop @@ -1409,14 +1390,14 @@ proc @main_4196260 () -> () var $ZF:bv1; prog entry @main_4196260; proc @main_4196260() -> () { } - modifies $NF:bv1, $ZF:bv1; - captures $NF:bv1, $ZF:bv1; + modifies $NF:bv1, $ZF:bv1 + captures $NF:bv1, $ZF:bv1 [ block %main_entry [ - $NF:bv1 := 0x1:bv1; - $ZF:bv1 := $NF:bv1; - goto (%main_basil_return_1); + $NF:bv1 := 0x1:bv1; + $ZF:bv1 := $NF:bv1; + goto (%main_basil_return_1); ]; block %main_basil_return_1 [ nop; return; ] ]; @@ -1475,4 +1456,18 @@ proc @c() -> () written: $R0:bv64,$mem:(bv64->bv8) @c: read: $R0:bv64,$mem:(bv64->bv8) - written: $mem:(bv64->bv8) |}] + written: $mem:(bv64->bv8) + |}] + +let%test_unit "parses parenthesised lambda param" = + let s = + {| + let $memory_load32_le : (bv64 -> bv8) -> bv64 -> bv32 = fun (#memory: bv64 -> bv8), (#index: bv64) :: + (bvconcat(load_le(8, #memory, bvadd(#index, 3:bv64)), + bvconcat((load_le(8, #memory, bvadd(#index, 2:bv64))), + bvconcat((load_le(8, #memory, bvadd(#index, 1:bv64))), + load_le(8, #memory, #index))))); + |} + in + let _ = ast_of_string ~__LINE__ ~__FILE__ ~__FUNCTION__ s in + () diff --git a/test/analysis/ide_live.ml b/test/analysis/ide_live.ml index 21dd2b4d..0c5acaab 100644 --- a/test/analysis/ide_live.ml +++ b/test/analysis/ide_live.ml @@ -42,8 +42,7 @@ proc @main () -> () let _, results = IDELiveAnalysis.solve program in let main = program.entry_proc |> Option.get_exn_or "No entry proc" in print_lives results main; - [%expect - {| + [%expect {| @main $mem:(bv64->bv8) $x:bv64 @@ -82,8 +81,7 @@ proc @fun (c:bv64, d:bv64) -> (out:bv64) let program = lst.prog in let _, results = IDELiveAnalysis.solve program in ID.Map.iter (fun id _ -> print_lives results id) program.procs; - [%expect - {| + [%expect {| @main b:bv64 y:bv64 @@ -131,8 +129,7 @@ proc @fun2 (f:bv64) -> (out2:bv64) let program = lst.prog in let _, results = IDELiveAnalysis.solve program in ID.Map.iter (fun id _ -> print_lives results id) program.procs; - [%expect - {| + [%expect {| @main b:bv64 y:bv64 @@ -197,8 +194,7 @@ proc @fun2 (f:bv64) -> (out2:bv64) let program = lst.prog in let _, results = IDELiveAnalysis.solve program in ID.Map.iter (fun id _ -> print_lives results id) program.procs; - [%expect - {| + [%expect {| @main b:bv64 y:bv64 diff --git a/test/analysis/ssadfg.ml b/test/analysis/ssadfg.ml index d17f13ec..5f0d38cc 100644 --- a/test/analysis/ssadfg.ml +++ b/test/analysis/ssadfg.ml @@ -72,8 +72,7 @@ proc @main_4196260 () -> () (Analysis.Defuse_bool.IsZeroLattice.show v)) in print_endline f; - [%expect - {| + [%expect {| CF_out->Top NF_out->NonZero R0_out->Zero diff --git a/test/cram/basicssa.t b/test/cram/basicssa.t index 1e7d6527..5129885e 100644 --- a/test/cram/basicssa.t +++ b/test/cram/basicssa.t @@ -19,110 +19,110 @@ Run on basic irreducible loop example proc @main_1876() -> () { .address = 1876; .name = "main"; .returnBlock = "main_basil_return_1" } modifies $mem:(bv64->bv8), $stack:(bv64->bv8), $CF:bv1, $NF:bv1, $R0:bv64, - $R1:bv64, $R29:bv64, $R30:bv64, $R31:bv64, $VF:bv1, $ZF:bv1; + $R1:bv64, $R29:bv64, $R30:bv64, $R31:bv64, $VF:bv1, $ZF:bv1 captures $mem:(bv64->bv8), $stack:(bv64->bv8), $CF:bv1, $NF:bv1, $R0:bv64, - $R1:bv64, $R29:bv64, $R30:bv64, $R31:bv64, $VF:bv1, $ZF:bv1; + $R1:bv64, $R29:bv64, $R30:bv64, $R31:bv64, $VF:bv1, $ZF:bv1 [ 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; - $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 := 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)); - goto (%main_27,%main_23); + 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; + $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 := 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)); + goto (%main_27,%main_23); ]; block %main_23 [ - guard neq(booltobv1(eq($ZF:bv1, 0x1:bv1)), 0x0:bv1); - goto (%main_21); + guard neq(booltobv1(eq($ZF:bv1, 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); - goto (%main_25); + guard eq(booltobv1(eq($ZF:bv1, 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); - $R30:bv64 := 0x7a0:bv64; - - call @puts_1584(); - goto (%main_3); + $R0:bv64 := 0x0:bv64; + $R0:bv64 := bvadd($R0:bv64, 0x820:bv64); + $R30:bv64 := 0x7a0:bv64; + + call @puts_1584(); + goto (%main_3); ]; 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 := 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; - goto (%main_19); + $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 := 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; + goto (%main_19); ]; block %main_19 [ - $R0:bv64 := 0x0:bv64; - $R0:bv64 := bvadd($R0:bv64, 0x820:bv64); - $R30:bv64 := 0x7d0:bv64; - - call @puts_1584(); - goto (%main_17); + $R0:bv64 := 0x0:bv64; + $R0:bv64 := bvadd($R0:bv64, 0x820:bv64); + $R30:bv64 := 0x7d0:bv64; + + call @puts_1584(); + goto (%main_17); ]; 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)); - goto (%main_15,%main_9); + $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)); + goto (%main_15,%main_9); ]; block %main_9 [ - guard neq(bvnot(booltobv1(eq($ZF:bv1, 0x1:bv1))), 0x0:bv1); - goto (%main_7); + guard neq(bvnot(booltobv1(eq($ZF:bv1, 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); - $R0:bv64 := 0x0:bv64; - $R0:bv64 := bvadd($R0:bv64, 0x828:bv64); - $R30:bv64 := 0x7f4:bv64; - - call @puts_1584(); - goto (%main_13); + guard eq(bvnot(booltobv1(eq($ZF:bv1, 0x1:bv1))), 0x0:bv1); + $R0:bv64 := 0x0:bv64; + $R0:bv64 := bvadd($R0:bv64, 0x828:bv64); + $R30:bv64 := 0x7f4:bv64; + + call @puts_1584(); + goto (%main_13); ]; 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); - goto (%main_basil_return_1); + $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); + goto (%main_basil_return_1); ]; block %main_basil_return_1 [ nop; return; ] ]; @@ -149,162 +149,158 @@ Run on basic irreducible loop example R30_out:bv64, R31_out:bv64, VF_out:bv1, ZF_out:bv1) { .address = 1876; .name = "main"; .returnBlock = "main_basil_return_1" } modifies $mem:(bv64->bv8), $stack:(bv64->bv8), $CF:bv1, $NF:bv1, $R0:bv64, - $R1:bv64, $R29:bv64, $R30:bv64, $R31:bv64, $VF:bv1, $ZF:bv1; + $R1:bv64, $R29:bv64, $R30:bv64, $R31:bv64, $VF:bv1, $ZF:bv1 captures $mem:(bv64->bv8), $stack:(bv64->bv8), $CF:bv1, $NF:bv1, $R0:bv64, - $R1:bv64, $R29:bv64, $R30:bv64, $R31:bv64, $VF:bv1, $ZF:bv1; + $R1:bv64, $R29:bv64, $R30:bv64, $R31:bv64, $VF:bv1, $ZF:bv1 [ block %inputs [ - (var CF:bv1 := CF_in:bv1, var NF:bv1 := NF_in:bv1, var R0:bv64 := R0_in:bv64, - var R1:bv64 := R1_in:bv64, var R29:bv64 := R29_in:bv64, - var R30:bv64 := R30_in:bv64, var R31:bv64 := R31_in:bv64, - var VF:bv1 := VF_in:bv1, var ZF:bv1 := ZF_in:bv1); - goto (%main_entry); + (var CF:bv1 := CF_in:bv1, var NF:bv1 := NF_in:bv1, var R0:bv64 := R0_in:bv64, + var R1:bv64 := R1_in:bv64, var R29:bv64 := R29_in:bv64, + var R30:bv64 := R30_in:bv64, var R31:bv64 := R31_in:bv64, + var VF:bv1 := VF_in:bv1, var ZF:bv1 := ZF_in:bv1); + goto (%main_entry); ]; block %main_entry [ - var #4_1:bv64 := bvadd(R31:bv64, 0xffffffffffffffe0:bv64); - $stack:(bv64->bv8) := store le $stack:(bv64->bv8) #4_1:bv64 R29:bv64 64; - $stack:(bv64->bv8) := store le $stack:(bv64->bv8) bvadd(#4_1:bv64, 0x8:bv64) R30:bv64 64; - var R31_1:bv64 := #4_1:bv64; - var R29_1:bv64 := R31_1:bv64; - $stack:(bv64->bv8) := store le $stack:(bv64->bv8) bvadd(R31_1:bv64, - 0x1c:bv64) extract(32,0, R0:bv64) 32; - $stack:(bv64->bv8) := store le $stack:(bv64->bv8) bvadd(R31_1:bv64, - 0x10:bv64) R1:bv64 64; - var R0_1:bv64 := 0x20000:bv64; - var R0_2:bv64 := bvadd(R0_1:bv64, 0x3c:bv64); - $mem:(bv64->bv8) := store le $mem:(bv64->bv8) R0_2:bv64 0x0:bv32 32; - var R0_3:bv64 := 0x20000:bv64; - var R0_4:bv64 := bvadd(R0_3:bv64, 0x40:bv64); - var load18_1:bv32 := load le $mem:(bv64->bv8) R0_4:bv64 32; - var R0_5:bv64 := zero_extend(32, load18_1:bv32); - var R0_6:bv64 := zero_extend(32, - bvconcat(0x0:bv31, extract(1,0, R0_5:bv64))); - var #5_1:bv32 := bvadd(extract(32,0, R0_6:bv64), 0xffffffff:bv32); - var VF_1:bv1 := bvnot(booltobv1(eq(sign_extend(1, - bvadd(#5_1:bv32, 0x1:bv32)), sign_extend(1, extract(32,0, R0_6:bv64))))); - var CF_1:bv1 := bvnot(booltobv1(eq(zero_extend(1, - bvadd(#5_1:bv32, 0x1:bv32)), - bvadd(zero_extend(1, extract(32,0, R0_6:bv64)), 0x100000000:bv33)))); - var ZF_1:bv1 := booltobv1(eq(bvadd(#5_1:bv32, 0x1:bv32), 0x0:bv32)); - var NF_1:bv1 := extract(32,31, bvadd(#5_1:bv32, 0x1:bv32)); - goto (%main_27,%main_23); + var #4_1:bv64 := bvadd(R31:bv64, 0xffffffffffffffe0:bv64); + $stack:(bv64->bv8) := store le $stack:(bv64->bv8) #4_1:bv64 R29:bv64 64; + $stack:(bv64->bv8) := store le $stack:(bv64->bv8) bvadd(#4_1:bv64, 0x8:bv64) R30:bv64 64; + var R31_1:bv64 := #4_1:bv64; + var R29_1:bv64 := R31_1:bv64; + $stack:(bv64->bv8) := store le $stack:(bv64->bv8) bvadd(R31_1:bv64, 0x1c:bv64) extract(32,0, R0:bv64) 32; + $stack:(bv64->bv8) := store le $stack:(bv64->bv8) bvadd(R31_1:bv64, 0x10:bv64) R1:bv64 64; + var R0_1:bv64 := 0x20000:bv64; + var R0_2:bv64 := bvadd(R0_1:bv64, 0x3c:bv64); + $mem:(bv64->bv8) := store le $mem:(bv64->bv8) R0_2:bv64 0x0:bv32 32; + var R0_3:bv64 := 0x20000:bv64; + var R0_4:bv64 := bvadd(R0_3:bv64, 0x40:bv64); + var load18_1:bv32 := load le $mem:(bv64->bv8) R0_4:bv64 32; + var R0_5:bv64 := zero_extend(32, load18_1:bv32); + var R0_6:bv64 := zero_extend(32, bvconcat(0x0:bv31, extract(1,0, R0_5:bv64))); + var #5_1:bv32 := bvadd(extract(32,0, R0_6:bv64), 0xffffffff:bv32); + var VF_1:bv1 := bvnot(booltobv1(eq(sign_extend(1, bvadd(#5_1:bv32, 0x1:bv32)), + sign_extend(1, extract(32,0, R0_6:bv64))))); + var CF_1:bv1 := bvnot(booltobv1(eq(zero_extend(1, bvadd(#5_1:bv32, 0x1:bv32)), + bvadd(zero_extend(1, extract(32,0, R0_6:bv64)), 0x100000000:bv33)))); + var ZF_1:bv1 := booltobv1(eq(bvadd(#5_1:bv32, 0x1:bv32), 0x0:bv32)); + var NF_1:bv1 := extract(32,31, bvadd(#5_1:bv32, 0x1:bv32)); + goto (%main_27,%main_23); ]; block %main_23 [ - var ZF_3:bv1 := ZF_1:bv1; - guard neq(booltobv1(eq(ZF_3:bv1, 0x1:bv1)), 0x0:bv1); - goto (%main_21); + var ZF_3:bv1 := ZF_1:bv1; + guard neq(booltobv1(eq(ZF_3:bv1, 0x1:bv1)), 0x0:bv1); + goto (%main_21); ]; block %main_21 [ goto (%main_19); ]; block %main_27 [ - var ZF_2:bv1 := ZF_1:bv1; - guard eq(booltobv1(eq(ZF_2:bv1, 0x1:bv1)), 0x0:bv1); - goto (%main_25); + var ZF_2:bv1 := ZF_1:bv1; + guard eq(booltobv1(eq(ZF_2:bv1, 0x1:bv1)), 0x0:bv1); + goto (%main_25); ]; block %main_25 [ goto (%main_5); ]; - block %main_5 [ - (var CF_5:bv1 := phi(%main_25 -> CF_1:bv1, %main_7 -> CF_4:bv1), - var NF_5:bv1 := phi(%main_25 -> NF_1:bv1, %main_7 -> NF_4:bv1), - var R1_3:bv64 := phi(%main_25 -> R1:bv64, %main_7 -> R1_2:bv64), - var R29_4:bv64 := phi(%main_25 -> R29_1:bv64, %main_7 -> R29_3:bv64), - var R31_4:bv64 := phi(%main_25 -> R31_1:bv64, %main_7 -> R31_3:bv64), - var VF_5:bv1 := phi(%main_25 -> VF_1:bv1, %main_7 -> VF_4:bv1), - var ZF_8:bv1 := phi(%main_25 -> ZF_2:bv1, %main_7 -> ZF_7:bv1)); - var R0_13:bv64 := 0x0:bv64; - var R0_14:bv64 := bvadd(R0_13:bv64, 0x820:bv64); - var R30_3:bv64 := 0x7a0:bv64; - (var CF_6:bv1=CF_out, var NF_6:bv1=NF_out, var R0_15:bv64=R0_out, - var R1_4:bv64=R1_out, var R29_5:bv64=R29_out, var R30_4:bv64=R30_out, - var R31_5:bv64=R31_out, var VF_6:bv1=VF_out, var ZF_9:bv1=ZF_out) := - call @puts_1584(CF_in=CF_5:bv1, NF_in=NF_5:bv1, R0_in=R0_14:bv64, - R1_in=R1_3:bv64, R29_in=R29_4:bv64, R30_in=R30_3:bv64, R31_in=R31_4:bv64, - VF_in=VF_5:bv1, ZF_in=ZF_8:bv1); - goto (%main_3); + block %main_5 ( + var CF_5:bv1 := phi(%main_25 -> CF_1:bv1, %main_7 -> CF_4:bv1), + var NF_5:bv1 := phi(%main_25 -> NF_1:bv1, %main_7 -> NF_4:bv1), + var R1_3:bv64 := phi(%main_25 -> R1:bv64, %main_7 -> R1_2:bv64), + var R29_4:bv64 := phi(%main_25 -> R29_1:bv64, %main_7 -> R29_3:bv64), + var R31_4:bv64 := phi(%main_25 -> R31_1:bv64, %main_7 -> R31_3:bv64), + var VF_5:bv1 := phi(%main_25 -> VF_1:bv1, %main_7 -> VF_4:bv1), + var ZF_8:bv1 := phi(%main_25 -> ZF_2:bv1, %main_7 -> ZF_7:bv1) + ) [ + var R0_13:bv64 := 0x0:bv64; + var R0_14:bv64 := bvadd(R0_13:bv64, 0x820:bv64); + var R30_3:bv64 := 0x7a0:bv64; + (var CF_6:bv1=CF_out, var NF_6:bv1=NF_out, var R0_15:bv64=R0_out, + var R1_4:bv64=R1_out, var R29_5:bv64=R29_out, var R30_4:bv64=R30_out, + var R31_5:bv64=R31_out, var VF_6:bv1=VF_out, var ZF_9:bv1=ZF_out) := + call @puts_1584(CF_in=CF_5:bv1, NF_in=NF_5:bv1, R0_in=R0_14:bv64, + R1_in=R1_3:bv64, R29_in=R29_4:bv64, R30_in=R30_3:bv64, R31_in=R31_4:bv64, + VF_in=VF_5:bv1, ZF_in=ZF_8:bv1); + goto (%main_3); ]; block %main_3 [ - var R0_16:bv64 := 0x20000:bv64; - var R0_17:bv64 := bvadd(R0_16:bv64, 0x3c:bv64); - var load19_1:bv32 := load le $mem:(bv64->bv8) R0_17:bv64 32; - var R0_18:bv64 := zero_extend(32, load19_1:bv32); - var R1_5:bv64 := zero_extend(32, bvadd(extract(32,0, R0_18:bv64), 0x1:bv32)); - var R0_19:bv64 := 0x20000:bv64; - var R0_20:bv64 := bvadd(R0_19:bv64, 0x3c:bv64); - $mem:(bv64->bv8) := store le $mem:(bv64->bv8) R0_20:bv64 extract(32,0, R1_5:bv64) 32; - goto (%main_19); + var R0_16:bv64 := 0x20000:bv64; + var R0_17:bv64 := bvadd(R0_16:bv64, 0x3c:bv64); + var load19_1:bv32 := load le $mem:(bv64->bv8) R0_17:bv64 32; + var R0_18:bv64 := zero_extend(32, load19_1:bv32); + var R1_5:bv64 := zero_extend(32, bvadd(extract(32,0, R0_18:bv64), 0x1:bv32)); + var R0_19:bv64 := 0x20000:bv64; + var R0_20:bv64 := bvadd(R0_19:bv64, 0x3c:bv64); + $mem:(bv64->bv8) := store le $mem:(bv64->bv8) R0_20:bv64 extract(32,0, R1_5:bv64) 32; + goto (%main_19); ]; - block %main_19 [ - (var CF_2:bv1 := phi(%main_3 -> CF_6:bv1, %main_21 -> CF_1:bv1), - var NF_2:bv1 := phi(%main_3 -> NF_6:bv1, %main_21 -> NF_1:bv1), - var R1_1:bv64 := phi(%main_3 -> R1_5:bv64, %main_21 -> R1:bv64), - var R29_2:bv64 := phi(%main_3 -> R29_5:bv64, %main_21 -> R29_1:bv64), - var R31_2:bv64 := phi(%main_3 -> R31_5:bv64, %main_21 -> R31_1:bv64), - var VF_2:bv1 := phi(%main_3 -> VF_6:bv1, %main_21 -> VF_1:bv1), - var ZF_4:bv1 := phi(%main_3 -> ZF_9:bv1, %main_21 -> ZF_3:bv1)); - var R0_7:bv64 := 0x0:bv64; - var R0_8:bv64 := bvadd(R0_7:bv64, 0x820:bv64); - var R30_1:bv64 := 0x7d0:bv64; - (var CF_3:bv1=CF_out, var NF_3:bv1=NF_out, var R0_9:bv64=R0_out, - var R1_2:bv64=R1_out, var R29_3:bv64=R29_out, var R30_2:bv64=R30_out, - var R31_3:bv64=R31_out, var VF_3:bv1=VF_out, var ZF_5:bv1=ZF_out) := - call @puts_1584(CF_in=CF_2:bv1, NF_in=NF_2:bv1, R0_in=R0_8:bv64, - R1_in=R1_1:bv64, R29_in=R29_2:bv64, R30_in=R30_1:bv64, R31_in=R31_2:bv64, - VF_in=VF_2:bv1, ZF_in=ZF_4:bv1); - goto (%main_17); + block %main_19 ( + var CF_2:bv1 := phi(%main_3 -> CF_6:bv1, %main_21 -> CF_1:bv1), + var NF_2:bv1 := phi(%main_3 -> NF_6:bv1, %main_21 -> NF_1:bv1), + var R1_1:bv64 := phi(%main_3 -> R1_5:bv64, %main_21 -> R1:bv64), + var R29_2:bv64 := phi(%main_3 -> R29_5:bv64, %main_21 -> R29_1:bv64), + var R31_2:bv64 := phi(%main_3 -> R31_5:bv64, %main_21 -> R31_1:bv64), + var VF_2:bv1 := phi(%main_3 -> VF_6:bv1, %main_21 -> VF_1:bv1), + var ZF_4:bv1 := phi(%main_3 -> ZF_9:bv1, %main_21 -> ZF_3:bv1) + ) [ + var R0_7:bv64 := 0x0:bv64; + var R0_8:bv64 := bvadd(R0_7:bv64, 0x820:bv64); + var R30_1:bv64 := 0x7d0:bv64; + (var CF_3:bv1=CF_out, var NF_3:bv1=NF_out, var R0_9:bv64=R0_out, + var R1_2:bv64=R1_out, var R29_3:bv64=R29_out, var R30_2:bv64=R30_out, + var R31_3:bv64=R31_out, var VF_3:bv1=VF_out, var ZF_5:bv1=ZF_out) := + call @puts_1584(CF_in=CF_2:bv1, NF_in=NF_2:bv1, R0_in=R0_8:bv64, + R1_in=R1_1:bv64, R29_in=R29_2:bv64, R30_in=R30_1:bv64, R31_in=R31_2:bv64, + VF_in=VF_2:bv1, ZF_in=ZF_4:bv1); + goto (%main_17); ]; block %main_17 [ - var R0_10:bv64 := 0x20000:bv64; - var R0_11:bv64 := bvadd(R0_10:bv64, 0x3c:bv64); - var load20_1:bv32 := load le $mem:(bv64->bv8) R0_11:bv64 32; - var R0_12:bv64 := zero_extend(32, load20_1:bv32); - var #6_1:bv32 := bvadd(extract(32,0, R0_12:bv64), 0xfffffffa:bv32); - var VF_4:bv1 := bvnot(booltobv1(eq(sign_extend(1, - bvadd(#6_1:bv32, 0x1:bv32)), - bvadd(sign_extend(1, extract(32,0, R0_12:bv64)), 0x1fffffffb:bv33)))); - var CF_4:bv1 := bvnot(booltobv1(eq(zero_extend(1, - bvadd(#6_1:bv32, 0x1:bv32)), - bvadd(zero_extend(1, extract(32,0, R0_12:bv64)), 0xfffffffb:bv33)))); - var ZF_6:bv1 := booltobv1(eq(bvadd(#6_1:bv32, 0x1:bv32), 0x0:bv32)); - var NF_4:bv1 := extract(32,31, bvadd(#6_1:bv32, 0x1:bv32)); - goto (%main_15,%main_9); + var R0_10:bv64 := 0x20000:bv64; + var R0_11:bv64 := bvadd(R0_10:bv64, 0x3c:bv64); + var load20_1:bv32 := load le $mem:(bv64->bv8) R0_11:bv64 32; + var R0_12:bv64 := zero_extend(32, load20_1:bv32); + var #6_1:bv32 := bvadd(extract(32,0, R0_12:bv64), 0xfffffffa:bv32); + var VF_4:bv1 := bvnot(booltobv1(eq(sign_extend(1, bvadd(#6_1:bv32, 0x1:bv32)), + bvadd(sign_extend(1, extract(32,0, R0_12:bv64)), 0x1fffffffb:bv33)))); + var CF_4:bv1 := bvnot(booltobv1(eq(zero_extend(1, bvadd(#6_1:bv32, 0x1:bv32)), + bvadd(zero_extend(1, extract(32,0, R0_12:bv64)), 0xfffffffb:bv33)))); + var ZF_6:bv1 := booltobv1(eq(bvadd(#6_1:bv32, 0x1:bv32), 0x0:bv32)); + var NF_4:bv1 := extract(32,31, bvadd(#6_1:bv32, 0x1:bv32)); + goto (%main_15,%main_9); ]; block %main_9 [ - var ZF_7:bv1 := ZF_6:bv1; - guard neq(bvnot(booltobv1(eq(ZF_7:bv1, 0x1:bv1))), 0x0:bv1); - goto (%main_7); + var ZF_7:bv1 := ZF_6:bv1; + guard neq(bvnot(booltobv1(eq(ZF_7:bv1, 0x1:bv1))), 0x0:bv1); + goto (%main_7); ]; block %main_7 [ goto (%main_5); ]; block %main_15 [ - var ZF_10:bv1 := ZF_6:bv1; - guard eq(bvnot(booltobv1(eq(ZF_10:bv1, 0x1:bv1))), 0x0:bv1); - var R0_21:bv64 := 0x0:bv64; - var R0_22:bv64 := bvadd(R0_21:bv64, 0x828:bv64); - var R30_5:bv64 := 0x7f4:bv64; - (var CF_7:bv1=CF_out, var NF_7:bv1=NF_out, var R0_23:bv64=R0_out, - var R1_6:bv64=R1_out, var R29_6:bv64=R29_out, var R30_6:bv64=R30_out, - var R31_6:bv64=R31_out, var VF_7:bv1=VF_out, var ZF_11:bv1=ZF_out) := - call @puts_1584(CF_in=CF_4:bv1, NF_in=NF_4:bv1, R0_in=R0_22:bv64, - R1_in=R1_2:bv64, R29_in=R29_3:bv64, R30_in=R30_5:bv64, R31_in=R31_3:bv64, - VF_in=VF_4:bv1, ZF_in=ZF_10:bv1); - goto (%main_13); + var ZF_10:bv1 := ZF_6:bv1; + guard eq(bvnot(booltobv1(eq(ZF_10:bv1, 0x1:bv1))), 0x0:bv1); + var R0_21:bv64 := 0x0:bv64; + var R0_22:bv64 := bvadd(R0_21:bv64, 0x828:bv64); + var R30_5:bv64 := 0x7f4:bv64; + (var CF_7:bv1=CF_out, var NF_7:bv1=NF_out, var R0_23:bv64=R0_out, + var R1_6:bv64=R1_out, var R29_6:bv64=R29_out, var R30_6:bv64=R30_out, + var R31_6:bv64=R31_out, var VF_7:bv1=VF_out, var ZF_11:bv1=ZF_out) := + call @puts_1584(CF_in=CF_4:bv1, NF_in=NF_4:bv1, R0_in=R0_22:bv64, + R1_in=R1_2:bv64, R29_in=R29_3:bv64, R30_in=R30_5:bv64, R31_in=R31_3:bv64, + VF_in=VF_4:bv1, ZF_in=ZF_10:bv1); + goto (%main_13); ]; block %main_13 [ goto (%main_11); ]; block %main_11 [ - var R0_24:bv64 := 0x0:bv64; - var load21_1:bv64 := load le $stack:(bv64->bv8) R31_6:bv64 64; - var R29_7:bv64 := load21_1:bv64; - var load22_1:bv64 := load le $stack:(bv64->bv8) bvadd(R31_6:bv64, 0x8:bv64) 64; - var R30_7:bv64 := load22_1:bv64; - var R31_7:bv64 := bvadd(R31_6:bv64, 0x20:bv64); - goto (%main_basil_return_1); + var R0_24:bv64 := 0x0:bv64; + var load21_1:bv64 := load le $stack:(bv64->bv8) R31_6:bv64 64; + var R29_7:bv64 := load21_1:bv64; + var load22_1:bv64 := load le $stack:(bv64->bv8) bvadd(R31_6:bv64, 0x8:bv64) 64; + var R30_7:bv64 := load22_1:bv64; + var R31_7:bv64 := bvadd(R31_6:bv64, 0x20:bv64); + goto (%main_basil_return_1); ]; block %main_basil_return_1 [ goto (%returns); ]; block %returns [ - (var CF_out:bv1 := CF_7:bv1, var NF_out:bv1 := NF_7:bv1, - var R0_out:bv64 := R0_24:bv64, var R1_out:bv64 := R1_6:bv64, - var R29_out:bv64 := R29_7:bv64, var R30_out:bv64 := R30_7:bv64, - var R31_out:bv64 := R31_7:bv64, var VF_out:bv1 := VF_7:bv1, - var ZF_out:bv1 := ZF_11:bv1); - return; + (var CF_out:bv1 := CF_7:bv1, var NF_out:bv1 := NF_7:bv1, + var R0_out:bv64 := R0_24:bv64, var R1_out:bv64 := R1_6:bv64, + var R29_out:bv64 := R29_7:bv64, var R30_out:bv64 := R30_7:bv64, + var R31_out:bv64 := R31_7:bv64, var VF_out:bv1 := VF_7:bv1, + var ZF_out:bv1 := ZF_11:bv1); + return; ] ]; proc @puts_1584(CF_in:bv1, NF_in:bv1, R0_in:bv64, R1_in:bv64, R29_in:bv64, @@ -318,14 +314,14 @@ Run on basic irreducible loop example $ diff after.il after_reparsed.il 18,21c18,21 < modifies $mem:(bv64->bv8), $stack:(bv64->bv8), $CF:bv1, $NF:bv1, $R0:bv64, - < $R1:bv64, $R29:bv64, $R30:bv64, $R31:bv64, $VF:bv1, $ZF:bv1; + < $R1:bv64, $R29:bv64, $R30:bv64, $R31:bv64, $VF:bv1, $ZF:bv1 < captures $mem:(bv64->bv8), $stack:(bv64->bv8), $CF:bv1, $NF:bv1, $R0:bv64, - < $R1:bv64, $R29:bv64, $R30:bv64, $R31:bv64, $VF:bv1, $ZF:bv1; + < $R1:bv64, $R29:bv64, $R30:bv64, $R31:bv64, $VF:bv1, $ZF:bv1 --- > modifies $stack:(bv64->bv8), $CF:bv1, $NF:bv1, $R0:bv64, $R1:bv64, $R29:bv64, - > $R30:bv64, $R31:bv64, $VF:bv1, $ZF:bv1, $mem:(bv64->bv8); + > $R30:bv64, $R31:bv64, $VF:bv1, $ZF:bv1, $mem:(bv64->bv8) > captures $stack:(bv64->bv8), $CF:bv1, $NF:bv1, $R0:bv64, $R1:bv64, $R29:bv64, - > $R30:bv64, $R31:bv64, $VF:bv1, $ZF:bv1, $mem:(bv64->bv8); + > $R30:bv64, $R31:bv64, $VF:bv1, $ZF:bv1, $mem:(bv64->bv8) [1] The interpreter should give the same output for both @@ -350,21 +346,19 @@ Multiple loops dependencies of loops etc are handled correctly > proc @main(R0_in:bv64) -> (R0_out:bv64) { } 7a7 > block %inputs [ var R0:bv64 := R0_in:bv64; goto (%e); ]; - 9,12c9,19 + 9,12c9,17 < block %e1 [ $R0:bv64 := 0x1:bv64; goto (%e2); ]; < block %e2 [ goto (%e4,%e1); ]; < block %e3 [ $R0:bv64 := 0x3:bv64; goto (%e4,%e1); ]; < block %e4 [ return; ] --- > block %e1 [ var R0_2:bv64 := 0x1:bv64; goto (%e2); ]; - > block %e2 [ - > (var R0_3:bv64 := phi(%e1 -> R0_2:bv64, %e -> R0:bv64)); - > goto (%e4,%e1); + > block %e2 ( var R0_3:bv64 := phi(%e1 -> R0_2:bv64, %e -> R0:bv64) ) [ + > goto (%e4,%e1); > ]; > block %e3 [ var R0_1:bv64 := 0x3:bv64; goto (%e4,%e1); ]; - > block %e4 [ - > (var R0_4:bv64 := phi(%e2 -> R0_3:bv64, %e3 -> R0_1:bv64, %e2 -> R0_3:bv64)); - > goto (%returns); - > ]; + > block %e4 ( + > var R0_4:bv64 := phi(%e2 -> R0_3:bv64, %e3 -> R0_1:bv64, %e2 -> R0_3:bv64) + > ) [ goto (%returns); ]; > block %returns [ var R0_out:bv64 := R0_4:bv64; return; ] [1] diff --git a/test/cram/expr_smt.t b/test/cram/expr_smt.t index ef552625..f257ff1d 100644 --- a/test/cram/expr_smt.t +++ b/test/cram/expr_smt.t @@ -8,73 +8,73 @@ 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), + < $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), --- - > $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:bv64)), 0xffffffff00000000:bv64), [1] diff --git a/test/cram/memassign.t b/test/cram/memassign.t index 60372a01..577261dc 100644 --- a/test/cram/memassign.t +++ b/test/cram/memassign.t @@ -1,10 +1,10 @@ $ dune exec bincaml -- dump-il memassign.il --proc '@main_4196164' | grep Global --before-context 1 --after-context 1 .returnBlock = "main_return" } - modifies $Global_4325420_4325424:bv32; - captures $Global_4325420_4325424:bv32; + modifies $Global_4325420_4325424:bv32 + captures $Global_4325420_4325424:bv32 -- block %main_entry [ - $Global_4325420_4325424:bv32 := store 0x2a:bv32; - goto (%main_return); + $Global_4325420_4325424:bv32 := store 0x2a:bv32; + goto (%main_return); diff --git a/test/cram/roundtrip.t b/test/cram/roundtrip.t index 8f080cb0..dc4a8888 100644 --- a/test/cram/roundtrip.t +++ b/test/cram/roundtrip.t @@ -6,14 +6,14 @@ The serialise -> parse serialise loop should be idempotent $ diff before.il after.il 15,18c15,18 < modifies $mem:(bv64->bv8), $stack:(bv64->bv8), $CF:bv1, $NF:bv1, $R0:bv64, - < $R1:bv64, $R29:bv64, $R30:bv64, $R31:bv64, $VF:bv1, $ZF:bv1; + < $R1:bv64, $R29:bv64, $R30:bv64, $R31:bv64, $VF:bv1, $ZF:bv1 < captures $mem:(bv64->bv8), $stack:(bv64->bv8), $CF:bv1, $NF:bv1, $R0:bv64, - < $R1:bv64, $R29:bv64, $R30:bv64, $R31:bv64, $VF:bv1, $ZF:bv1; + < $R1:bv64, $R29:bv64, $R30:bv64, $R31:bv64, $VF:bv1, $ZF:bv1 --- > modifies $stack:(bv64->bv8), $CF:bv1, $NF:bv1, $R0:bv64, $R1:bv64, $R29:bv64, - > $R30:bv64, $R31:bv64, $VF:bv1, $ZF:bv1, $mem:(bv64->bv8); + > $R30:bv64, $R31:bv64, $VF:bv1, $ZF:bv1, $mem:(bv64->bv8) > captures $stack:(bv64->bv8), $CF:bv1, $NF:bv1, $R0:bv64, $R1:bv64, $R29:bv64, - > $R30:bv64, $R31:bv64, $VF:bv1, $ZF:bv1, $mem:(bv64->bv8); + > $R30:bv64, $R31:bv64, $VF:bv1, $ZF:bv1, $mem:(bv64->bv8) 121c121 < block %main_basil_return_1 [ nop; return; ] --- @@ -22,11 +22,11 @@ The serialise -> parse serialise loop should be idempotent $ diff before2.il after2.il 7,8c7,8 - < modifies $mem:(bv64->bv8), $stack:(bv64->bv8); - < captures $mem:(bv64->bv8), $stack:(bv64->bv8); + < modifies $mem:(bv64->bv8), $stack:(bv64->bv8) + < captures $mem:(bv64->bv8), $stack:(bv64->bv8) --- - > modifies $stack:(bv64->bv8), $mem:(bv64->bv8); - > captures $stack:(bv64->bv8), $mem:(bv64->bv8); + > modifies $stack:(bv64->bv8), $mem:(bv64->bv8) + > captures $stack:(bv64->bv8), $mem:(bv64->bv8) [1] Memassign repr diff --git a/test/lang/interp.ml b/test/lang/interp.ml index ec6241ae..5920d463 100644 --- a/test/lang/interp.ml +++ b/test/lang/interp.ml @@ -21,8 +21,7 @@ let%expect_test "fold_block" = let st, _ = Lang.Interp.run_prog prog in print_endline (Lang.Interp.IState.show st); (); - [%expect - {| + [%expect {| PC= test::Return Stack diff --git a/test/lang/stmt.ml b/test/lang/stmt.ml index 0ce035f6..7d989d59 100644 --- a/test/lang/stmt.ml +++ b/test/lang/stmt.ml @@ -48,8 +48,7 @@ let%expect_test "fold_block" = () block; print_endline (Block.to_string block); (); - [%expect - {| + [%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, @@ -59,11 +58,11 @@ let%expect_test "fold_block" = var load46_1:bv32 := load le $mem:(bv64->bv8) 0x42002c:bv64 32 var R0_10:bv64 := zero_extend(32, load46_1:bv32) [ - $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; - load46_1:bv32 := load le $mem:(bv64->bv8) 0x42002c:bv64 32; - R0_10:bv64 := zero_extend(32, load46_1:bv32); + $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; + load46_1:bv32 := load le $mem:(bv64->bv8) 0x42002c:bv64 32; + R0_10:bv64 := zero_extend(32, load46_1:bv32); ] |}] diff --git a/tree-sitter/dune b/tree-sitter/dune new file mode 100644 index 00000000..ca13dd0c --- /dev/null +++ b/tree-sitter/dune @@ -0,0 +1,27 @@ +; checks tree-sitter is valid and unambiguous + +(rule + (deps grammar.js) + (alias runtest) + (enabled_if %{bin-available:tree-sitter}) + (action + (run tree-sitter generate grammar.js))) + +; check that grammar.js is up to date. +; requires `bnfc-treesitter` from pac-nix. + +(rule + (alias runtest) + (deps %{project_root}/lib/fe/BasilIR.cf) + (enabled_if %{bin-available:bnfc}) + (action + (progn + (copy %{deps} basilir.cf) + (run + bnfc + --tree-sitter + --tree-sitter-word + LocalIdent + basilir.cf + --makefile) + (diff? grammar.js tree-sitter-basilir/grammar.js)))) diff --git a/tree-sitter/grammar.js b/tree-sitter/grammar.js index 0a2a71e7..710c6b85 100644 --- a/tree-sitter/grammar.js +++ b/tree-sitter/grammar.js @@ -4,8 +4,8 @@ module.exports = grammar({ name: "basilir", extras: $ =>[ /\s/, - /\/\/.*\n/, - /\/\*[^*]*\*([^\*\/][^*]*\*|\*)*\//, + $.token_CommentSingle, + $.token_CommentMulti, ], word: $ => $.token_LocalIdent, rules: { @@ -33,33 +33,47 @@ module.exports = grammar({ // (:). [BlockIdent] ::= BlockIdent "," [BlockIdent] ; seq($.token_BlockIdent, ",", optional($.list_token_BlockIdent)) ), - Semicolons: $ => + LambdaSep: $ => choice( - // Semicolons_Empty. Semicolons ::= ; + // LambdaSep1. LambdaSep ::= "->" ; + "->", + // LambdaSep2. LambdaSep ::= "::" ; + "::" + ), + VarModifiers: $ => + choice( + // Shared. VarModifiers ::= "shared" ; + "shared", + // Observable. VarModifiers ::= "observable" ; + "observable" + ), + list_VarModifiers: $ => + choice( + // []. [VarModifiers] ::= ; choice(), - // Semicolons_Some. Semicolons ::= Semicolons ";" ; - seq(optional($.Semicolons), ";") + // (:). [VarModifiers] ::= VarModifiers [VarModifiers] ; + seq($.VarModifiers, optional($.list_VarModifiers)) ), Decl: $ => choice( - // Decl_Axiom. Decl ::= "axiom" AttribSet Expr ; - seq("axiom", optional($.AttribSet), $.Expr), - // Decl_SharedMem. Decl ::= "memory" "shared" GlobalIdent ":" Type ; - seq("memory", "shared", $.token_GlobalIdent, ":", $.Type), - // Decl_UnsharedMem. Decl ::= "memory" GlobalIdent ":" Type ; - seq("memory", $.token_GlobalIdent, ":", $.Type), - // Decl_Var. Decl ::= "var" GlobalIdent ":" Type ; - seq("var", $.token_GlobalIdent, ":", $.Type), - // Decl_UninterpFun. Decl ::= "declare-fun" AttribSet GlobalIdent ":" "(" [Type] ")" "->" Type ; - seq("declare-fun", optional($.AttribSet), $.token_GlobalIdent, ":", "(", optional($.list_Type), ")", "->", $.Type), - // Decl_Fun. Decl ::= "define-fun" AttribSet GlobalIdent "(" [Params] ")" "->" Type "=" Expr ; - seq("define-fun", optional($.AttribSet), $.token_GlobalIdent, "(", optional($.list_Params), ")", "->", $.Type, "=", $.Expr), + // Decl_Axiom. Decl ::= "axiom" GlobalIdent AttribSet Expr ; + seq("axiom", $.token_GlobalIdent, optional($.AttribSet), $.Expr), + // Decl_Mem. Decl ::= "memory" [VarModifiers] GlobalIdent ":" Type VarSpec ; + seq("memory", optional($.list_VarModifiers), $.token_GlobalIdent, ":", $.Type, optional($.VarSpec)), + // Decl_Var. Decl ::= "var" [VarModifiers] GlobalIdent ":" Type VarSpec ; + seq("var", optional($.list_VarModifiers), $.token_GlobalIdent, ":", $.Type, optional($.VarSpec)), + // Decl_UninterpFun. Decl ::= "val" GlobalIdent AttribSet ":" Type ; + seq("val", $.token_GlobalIdent, optional($.AttribSet), ":", $.Type), + // Decl_Fun. Decl ::= "let" GlobalIdent AttribSet ":" Type "=" Expr ; + seq("let", $.token_GlobalIdent, optional($.AttribSet), ":", $.Type, "=", $.Expr), + // Decl_FunNoType. Decl ::= "let" GlobalIdent AttribSet "=" Expr ; + seq("let", $.token_GlobalIdent, optional($.AttribSet), "=", $.Expr), // Decl_ProgEmpty. Decl ::= "prog" "entry" ProcIdent AttribSet ; seq("prog", "entry", $.token_ProcIdent, optional($.AttribSet)), - // Decl_ProgWithSpec. Decl ::= "prog" "entry" ProcIdent AttribSet BeginList [ProgSpec] EndList ; - seq("prog", "entry", $.token_ProcIdent, optional($.AttribSet), $.token_BeginList, optional($.list_ProgSpec), $.token_EndList), - // Decl_Proc. Decl ::= "proc" ProcIdent "(" [Params] ")" "->" "(" [Params] ")" AttribSet [FunSpec] ProcDef ; - seq("proc", $.token_ProcIdent, "(", optional($.list_Params), ")", "->", "(", optional($.list_Params), ")", optional($.AttribSet), optional($.list_FunSpec), optional($.ProcDef)) + // Decl_ProgWithSpec. Decl ::= "prog" "entry" ProcIdent AttribSet [ProgSpec] ; + seq("prog", "entry", $.token_ProcIdent, optional($.AttribSet), $.list_ProgSpec), + // Decl_Proc. Decl ::= "proc" ProcIdent OpenParen [Params] CloseParen "->" OpenParen [Params] CloseParen AttribSet [FunSpec] ProcDef ; + seq("proc", $.token_ProcIdent, $.token_OpenParen, optional($.list_Params), $.token_CloseParen, "->", $.token_OpenParen, optional($.list_Params), $.token_CloseParen, optional($.AttribSet), optional($.list_FunSpec), optional($.ProcDef)) ), list_Type: $ => choice( @@ -83,31 +97,29 @@ module.exports = grammar({ BoolType: $ => // BoolType1. BoolType ::= BOOLTYPE ; $.token_BOOLTYPE, - MapType: $ => - // MapType1. MapType ::= "(" Type "->" Type ")" ; - seq("(", $.Type, "->", $.Type, ")"), BVType: $ => // BVType1. BVType ::= BVTYPE ; $.token_BVTYPE, - Type: $ => + MapType: $ => + // MapType1. MapType ::= Type1 "->" Type ; + seq($.Type1, "->", $.Type), + Type1: $ => choice( - // TypeIntType. Type ::= IntType ; + // TypeIntType. Type1 ::= IntType ; $.IntType, - // TypeBoolType. Type ::= BoolType ; + // TypeBoolType. Type1 ::= BoolType ; $.BoolType, - // TypeMapType. Type ::= MapType ; - $.MapType, - // TypeBVType. Type ::= BVType ; - $.BVType + // TypeBVType. Type1 ::= BVType ; + $.BVType, + // TypeParen. Type1 ::= OpenParen Type CloseParen ; + seq($.token_OpenParen, $.Type, $.token_CloseParen) ), - list_Expr: $ => + Type: $ => choice( - // []. [Expr] ::= ; - choice(), - // (:[]). [Expr] ::= Expr ; - $.Expr, - // (:). [Expr] ::= Expr "," [Expr] ; - seq($.Expr, ",", optional($.list_Expr)) + // TypeMapType. Type ::= MapType ; + $.MapType, + // _. Type ::= Type1 ; + $.Type1 ), IntVal: $ => choice( @@ -135,18 +147,22 @@ module.exports = grammar({ "nop", // Stmt_SingleAssign. Stmt ::= Assignment ; $.Assignment, - // Stmt_MultiAssign. Stmt ::= "(" [Assignment] ")" ; - seq("(", $.list_Assignment, ")"), - // Stmt_Load. Stmt ::= LVar ":=" "load" Endian GlobalIdent Expr IntVal ; - seq($.LVar, ":=", "load", $.Endian, $.token_GlobalIdent, $.Expr, $.IntVal), - // Stmt_Store. Stmt ::= "store" Endian GlobalIdent Expr Expr IntVal ; - seq("store", $.Endian, $.token_GlobalIdent, $.Expr, $.Expr, $.IntVal), + // Stmt_MemAssign. Stmt ::= LVar "mem:=" Expr ; + seq($.LVar, "mem:=", $.Expr), + // Stmt_ScalarStore. Stmt ::= LVar ":=" "store" Expr ; + seq($.LVar, ":=", "store", $.Expr), + // Stmt_ScalarLoad. Stmt ::= LVar ":=" "load" Var ; + seq($.LVar, ":=", "load", $.Var), + // Stmt_MultiAssign. Stmt ::= OpenParen [Assignment] CloseParen ; + seq($.token_OpenParen, $.list_Assignment, $.token_CloseParen), // Stmt_Load_Var. Stmt ::= LVar ":=" "load" Endian Var Expr IntVal ; seq($.LVar, ":=", "load", $.Endian, $.Var, $.Expr, $.IntVal), - // Stmt_Store_Var. Stmt ::= LVar ":=" "store" Endian Var Expr Expr IntVal ; - seq($.LVar, ":=", "store", $.Endian, $.Var, $.Expr, $.Expr, $.IntVal), - // Stmt_DirectCall. Stmt ::= LVars "call" ProcIdent "(" CallParams ")" ; - seq(optional($.LVars), "call", $.token_ProcIdent, "(", optional($.CallParams), ")"), + // Stmt_Store_Var. Stmt ::= LVar ":=" "store" Endian Var Expr2 Expr IntVal ; + seq($.LVar, ":=", "store", $.Endian, $.Var, $.Expr2, $.Expr, $.IntVal), + // Stmt_Store. Stmt ::= "store" Endian GlobalIdent Expr2 Expr IntVal ; + seq("store", $.Endian, $.token_GlobalIdent, $.Expr2, $.Expr, $.IntVal), + // Stmt_DirectCall. Stmt ::= LVars "call" ProcIdent OpenParen CallParams CloseParen ; + seq(optional($.LVars), "call", $.token_ProcIdent, $.token_OpenParen, optional($.CallParams), $.token_CloseParen), // Stmt_IndirectCall. Stmt ::= "indirect" "call" Expr ; seq("indirect", "call", $.Expr), // Stmt_Assume. Stmt ::= "assume" Expr ; @@ -164,11 +180,12 @@ module.exports = grammar({ seq($.Assignment, ",", $.list_Assignment) ), LocalVar: $ => - // LocalVar1. LocalVar ::= LocalIdent ":" Type ; - seq($.token_LocalIdent, ":", $.Type), - GlobalVar: $ => - // GlobalVar1. GlobalVar ::= GlobalIdent ":" Type ; - seq($.token_GlobalIdent, ":", $.Type), + choice( + // LocalTyped. LocalVar ::= LocalIdent ":" Type1 ; + seq($.token_LocalIdent, ":", $.Type1), + // LocalUntyped. LocalVar ::= LocalIdent ; + $.token_LocalIdent + ), list_LocalVar: $ => choice( // (:[]). [LocalVar] ::= LocalVar ; @@ -176,6 +193,22 @@ module.exports = grammar({ // (:). [LocalVar] ::= LocalVar "," [LocalVar] ; seq($.LocalVar, ",", $.list_LocalVar) ), + GlobalVar: $ => + choice( + // GlobalTyped. GlobalVar ::= GlobalIdent ":" Type1 ; + seq($.token_GlobalIdent, ":", $.Type1), + // GlobalUntyped. GlobalVar ::= GlobalIdent ; + $.token_GlobalIdent + ), + list_GlobalVar: $ => + choice( + // []. [GlobalVar] ::= ; + choice(), + // (:[]). [GlobalVar] ::= GlobalVar ; + $.GlobalVar, + // (:). [GlobalVar] ::= GlobalVar "," [GlobalVar] ; + seq($.GlobalVar, ",", optional($.list_GlobalVar)) + ), Var: $ => choice( // VarLocalVar. Var ::= LocalVar ; @@ -183,6 +216,29 @@ module.exports = grammar({ // VarGlobalVar. Var ::= GlobalVar ; $.GlobalVar ), + LocalVarParen: $ => + choice( + // LocalVarParenLocalVar. LocalVarParen ::= LocalVar ; + $.LocalVar, + // LocalVarParen1. LocalVarParen ::= OpenParen LocalIdent ":" Type CloseParen ; + seq($.token_OpenParen, $.token_LocalIdent, ":", $.Type, $.token_CloseParen) + ), + GlobalVarParen: $ => + choice( + // GlobalVarParenGlobalVar. GlobalVarParen ::= GlobalVar ; + $.GlobalVar, + // GlobalVarParen1. GlobalVarParen ::= OpenParen GlobalIdent ":" Type CloseParen ; + seq($.token_OpenParen, $.token_GlobalIdent, ":", $.Type, $.token_CloseParen) + ), + list_LocalVarParen: $ => + choice( + // []. [LocalVarParen] ::= ; + choice(), + // (:[]). [LocalVarParen] ::= LocalVarParen ; + $.LocalVarParen, + // (:). [LocalVarParen] ::= LocalVarParen "," [LocalVarParen] ; + seq($.LocalVarParen, ",", optional($.list_LocalVarParen)) + ), NamedCallReturn: $ => // NamedCallReturn1. NamedCallReturn ::= LVar "=" LocalIdent ; seq($.LVar, "=", $.token_LocalIdent), @@ -199,24 +255,22 @@ module.exports = grammar({ choice( // LVars_Empty. LVars ::= ; choice(), - // LVars_LocalList. LVars ::= "var" "(" [LocalVar] ")" ":=" ; - seq("var", "(", $.list_LocalVar, ")", ":="), - // LVars_List. LVars ::= "(" [LVar] ")" ":=" ; - seq("(", $.list_LVar, ")", ":="), - // NamedLVars_List. LVars ::= "(" [NamedCallReturn] ")" ":=" ; - seq("(", optional($.list_NamedCallReturn), ")", ":=") + // LVars_LocalList. LVars ::= "var" OpenParen [LocalVar] CloseParen ":=" ; + seq("var", $.token_OpenParen, $.list_LocalVar, $.token_CloseParen, ":="), + // LVars_List. LVars ::= OpenParen [LVar] CloseParen ":=" ; + seq($.token_OpenParen, $.list_LVar, $.token_CloseParen, ":="), + // NamedLVars_List. LVars ::= OpenParen [NamedCallReturn] CloseParen ":=" ; + seq($.token_OpenParen, optional($.list_NamedCallReturn), $.token_CloseParen, ":=") ), NamedCallArg: $ => // NamedCallArg1. NamedCallArg ::= LocalIdent "=" Expr ; seq($.token_LocalIdent, "=", $.Expr), list_NamedCallArg: $ => choice( - // []. [NamedCallArg] ::= ; - choice(), // (:[]). [NamedCallArg] ::= NamedCallArg ; $.NamedCallArg, // (:). [NamedCallArg] ::= NamedCallArg "," [NamedCallArg] ; - seq($.NamedCallArg, ",", optional($.list_NamedCallArg)) + seq($.NamedCallArg, ",", $.list_NamedCallArg) ), CallParams: $ => choice( @@ -227,12 +281,12 @@ module.exports = grammar({ ), Jump: $ => choice( - // Jump_GoTo. Jump ::= "goto" "(" [BlockIdent] ")" ; - seq("goto", "(", optional($.list_token_BlockIdent), ")"), + // Jump_GoTo. Jump ::= "goto" OpenParen [BlockIdent] CloseParen ; + seq("goto", $.token_OpenParen, optional($.list_token_BlockIdent), $.token_CloseParen), // Jump_Unreachable. Jump ::= "unreachable" ; "unreachable", - // Jump_Return. Jump ::= "return" "(" [Expr] ")" ; - seq("return", "(", optional($.list_Expr), ")"), + // Jump_Return. Jump ::= "return" OpenParen [Expr] CloseParen ; + seq("return", $.token_OpenParen, optional($.list_Expr), $.token_CloseParen), // Jump_ProcReturn. Jump ::= "return" ; "return" ), @@ -285,8 +339,8 @@ module.exports = grammar({ seq($.PhiExpr, ",", optional($.list_PhiExpr)) ), PhiAssign: $ => - // PhiAssign1. PhiAssign ::= LVar ":=" "phi" "(" [PhiExpr] ")" ; - seq($.LVar, ":=", "phi", "(", optional($.list_PhiExpr), ")"), + // PhiAssign1. PhiAssign ::= LVar ":=" "phi" OpenParen [PhiExpr] CloseParen ; + seq($.LVar, ":=", "phi", $.token_OpenParen, optional($.list_PhiExpr), $.token_CloseParen), list_PhiAssign: $ => choice( // []. [PhiAssign] ::= ; @@ -300,8 +354,8 @@ module.exports = grammar({ choice( // Block_NoPhi. Block ::= "block" BlockIdent AttribSet BeginList [StmtWithAttrib] JumpWithAttrib ";" EndList ; seq("block", $.token_BlockIdent, optional($.AttribSet), $.token_BeginList, optional($.list_StmtWithAttrib), $.JumpWithAttrib, ";", $.token_EndList), - // Block_Phi. Block ::= "block" BlockIdent AttribSet BeginList "(" [PhiAssign] ")" ";" [StmtWithAttrib] JumpWithAttrib ";" EndList ; - seq("block", $.token_BlockIdent, optional($.AttribSet), $.token_BeginList, "(", optional($.list_PhiAssign), ")", ";", optional($.list_StmtWithAttrib), $.JumpWithAttrib, ";", $.token_EndList) + // Block_Phi. Block ::= "block" BlockIdent AttribSet OpenParen [PhiAssign] CloseParen BeginList [StmtWithAttrib] JumpWithAttrib ";" EndList ; + seq("block", $.token_BlockIdent, optional($.AttribSet), $.token_OpenParen, optional($.list_PhiAssign), $.token_CloseParen, $.token_BeginList, optional($.list_StmtWithAttrib), $.JumpWithAttrib, ";", $.token_EndList) ), AttrKeyValue: $ => // AttrKeyValue1. AttrKeyValue ::= BIdent "=" Attr ; @@ -337,8 +391,8 @@ module.exports = grammar({ seq($.token_BeginRec, optional($.list_AttrKeyValue), $.token_EndRec), // Attr_List. Attr ::= BeginList [Attr] EndList ; seq($.token_BeginList, optional($.list_Attr), $.token_EndList), - // Attr_Lit. Attr ::= Value ; - $.Value, + // Attr_Expr. Attr ::= Expr ; + $.Expr, // Attr_Str. Attr ::= Str ; $.token_Str ), @@ -365,40 +419,71 @@ module.exports = grammar({ // Value_False. Value ::= "false" ; "false" ), + list_Expr: $ => + choice( + // []. [Expr] ::= ; + choice(), + // (:[]). [Expr] ::= Expr ; + $.Expr, + // (:). [Expr] ::= Expr "," [Expr] ; + seq($.Expr, ",", optional($.list_Expr)) + ), Expr: $ => choice( - // Expr_Literal. Expr ::= Value ; + // _. Expr ::= Expr1 ; + $.Expr1, + // Expr_Forall. Expr ::= "forall" AttribSet LambdaDef ; + seq("forall", optional($.AttribSet), $.LambdaDef), + // Expr_Exists. Expr ::= "exists" AttribSet LambdaDef ; + seq("exists", optional($.AttribSet), $.LambdaDef), + // Expr_Lambda. Expr ::= "fun" AttribSet LambdaDef ; + seq("fun", optional($.AttribSet), $.LambdaDef) + ), + Expr1: $ => + choice( + // _. Expr1 ::= Expr2 ; + $.Expr2, + // Expr_FunctionOp. Expr1 ::= Expr1 OpenParen [Expr] CloseParen ; + seq($.Expr1, $.token_OpenParen, optional($.list_Expr), $.token_CloseParen) + ), + Expr2: $ => + choice( + // Expr_Literal. Expr2 ::= Value ; $.Value, - // Expr_Local. Expr ::= LocalVar ; + // Expr_Local. Expr2 ::= LocalVar ; $.LocalVar, - // Expr_Global. Expr ::= GlobalVar ; + // Expr_Global. Expr2 ::= GlobalVar ; $.GlobalVar, - // Expr_Forall. Expr ::= "forall" LambdaDef ; - seq("forall", $.LambdaDef), - // Expr_Exists. Expr ::= "exists" LambdaDef ; - seq("exists", $.LambdaDef), - // Expr_Old. Expr ::= "old" "(" Expr ")" ; - seq("old", "(", $.Expr, ")"), - // Expr_FunctionOp. Expr ::= GlobalIdent "(" [Expr] ")" ; - seq($.token_GlobalIdent, "(", optional($.list_Expr), ")"), - // Expr_Binary. Expr ::= BinOp "(" Expr "," Expr ")" ; - seq($.BinOp, "(", $.Expr, ",", $.Expr, ")"), - // Expr_Assoc. Expr ::= BoolBinOp "(" [Expr] ")" ; - seq($.BoolBinOp, "(", optional($.list_Expr), ")"), - // Expr_Unary. Expr ::= UnOp "(" Expr ")" ; - seq($.UnOp, "(", $.Expr, ")"), - // Expr_ZeroExtend. Expr ::= "zero_extend" "(" IntVal "," Expr ")" ; - seq("zero_extend", "(", $.IntVal, ",", $.Expr, ")"), - // Expr_SignExtend. Expr ::= "sign_extend" "(" IntVal "," Expr ")" ; - seq("sign_extend", "(", $.IntVal, ",", $.Expr, ")"), - // Expr_Extract. Expr ::= "extract" "(" IntVal "," IntVal "," Expr ")" ; - seq("extract", "(", $.IntVal, ",", $.IntVal, ",", $.Expr, ")"), - // Expr_Concat. Expr ::= "bvconcat" "(" [Expr] ")" ; - seq("bvconcat", "(", optional($.list_Expr), ")") + // Expr_Old. Expr2 ::= "old" OpenParen Expr CloseParen ; + seq("old", $.token_OpenParen, $.Expr, $.token_CloseParen), + // Expr_Binary. Expr2 ::= BinOp OpenParen Expr "," Expr CloseParen ; + seq($.BinOp, $.token_OpenParen, $.Expr, ",", $.Expr, $.token_CloseParen), + // Expr_Assoc. Expr2 ::= BoolBinOp OpenParen [Expr] CloseParen ; + seq($.BoolBinOp, $.token_OpenParen, optional($.list_Expr), $.token_CloseParen), + // Expr_Unary. Expr2 ::= UnOp OpenParen Expr CloseParen ; + seq($.UnOp, $.token_OpenParen, $.Expr, $.token_CloseParen), + // Expr_LoadBe. Expr2 ::= "load_be" OpenParen IntVal "," Expr "," Expr CloseParen ; + seq("load_be", $.token_OpenParen, $.IntVal, ",", $.Expr, ",", $.Expr, $.token_CloseParen), + // Expr_LoadLe. Expr2 ::= "load_le" OpenParen IntVal "," Expr "," Expr CloseParen ; + seq("load_le", $.token_OpenParen, $.IntVal, ",", $.Expr, ",", $.Expr, $.token_CloseParen), + // Expr_ZeroExtend. Expr2 ::= "zero_extend" OpenParen IntVal "," Expr CloseParen ; + seq("zero_extend", $.token_OpenParen, $.IntVal, ",", $.Expr, $.token_CloseParen), + // Expr_SignExtend. Expr2 ::= "sign_extend" OpenParen IntVal "," Expr CloseParen ; + seq("sign_extend", $.token_OpenParen, $.IntVal, ",", $.Expr, $.token_CloseParen), + // Expr_Extract. Expr2 ::= "extract" OpenParen IntVal "," IntVal "," Expr CloseParen ; + 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_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) ), LambdaDef: $ => - // LambdaDef1. LambdaDef ::= "(" [LocalVar] ")" LambdaSep Expr ; - seq("(", $.list_LocalVar, ")", $.token_LambdaSep, $.Expr), + // LambdaDef1. LambdaDef ::= [LocalVarParen] LambdaSep Expr ; + seq(optional($.list_LocalVarParen), $.LambdaSep, $.Expr), BinOp: $ => choice( // BinOpBVBinOp. BinOp ::= BVBinOp ; @@ -421,7 +506,27 @@ module.exports = grammar({ // UnOp_intneg. UnOp ::= "intneg" ; "intneg", // UnOp_booltobv1. UnOp ::= "booltobv1" ; - "booltobv1" + "booltobv1", + // UnOp_gamma. UnOp ::= "gamma" ; + "gamma", + // UnOp_classification. UnOp ::= "classification" ; + "classification" + ), + Case: $ => + choice( + // CaseCase. Case ::= Expr "->" Expr ; + seq($.Expr, "->", $.Expr), + // CaseDefault. Case ::= "_" "->" Expr ; + seq("_", "->", $.Expr) + ), + list_Case: $ => + choice( + // []. [Case] ::= ; + choice(), + // (:[]). [Case] ::= Case ; + $.Case, + // (:). [Case] ::= Case "|" [Case] ; + seq($.Case, "|", optional($.list_Case)) ), EqOp: $ => choice( @@ -542,35 +647,64 @@ module.exports = grammar({ // EnsureTok_ensures. EnsureTok ::= "ensures" ; "ensures" ), + RelyTok: $ => + choice( + // RelyTok_rely. RelyTok ::= "rely" ; + "rely", + // RelyTok_relies. RelyTok ::= "relies" ; + "relies" + ), + GuarTok: $ => + choice( + // GuarTok_guarantee. GuarTok ::= "guarantee" ; + "guarantee", + // GuarTok_guarantees. GuarTok ::= "guarantees" ; + "guarantees" + ), FunSpec: $ => choice( // FunSpec_Require. FunSpec ::= RequireTok Expr ; seq($.RequireTok, $.Expr), // FunSpec_Ensure. FunSpec ::= EnsureTok Expr ; seq($.EnsureTok, $.Expr), + // FunSpec_Rely. FunSpec ::= RelyTok Expr ; + seq($.RelyTok, $.Expr), + // FunSpec_Guar. FunSpec ::= GuarTok Expr ; + seq($.GuarTok, $.Expr), + // FunSpec_Captures. FunSpec ::= "captures" [GlobalVar] ; + seq("captures", optional($.list_GlobalVar)), + // FunSpec_Modifies. FunSpec ::= "modifies" [GlobalVar] ; + seq("modifies", optional($.list_GlobalVar)), // FunSpec_Invariant. FunSpec ::= "invariant" BlockIdent Expr ; seq("invariant", $.token_BlockIdent, $.Expr) ), + VarSpec: $ => + choice( + // VarSpec_Classification. VarSpec ::= "classification" Expr ; + seq("classification", $.Expr), + // VarSpec_Empty. VarSpec ::= ; + choice() + ), ProgSpec: $ => choice( - // ProgSpec_Rely. ProgSpec ::= "rely" Expr ; - seq("rely", $.Expr), - // ProgSpec_Guarantee. ProgSpec ::= "guarantee" Expr ; - seq("guarantee", $.Expr) + // ProgSpec_Rely. ProgSpec ::= RelyTok Expr ; + seq($.RelyTok, $.Expr), + // ProgSpec_Guarantee. ProgSpec ::= GuarTok Expr ; + seq($.GuarTok, $.Expr) ), list_FunSpec: $ => choice( // []. [FunSpec] ::= ; choice(), - // (:). [FunSpec] ::= FunSpec ";" [FunSpec] ; - seq($.FunSpec, ";", optional($.list_FunSpec)) + // (:). [FunSpec] ::= FunSpec [FunSpec] ; + seq($.FunSpec, optional($.list_FunSpec)) ), list_ProgSpec: $ => choice( - // []. [ProgSpec] ::= ; - choice(), - // (:). [ProgSpec] ::= ProgSpec ";" [ProgSpec] ; - seq($.ProgSpec, ";", optional($.list_ProgSpec)) + // (:[]). [ProgSpec] ::= ProgSpec ; + $.ProgSpec, + // (:). [ProgSpec] ::= ProgSpec [ProgSpec] ; + seq($.ProgSpec, $.list_ProgSpec) ), token_BVTYPE: $ => /bv\d+/, @@ -588,6 +722,10 @@ module.exports = grammar({ /%([#\$\._]|(\d|[a-zA-Z]))+/, token_ProcIdent: $ => /@([#\$\._]|(\d|[a-zA-Z]))+/, + token_OpenParen: $ => + /\(/, + token_CloseParen: $ => + /\)/, token_BeginList: $ => /\[/, token_EndList: $ => @@ -596,13 +734,15 @@ module.exports = grammar({ /\{/, token_EndRec: $ => /\}/, - token_LambdaSep: $ => - /::|->/, token_Str: $ => /"([^"\\]|\\["\\fnrt])*"/, token_IntegerHex: $ => /0x([abcdef]|\d)+/, token_IntegerDec: $ => /\d+/, + token_CommentSingle: $ => + /\/\/.*\n/, + token_CommentMulti: $ => + /\/\*[^*]*\*([^\*\/][^*]*\*|\*)*\//, }, }); diff --git a/tree-sitter/queries/highlights.scm b/tree-sitter/queries/highlights.scm index 67dc0492..27df3d72 100644 --- a/tree-sitter/queries/highlights.scm +++ b/tree-sitter/queries/highlights.scm @@ -6,8 +6,6 @@ "unreachable" @keyword.return "return" @keyword.return -["ensures" "ensure" "requires" "require"] @keyword - "call" @keyword.function "indirect" @keyword.function @@ -21,13 +19,33 @@ "assume" @keyword "var" @keyword "memory" @keyword -"shared" @keyword +"shared" @keyword.modifier +[ "rely" + "relies" + "guarantee" + "guarantee" + "require" + "requires" + "ensures" + "ensure" + "captures" + "modifies" + "classification" + "invariant" ] @keyword +[ "forall" + "exists" + "fun" + "old" ] @keyword.operator + +[ "match" + "with" + "cases" ] @keyword.conditional -(IntVal) @constant -(token_IntegerHex) @constant -(token_IntegerDec) @constant -"true" @constant -"false" @constant +(IntVal) @number +(token_IntegerHex) @number +(token_IntegerDec) @number +"true" @constant.builtin +"false" @constant.builtin (Type) @type (token_BVTYPE) @type.builtin @@ -52,6 +70,9 @@ (UnOp) @function.builtin (EqOp) @function.builtin +"load_be" @function.builtin +"load_le" @function.builtin + "boolnot" @function.builtin "intneg" @function.builtin "booltobv1" @function.builtin @@ -107,14 +128,17 @@ (token_EndList) (token_BeginRec) (token_EndRec) + (token_OpenParen) + (token_CloseParen) ] @punctuation.bracket [ ";" "," ] @punctuation.delimiter -[ ":" "=" ":=" ] @punctuation -[ "(" ")" - (token_BeginRec) +[ ":" "=" ":=" "::" ] @punctuation +[ (token_BeginRec) (token_EndRec) (token_BeginList) (token_EndList) ] @punctuation.bracket (token_Str) @string +(token_CommentMulti) @comment +(token_CommentSingle) @comment