From c2319ee007eba06f92837e1e370dfa5e58b06b82 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 10 Mar 2020 14:57:24 +0100 Subject: oper2 --- backend/CSE3analysis.v | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) (limited to 'backend/CSE3analysis.v') diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v index 41fa67f6..456898cf 100644 --- a/backend/CSE3analysis.v +++ b/backend/CSE3analysis.v @@ -216,6 +216,16 @@ Section OPERATIONS. else None end end. -End OPERATIONS. + + Definition oper2 (no : node) (dst : reg) (op: sym_op)(args : list reg) + (rel : RELATION.t) := + let rel' := kill_reg dst rel in + match eq_find no {| eq_lhs := dst; + eq_op := op; + eq_args:= args |} with + | Some id => PSet.add id rel' + | None => rel' + end. + End OPERATIONS. Definition totoro := RELATION.lub. -- cgit