From e16b34d9fc1aa7854759787fd52ad59c964c2d4b Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Wed, 3 Jul 2019 11:06:07 +0200
Subject: Perform constant propagation for known built-in functions

When an external function is a known built-in function and it is
applied to compile-time integer or FP constants, we can use
the known semantics of the builtin to compute the result
at compile-time.
---
 backend/ValueDomain.v | 44 ++++++++++++++++++++++++++++++++++++++++++--
 1 file changed, 42 insertions(+), 2 deletions(-)

(limited to 'backend/ValueDomain.v')

diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v
index f6afa836..fd3bd5ae 100644
--- a/backend/ValueDomain.v
+++ b/backend/ValueDomain.v
@@ -13,7 +13,7 @@
 Require Import FunInd.
 Require Import Zwf Coqlib Maps Zbits Integers Floats Lattice.
 Require Import Compopts AST.
-Require Import Values Memory Globalenvs Events.
+Require Import Values Memory Globalenvs Builtins Events.
 Require Import Registers RTL.
 
 (** The abstract domains for value analysis *)
@@ -3038,7 +3038,47 @@ Proof with (auto using provenance_monotone with va).
 - destruct (zlt n 16)...
 Qed.
 
-(** Abstracting memory blocks *)
+(** Analysis of known builtin functions.  All we have is a dynamic semantics
+  as a function [list val -> option val], but we can still perform 
+  some constant propagation. *)
+
+Definition val_of_aval (a: aval) : val :=
+  match a with
+  | I n => Vint n
+  | L n => Vlong n
+  | F f => Vfloat f
+  | FS f => Vsingle f
+  | _ => Vundef
+  end.
+
+Definition aval_of_val (v: val) : option aval :=
+  match v with
+  | Vint n => Some (I n)
+  | Vlong n => Some (L n)
+  | Vfloat f => Some (F f)
+  | Vsingle f => Some (FS f)
+  | _ => None
+  end.
+
+Lemma val_of_aval_sound:
+  forall v a, vmatch v a -> Val.lessdef (val_of_aval a) v.
+Proof.
+  destruct 1; simpl; auto.
+Qed.
+
+Corollary list_val_of_aval_sound:
+  forall vl al, list_forall2 vmatch vl al -> Val.lessdef_list (map val_of_aval al) vl.
+Proof.
+  induction 1; simpl; constructor; auto using val_of_aval_sound.
+Qed.
+
+Lemma aval_of_val_sound:
+  forall v a, aval_of_val v = Some a -> vmatch v a. 
+Proof.
+  intros v a E; destruct v; simpl in E; inv E; constructor.
+Qed.
+
+(** * Abstracting memory blocks *)
 
 Inductive acontent : Type :=
  | ACval (chunk: memory_chunk) (av: aval).
-- 
cgit