From 65ab86a0e3df080ca9a1c37631904d8d02c07596 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Tue, 25 Oct 2016 17:26:50 +0200
Subject: SplitLong: propagate constants through "longofint"

This can make a big difference in which optimizations are triggered later.
Constants were already propagated by "longofintu".
---
 backend/SplitLong.vp | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

(limited to 'backend/SplitLong.vp')

diff --git a/backend/SplitLong.vp b/backend/SplitLong.vp
index 60d8e4c4..cbf7fa30 100644
--- a/backend/SplitLong.vp
+++ b/backend/SplitLong.vp
@@ -112,8 +112,11 @@ Definition is_longconst_zero (e: expr) :=
 
 Definition intoflong (e: expr) := lowlong e.
 
-Definition longofint (e: expr) :=
-  Elet e (makelong (shrimm (Eletvar O) (Int.repr 31)) (Eletvar O)).
+Nondetfunction longofint (e: expr) :=
+  match e with
+  | Eop (Ointconst n) Enil => longconst (Int64.repr (Int.signed n))
+  | _ => Elet e (makelong (shrimm (Eletvar O) (Int.repr 31)) (Eletvar O))
+  end.
 
 Definition longofintu (e: expr) :=
   makelong (Eop (Ointconst Int.zero) Enil) e.
-- 
cgit