From 255cee09b71255051c2b40eae0c88bffce1f6f32 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sat, 20 Apr 2013 07:54:52 +0000
Subject: Big merge of the newregalloc-int64 branch.  Lots of changes in two
 directions: 1- new register allocator (+ live range splitting,
 spilling&reloading, etc)    based on a posteriori validation using the
 Rideau-Leroy algorithm 2- support for 64-bit integer arithmetic (type "long
 long").

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2200 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 backend/CminorSel.v | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

(limited to 'backend/CminorSel.v')

diff --git a/backend/CminorSel.v b/backend/CminorSel.v
index b5a0d39b..3538dda8 100644
--- a/backend/CminorSel.v
+++ b/backend/CminorSel.v
@@ -43,6 +43,8 @@ Inductive expr : Type :=
   | Econdition : condition -> exprlist -> expr -> expr -> expr
   | Elet : expr -> expr -> expr
   | Eletvar : nat -> expr
+  | Ebuiltin : external_function -> exprlist -> expr
+  | Eexternal : ident -> signature -> exprlist -> expr
 
 with exprlist : Type :=
   | Enil: exprlist
@@ -171,6 +173,17 @@ Inductive eval_expr: letenv -> expr -> val -> Prop :=
   | eval_Eletvar: forall le n v,
       nth_error le n = Some v ->
       eval_expr le (Eletvar n) v
+  | eval_Ebuiltin: forall le ef al vl v,
+      eval_exprlist le al vl ->
+      external_call ef ge vl m E0 v m ->
+      eval_expr le (Ebuiltin ef al) v
+  | eval_Eexternal: forall le id sg al b ef vl v,
+      Genv.find_symbol ge id = Some b ->
+      Genv.find_funct_ptr ge b = Some (External ef) ->
+      ef_sig ef = sg ->
+      eval_exprlist le al vl ->
+      external_call ef ge vl m E0 v m ->
+      eval_expr le (Eexternal id sg al) v
 
 with eval_exprlist: letenv -> exprlist -> list val -> Prop :=
   | eval_Enil: forall le,
@@ -388,6 +401,8 @@ Fixpoint lift_expr (p: nat) (a: expr) {struct a}: expr :=
   | Elet b c => Elet (lift_expr p b) (lift_expr (S p) c)
   | Eletvar n =>
       if le_gt_dec p n then Eletvar (S n) else Eletvar n
+  | Ebuiltin ef bl => Ebuiltin ef (lift_exprlist p bl)
+  | Eexternal id sg bl => Eexternal id sg (lift_exprlist p bl)
   end
 
 with lift_exprlist (p: nat) (a: exprlist) {struct a}: exprlist :=
-- 
cgit