From 6cd8264024bbf4a0096550e2ea17e9c0b9b29787 Mon Sep 17 00:00:00 2001 From: Halogen Truong Date: Tue, 27 Aug 2024 21:38:22 +1000 Subject: [PATCH 1/5] Give local loads precedence above comparisons, rename stw and associated keywords, add local memory ops to concrete examples --- .../translation/from_pancake32ProgScript.sml | 4 +- .../translation/from_pancake64ProgScript.sml | 4 +- pancake/parser/panConcreteExamplesScript.sml | 11 +++++ pancake/parser/panLexerScript.sml | 13 +++--- pancake/parser/panPEGScript.sml | 42 ++++++++++--------- pancake/parser/panPtreeConversionScript.sml | 4 +- 6 files changed, 46 insertions(+), 32 deletions(-) diff --git a/compiler/bootstrap/translation/from_pancake32ProgScript.sml b/compiler/bootstrap/translation/from_pancake32ProgScript.sml index 718bcd769b..39069db4f3 100644 --- a/compiler/bootstrap/translation/from_pancake32ProgScript.sml +++ b/compiler/bootstrap/translation/from_pancake32ProgScript.sml @@ -500,9 +500,9 @@ Definition conv_Exp_alt_def: else if isNT nodeNT LoadByteNT then case args of [] => NONE - | [t] => OPTION_MAP LoadByte (conv_Exp_alt t) + | [t] => OPTION_MAP ELoadByte (conv_Exp_alt t) | t::v6::v7 => NONE - else if isNT nodeNT LoadNT then + else if isNT nodeNT ELoadNT then case args of [] => NONE | [t1] => NONE diff --git a/compiler/bootstrap/translation/from_pancake64ProgScript.sml b/compiler/bootstrap/translation/from_pancake64ProgScript.sml index d6f2dc5bb6..0bab431f27 100644 --- a/compiler/bootstrap/translation/from_pancake64ProgScript.sml +++ b/compiler/bootstrap/translation/from_pancake64ProgScript.sml @@ -502,12 +502,12 @@ Definition conv_Exp_alt_def: case args of [t] => OPTION_MAP (λe. Cmp Equal (Const 0w) e) (conv_Exp_alt t) | _ => NONE - else if isNT nodeNT LoadByteNT then + else if isNT nodeNT ELoadByteNT then case args of [] => NONE | [t] => OPTION_MAP LoadByte (conv_Exp_alt t) | t::v6::v7 => NONE - else if isNT nodeNT LoadNT then + else if isNT nodeNT ELoadNT then case args of [] => NONE | [t1] => NONE diff --git a/pancake/parser/panConcreteExamplesScript.sml b/pancake/parser/panConcreteExamplesScript.sml index 69cf4c6cb3..3db24bd8ac 100644 --- a/pancake/parser/panConcreteExamplesScript.sml +++ b/pancake/parser/panConcreteExamplesScript.sml @@ -339,6 +339,17 @@ val struct_argument_parse_tree = parse_tree_pancake $ struct_arguments; val struct_argument_parse = parse_pancake $ struct_arguments; +val locmem_ex = ‘ + fun test_locmem() { + var v = 12; + st 1000, 1 + 1; // store 1 + 1 (ie 2) at local memory address 1000 + st8 1000 + 4, v; // store byte from variable v (12) to local memory address 1004 + v = lds 1 1000 + 8; // load word from local address 1008 and assign to variable v + v = ld8 1000 + 4 * 3; // load byte from local address 1012 and assign to variable v + }’; + +val locmem_ex_parse = check_success $ parse_pancake locmem_ex; + val shmem_ex = ‘ fun test_shmem() { var v = 12; diff --git a/pancake/parser/panLexerScript.sml b/pancake/parser/panLexerScript.sml index dd5c19e400..1e24d0b7ea 100644 --- a/pancake/parser/panLexerScript.sml +++ b/pancake/parser/panLexerScript.sml @@ -18,9 +18,9 @@ open mlstringTheory; val _ = new_theory "panLexer"; Datatype: - keyword = SkipK | StoreK | StoreBK | Store32K | IfK | ElseK | WhileK + keyword = SkipK | StK | StwK | St8K | St32K | IfK | ElseK | WhileK | BrK | ContK | RaiseK | RetK | TicK | VarK | WithK | HandleK | BiwK - | LdsK | LdbK | LdwK | Ld32K | BaseK | InK | FunK | ExportK | TrueK | FalseK + | LdsK | Ld8K | LdwK | Ld32K | BaseK | InK | FunK | ExportK | TrueK | FalseK End Datatype: @@ -114,9 +114,10 @@ End Definition get_keyword_def: get_keyword s = if s = "skip" then (KeywordT SkipK) else - if s = "stw" then (KeywordT StoreK) else - if s = "st8" then (KeywordT StoreBK) else - if s = "st32" then (KeywordT Store32K) else + if s = "st" then (KeywordT StK) else + if s = "stw" then (KeywordT StwK) else + if s = "st8" then (KeywordT St8K) else + if s = "st32" then (KeywordT St32K) else if s = "if" then (KeywordT IfK) else if s = "else" then (KeywordT ElseK) else if s = "while" then (KeywordT WhileK) else @@ -131,7 +132,7 @@ Definition get_keyword_def: if s = "handle" then (KeywordT HandleK) else if s = "lds" then (KeywordT LdsK) else if s = "ldw" then (KeywordT LdwK) else - if s = "ld8" then (KeywordT LdbK) else + if s = "ld8" then (KeywordT Ld8K) else if s = "ld32" then (KeywordT Ld32K) else if s = "@base" then (KeywordT BaseK) else if s = "@biw" then (KeywordT BiwK) else diff --git a/pancake/parser/panPEGScript.sml b/pancake/parser/panPEGScript.sml index 2a503ffbbe..fd9041aba3 100644 --- a/pancake/parser/panPEGScript.sml +++ b/pancake/parser/panPEGScript.sml @@ -21,10 +21,12 @@ Datatype: | DecCallNT | RetCallNT | ArgListNT | NotNT | ParamListNT - | EXorNT | EOrNT | EAndNT | EEqNT | ECmpNT + | EBoolAndNT | EEqNT | ECmpNT + | ELoadNT | ELoadByteNT + | EXorNT | EOrNT | EAndNT | EShiftNT | EAddNT | EMulNT - | EBaseNT | EBoolAndNT - | StructNT | LoadNT | LoadByteNT | LabelNT | FLabelNT + | EBaseNT + | StructNT | LabelNT | FLabelNT | ShapeNT | ShapeCombNT | EqOpsNT | CmpOpsNT | ShiftOpsNT | AddOpsNT | MulOpsNT | SharedLoadNT | SharedLoadByteNT | SharedLoad32NT @@ -182,10 +184,10 @@ Definition pancake_peg_def[nocompute]: (mksubtree DecNT)); (INL AssignNT, seql [keep_ident; consume_tok AssignT; mknt ExpNT] (mksubtree AssignNT)); - (INL StoreNT, seql [consume_kw StoreK; mknt ExpNT; + (INL StoreNT, seql [consume_kw StK; mknt ExpNT; consume_tok CommaT; mknt ExpNT] (mksubtree StoreNT)); - (INL StoreByteNT, seql [consume_kw StoreBK; mknt ExpNT; + (INL StoreByteNT, seql [consume_kw St8K; mknt ExpNT; consume_tok CommaT; mknt ExpNT] (mksubtree StoreByteNT)); (INL IfNT, seql [consume_kw IfK; mknt ExpNT; consume_tok LCurT; @@ -243,9 +245,15 @@ Definition pancake_peg_def[nocompute]: (INL EEqNT, seql [mknt ECmpNT; try (seql [mknt EqOpsNT; mknt ECmpNT] I)] (mksubtree EEqNT)); - (INL ECmpNT, seql [mknt EOrNT; - try (seql [mknt CmpOpsNT; mknt EOrNT] I)] + (INL ECmpNT, seql [mknt ELoadNT; + try (seql [mknt CmpOpsNT; mknt ELoadNT] I)] (mksubtree ECmpNT)); + (INL ELoadNT, choicel [seql [consume_kw LdsK; mknt ShapeNT; mknt ELoadByteNT] + (mksubtree ELoadNT); + mknt ELoadByteNT]); + (INL ELoadByteNT, choicel [seql [consume_kw Ld8K; mknt EOrNT] + (mksubtree ELoadByteNT); + mknt EOrNT]); (INL EOrNT, seql [mknt EXorNT; rpt (seql [keep_tok OrT; mknt EXorNT] I) FLAT] @@ -275,8 +283,7 @@ Definition pancake_peg_def[nocompute]: mknt NotNT; keep_kw TrueK; keep_kw FalseK; keep_int; keep_ident; mknt LabelNT; - mknt StructNT; mknt LoadNT; - mknt LoadByteNT; keep_kw BaseK; keep_kw BiwK; + mknt StructNT; keep_kw BaseK; keep_kw BiwK; ]; rpt (seql [consume_tok DotT; keep_nat] I) FLAT] @@ -290,10 +297,6 @@ Definition pancake_peg_def[nocompute]: (INL StructNT, seql [consume_tok LessT; mknt ArgListNT; consume_tok GreaterT] (mksubtree StructNT)); - (INL LoadNT, seql [consume_kw LdsK; mknt ShapeNT; mknt ExpNT] - (mksubtree LoadNT)); - (INL LoadByteNT, seql [consume_kw LdbK; mknt ExpNT] - (mksubtree LoadByteNT)); (INL ShapeNT, choicel [keep_int; seql [consume_tok LCurT; mknt ShapeCombNT; @@ -313,19 +316,19 @@ Definition pancake_peg_def[nocompute]: (INL SharedLoadNT,seql [consume_tok NotT; consume_kw LdwK; keep_ident; consume_tok CommaT; mknt ExpNT] (mksubtree SharedLoadNT)); - (INL SharedLoadByteNT,seql [consume_tok NotT; consume_kw LdbK; keep_ident; + (INL SharedLoadByteNT,seql [consume_tok NotT; consume_kw Ld8K; keep_ident; consume_tok CommaT; mknt ExpNT] (mksubtree SharedLoadByteNT)); (INL SharedLoad32NT,seql [consume_tok NotT; consume_kw Ld32K; keep_ident; consume_tok CommaT; mknt ExpNT] (mksubtree SharedLoad32NT)); - (INL SharedStoreNT,seql [consume_tok NotT; consume_kw StoreK; mknt ExpNT; + (INL SharedStoreNT,seql [consume_tok NotT; consume_kw StwK; mknt ExpNT; consume_tok CommaT; mknt ExpNT] (mksubtree SharedStoreNT)); - (INL SharedStoreByteNT,seql [consume_tok NotT; consume_kw StoreBK; mknt ExpNT; + (INL SharedStoreByteNT,seql [consume_tok NotT; consume_kw St8K; mknt ExpNT; consume_tok CommaT; mknt ExpNT] (mksubtree SharedStoreByteNT)); - (INL SharedStore32NT,seql [consume_tok NotT; consume_kw Store32K; mknt ExpNT; + (INL SharedStore32NT,seql [consume_tok NotT; consume_kw St32K; mknt ExpNT; consume_tok CommaT; mknt ExpNT] (mksubtree SharedStore32NT)); ] @@ -637,10 +640,9 @@ end val topo_nts = [“MulOpsNT”, “AddOpsNT”, “ShiftOpsNT”, “CmpOpsNT”, “EqOpsNT”, “ShapeNT”, - “ShapeCombNT”, “NotNT”, “LabelNT”, “FLabelNT”, “LoadByteNT”, - “LoadNT”, “StructNT”, + “ShapeCombNT”, “NotNT”, “LabelNT”, “FLabelNT”, “StructNT”, “EBaseNT”, “EMulNT”, “EAddNT”, “EShiftNT”, “EAndNT”, “EXorNT”, “EOrNT”, - “ECmpNT”, “EEqNT”, “EBoolAndNT”, + “ECmpNT”, “EEqNT”, “EBoolAndNT”, “ELoadNT”, “ELoadByteNT”, “ExpNT”, “ArgListNT”, “ReturnNT”, “RaiseNT”, “ExtCallNT”, “HandleNT”, “RetNT”, “RetCallNT”, “CallNT”, diff --git a/pancake/parser/panPtreeConversionScript.sml b/pancake/parser/panPtreeConversionScript.sml index 529f7fd522..d5d0eda2a3 100644 --- a/pancake/parser/panPtreeConversionScript.sml +++ b/pancake/parser/panPtreeConversionScript.sml @@ -274,11 +274,11 @@ Definition conv_Exp_def: case args of [t] => lift (Cmp Equal (Const 0w)) (conv_Exp t) | _ => NONE - else if isNT nodeNT LoadByteNT then + else if isNT nodeNT ELoadByteNT then case args of [t] => lift LoadByte (conv_Exp t) | _ => NONE - else if isNT nodeNT LoadNT then + else if isNT nodeNT ELoadNT then case args of [t1; t2] => do s <- conv_Shape t1; e <- conv_Exp t2; From ce0d51814f03c1853a7f275b72ff251fc8b42c05 Mon Sep 17 00:00:00 2001 From: Halogen Truong Date: Tue, 27 Aug 2024 23:12:21 +1000 Subject: [PATCH 2/5] Fix order of load PEG NTs --- pancake/parser/panPEGScript.sml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pancake/parser/panPEGScript.sml b/pancake/parser/panPEGScript.sml index fd9041aba3..860e38e392 100644 --- a/pancake/parser/panPEGScript.sml +++ b/pancake/parser/panPEGScript.sml @@ -642,7 +642,7 @@ val topo_nts = [“MulOpsNT”, “AddOpsNT”, “ShiftOpsNT”, “CmpOpsNT” “EqOpsNT”, “ShapeNT”, “ShapeCombNT”, “NotNT”, “LabelNT”, “FLabelNT”, “StructNT”, “EBaseNT”, “EMulNT”, “EAddNT”, “EShiftNT”, “EAndNT”, “EXorNT”, “EOrNT”, - “ECmpNT”, “EEqNT”, “EBoolAndNT”, “ELoadNT”, “ELoadByteNT”, + “ELoadNT”, “ELoadByteNT”, “ECmpNT”, “EEqNT”, “EBoolAndNT”, “ExpNT”, “ArgListNT”, “ReturnNT”, “RaiseNT”, “ExtCallNT”, “HandleNT”, “RetNT”, “RetCallNT”, “CallNT”, From 6b0dc7679f5e566a7915576fc5336035d1482ef6 Mon Sep 17 00:00:00 2001 From: Halogen Truong Date: Tue, 27 Aug 2024 23:13:56 +1000 Subject: [PATCH 3/5] Fix order for real this time --- pancake/parser/panPEGScript.sml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pancake/parser/panPEGScript.sml b/pancake/parser/panPEGScript.sml index 860e38e392..1d194426a3 100644 --- a/pancake/parser/panPEGScript.sml +++ b/pancake/parser/panPEGScript.sml @@ -642,7 +642,7 @@ val topo_nts = [“MulOpsNT”, “AddOpsNT”, “ShiftOpsNT”, “CmpOpsNT” “EqOpsNT”, “ShapeNT”, “ShapeCombNT”, “NotNT”, “LabelNT”, “FLabelNT”, “StructNT”, “EBaseNT”, “EMulNT”, “EAddNT”, “EShiftNT”, “EAndNT”, “EXorNT”, “EOrNT”, - “ELoadNT”, “ELoadByteNT”, “ECmpNT”, “EEqNT”, “EBoolAndNT”, + “ELoadByteNT”, “ELoadNT”, “ECmpNT”, “EEqNT”, “EBoolAndNT”, “ExpNT”, “ArgListNT”, “ReturnNT”, “RaiseNT”, “ExtCallNT”, “HandleNT”, “RetNT”, “RetCallNT”, “CallNT”, From 4f8e5714e6b515e367c495059f846916112b12e1 Mon Sep 17 00:00:00 2001 From: Halogen Truong Date: Wed, 28 Aug 2024 09:41:30 +1000 Subject: [PATCH 4/5] Fix translator typo --- compiler/bootstrap/translation/from_pancake32ProgScript.sml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/compiler/bootstrap/translation/from_pancake32ProgScript.sml b/compiler/bootstrap/translation/from_pancake32ProgScript.sml index 39069db4f3..337365ed47 100644 --- a/compiler/bootstrap/translation/from_pancake32ProgScript.sml +++ b/compiler/bootstrap/translation/from_pancake32ProgScript.sml @@ -497,10 +497,10 @@ Definition conv_Exp_alt_def: case args of [t] => OPTION_MAP (λe. Cmp Equal (Const 0w) e) (conv_Exp_alt t) | _ => NONE - else if isNT nodeNT LoadByteNT then + else if isNT nodeNT ELoadByteNT then case args of [] => NONE - | [t] => OPTION_MAP ELoadByte (conv_Exp_alt t) + | [t] => OPTION_MAP LoadByte (conv_Exp_alt t) | t::v6::v7 => NONE else if isNT nodeNT ELoadNT then case args of From 2752848f158e960d4faff4205c50d79fee206f44 Mon Sep 17 00:00:00 2001 From: Halogen Truong Date: Thu, 29 Aug 2024 00:58:56 +1000 Subject: [PATCH 5/5] Update stw mention in concrete examples --- pancake/parser/panConcreteExamplesScript.sml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pancake/parser/panConcreteExamplesScript.sml b/pancake/parser/panConcreteExamplesScript.sml index 3db24bd8ac..1f1b72e966 100644 --- a/pancake/parser/panConcreteExamplesScript.sml +++ b/pancake/parser/panConcreteExamplesScript.sml @@ -229,7 +229,7 @@ val ex9 = ‘ var c = @base + 16; var d = 1; @out_morefun(a,b,c,d); - stw @base, ic; + st @base, ic; return 0; }’;