From 2dca62f38463b0ebce24fff50666c846df50488e Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 3 Apr 2019 20:19:24 +0200 Subject: attempts at generating builtins, start --- backend/Selection.v | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) (limited to 'backend/Selection.v') diff --git a/backend/Selection.v b/backend/Selection.v index 05a06abf..27c5bd10 100644 --- a/backend/Selection.v +++ b/backend/Selection.v @@ -267,6 +267,11 @@ Definition sel_switch_long := (fun arg ofs => subl arg (longconst (Int64.repr ofs))) lowlong. +Definition sel_builtin optid ef args := + Sbuiltin (sel_builtin_res optid) ef + (sel_builtin_args args + (Machregs.builtin_constraints ef)). + (** Conversion from Cminor statements to Cminorsel statements. *) Fixpoint sel_stmt (s: Cminor.stmt) : res stmt := @@ -278,9 +283,7 @@ Fixpoint sel_stmt (s: Cminor.stmt) : res stmt := OK (match classify_call fn with | Call_default => Scall optid sg (inl _ (sel_expr fn)) (sel_exprlist args) | Call_imm id => Scall optid sg (inr _ id) (sel_exprlist args) - | Call_builtin ef => Sbuiltin (sel_builtin_res optid) ef - (sel_builtin_args args - (Machregs.builtin_constraints ef)) + | Call_builtin ef => sel_builtin optid ef args end) | Cminor.Sbuiltin optid ef args => OK (Sbuiltin (sel_builtin_res optid) ef -- cgit From 93fd5df1bff8b22b3513a07a765b0a72f1505243 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 3 Apr 2019 20:26:32 +0200 Subject: some more on builtins --- backend/Selection.v | 17 ++++++++++++++--- 1 file changed, 14 insertions(+), 3 deletions(-) (limited to 'backend/Selection.v') diff --git a/backend/Selection.v b/backend/Selection.v index 27c5bd10..e63cbce3 100644 --- a/backend/Selection.v +++ b/backend/Selection.v @@ -268,9 +268,20 @@ Definition sel_switch_long := lowlong. Definition sel_builtin optid ef args := - Sbuiltin (sel_builtin_res optid) ef - (sel_builtin_args args - (Machregs.builtin_constraints ef)). + match ef with + | EF_builtin name sign => + (if String.string_dec name "__builtin_ternary_uint" + then Sbuiltin (sel_builtin_res optid) ef + (sel_builtin_args args + (Machregs.builtin_constraints ef)) + else Sbuiltin (sel_builtin_res optid) ef + (sel_builtin_args args + (Machregs.builtin_constraints ef))) + | _ => + Sbuiltin (sel_builtin_res optid) ef + (sel_builtin_args args + (Machregs.builtin_constraints ef)) + end. (** Conversion from Cminor statements to Cminorsel statements. *) -- cgit From c8cd3d017890a250f32463b6dca6571d181a3c22 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 3 Apr 2019 20:35:04 +0200 Subject: selection of builtin.. progress... --- backend/Selection.v | 27 ++++++++++++++------------- 1 file changed, 14 insertions(+), 13 deletions(-) (limited to 'backend/Selection.v') diff --git a/backend/Selection.v b/backend/Selection.v index e63cbce3..a87578ba 100644 --- a/backend/Selection.v +++ b/backend/Selection.v @@ -267,20 +267,21 @@ Definition sel_switch_long := (fun arg ofs => subl arg (longconst (Int64.repr ofs))) lowlong. +Definition sel_builtin_default optid ef args := + OK (Sbuiltin (sel_builtin_res optid) ef + (sel_builtin_args args + (Machregs.builtin_constraints ef))). + Definition sel_builtin optid ef args := match ef with | EF_builtin name sign => (if String.string_dec name "__builtin_ternary_uint" - then Sbuiltin (sel_builtin_res optid) ef - (sel_builtin_args args - (Machregs.builtin_constraints ef)) - else Sbuiltin (sel_builtin_res optid) ef - (sel_builtin_args args - (Machregs.builtin_constraints ef))) - | _ => - Sbuiltin (sel_builtin_res optid) ef - (sel_builtin_args args - (Machregs.builtin_constraints ef)) + then (match optid with + | None => OK Sskip + | Some id => Error (msg "Selection: ternary uint") + end) + else sel_builtin_default optid ef args) + | _ => sel_builtin_default optid ef args end. (** Conversion from Cminor statements to Cminorsel statements. *) @@ -291,9 +292,9 @@ Fixpoint sel_stmt (s: Cminor.stmt) : res stmt := | Cminor.Sassign id e => OK (Sassign id (sel_expr e)) | Cminor.Sstore chunk addr rhs => OK (store chunk (sel_expr addr) (sel_expr rhs)) | Cminor.Scall optid sg fn args => - OK (match classify_call fn with - | Call_default => Scall optid sg (inl _ (sel_expr fn)) (sel_exprlist args) - | Call_imm id => Scall optid sg (inr _ id) (sel_exprlist args) + (match classify_call fn with + | Call_default => OK (Scall optid sg (inl _ (sel_expr fn)) (sel_exprlist args)) + | Call_imm id => OK (Scall optid sg (inr _ id) (sel_exprlist args)) | Call_builtin ef => sel_builtin optid ef args end) | Cminor.Sbuiltin optid ef args => -- cgit From 015a05d8661504388ea1109f740eb16220311f93 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 3 Apr 2019 20:44:16 +0200 Subject: begin implementing ternary builtin --- backend/Selection.v | 17 +++++++++++++---- 1 file changed, 13 insertions(+), 4 deletions(-) (limited to 'backend/Selection.v') diff --git a/backend/Selection.v b/backend/Selection.v index a87578ba..5e45dde3 100644 --- a/backend/Selection.v +++ b/backend/Selection.v @@ -276,10 +276,19 @@ Definition sel_builtin optid ef args := match ef with | EF_builtin name sign => (if String.string_dec name "__builtin_ternary_uint" - then (match optid with - | None => OK Sskip - | Some id => Error (msg "Selection: ternary uint") - end) + then + match optid with + | None => OK Sskip + | Some id => + match args with + | a1::a2::a3::nil => + OK (Sassign id (Eop Oselect + ((sel_expr a3)::: + (sel_expr a2)::: + (sel_expr a1):::Enil))) + | _ => Error (msg "__builtin_ternary_uint: arguments") + end + end else sel_builtin_default optid ef args) | _ => sel_builtin_default optid ef args end. -- cgit From 4032ed3192424a23dbb0a4f3bd2a539b22625168 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 3 Apr 2019 21:00:46 +0200 Subject: problem in ValueAOp --- backend/Selection.v | 18 +++++++++++++++++- 1 file changed, 17 insertions(+), 1 deletion(-) (limited to 'backend/Selection.v') diff --git a/backend/Selection.v b/backend/Selection.v index 5e45dde3..5cfa3dcb 100644 --- a/backend/Selection.v +++ b/backend/Selection.v @@ -286,10 +286,26 @@ Definition sel_builtin optid ef args := ((sel_expr a3)::: (sel_expr a2)::: (sel_expr a1):::Enil))) + | _ => Error (msg "__builtin_ternary_ulong: arguments") + end + end + else + if String.string_dec name "__builtin_ternary_ulong" + then + match optid with + | None => OK Sskip + | Some id => + match args with + | a1::a2::a3::nil => + OK (Sassign id (Eop Oselectl + ((sel_expr a3)::: + (sel_expr a2)::: + (sel_expr a1):::Enil))) | _ => Error (msg "__builtin_ternary_uint: arguments") end end - else sel_builtin_default optid ef args) + else + sel_builtin_default optid ef args) | _ => sel_builtin_default optid ef args end. -- cgit