Mercurial > urweb

annotate src/reduce_local.sml @ 1077:a3273bee05a9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Initial generalization of Especialize, with security bug known
author Adam Chlipala <adamc@hcoop.net>
date Tue, 15 Dec 2009 12:26:00 -0500
parents 0657e5adc938
children c316ca3c9ec6
rev   line source
adamc@482 1 (* Copyright (c) 2008, Adam Chlipala
adamc@482 2 * All rights reserved.
adamc@482 3 *
adamc@482 4 * Redistribution and use in source and binary forms, with or without
adamc@482 5 * modification, are permitted provided that the following conditions are met:
adamc@482 6 *
adamc@482 7 * - Redistributions of source code must retain the above copyright notice,
adamc@482 8 * this list of conditions and the following disclaimer.
adamc@482 9 * - Redistributions in binary form must reproduce the above copyright notice,
adamc@482 10 * this list of conditions and the following disclaimer in the documentation
adamc@482 11 * and/or other materials provided with the distribution.
adamc@482 12 * - The names of contributors may not be used to endorse or promote products
adamc@482 13 * derived from this software without specific prior written permission.
adamc@482 14 *
adamc@482 15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
adamc@482 16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
adamc@482 17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
adamc@482 18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
adamc@482 19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
adamc@482 20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
adamc@482 21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
adamc@482 22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
adamc@482 23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
adamc@482 24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
adamc@482 25 * POSSIBILITY OF SUCH DAMAGE.
adamc@482 26 *)
adamc@482 27
adamc@482 28 (* Simplify a Core program algebraically, without unfolding definitions *)
adamc@482 29
adamc@482 30 structure ReduceLocal :> REDUCE_LOCAL = struct
adamc@482 31
adamc@482 32 open Core
adamc@482 33
adamc@512 34 structure IM = IntBinaryMap
adamc@482 35
adamc@1062 36 fun multiLiftExpInExp n e =
adamc@1062 37 if n = 0 then
adamc@1062 38 e
adamc@1062 39 else
adamc@1062 40 multiLiftExpInExp (n - 1) (CoreEnv.liftExpInExp 0 e)
adamc@1062 41
adamc@512 42 datatype env_item =
adamc@512 43 Unknown
adamc@512 44 | Known of exp
adamc@482 45
adamc@512 46 | Lift of int
adamc@482 47
adamc@512 48 type env = env_item list
adamc@512 49
adamc@512 50 val deKnown = List.filter (fn Known _ => false
adamc@512 51 | _ => true)
adamc@512 52
adamc@1062 53 datatype result = Yes of env | No | Maybe
adamc@1062 54
adamc@1062 55 fun match (env, p : pat, e : exp) =
adamc@1062 56 let
adamc@1062 57 val baseline = length env
adamc@1062 58
adamc@1062 59 fun match (env, p, e) =
adamc@1062 60 case (#1 p, #1 e) of
adamc@1062 61 (PWild, _) => Yes env
adamc@1062 62 | (PVar (x, t), _) => Yes (Known (multiLiftExpInExp (length env - baseline) e) :: env)
adamc@1062 63
adamc@1062 64 | (PPrim p, EPrim p') =>
adamc@1062 65 if Prim.equal (p, p') then
adamc@1062 66 Yes env
adamc@1062 67 else
adamc@1062 68 No
adamc@1062 69
adamc@1062 70 | (PCon (_, PConVar n1, _, NONE), ECon (_, PConVar n2, _, NONE)) =>
adamc@1062 71 if n1 = n2 then
adamc@1062 72 Yes env
adamc@1062 73 else
adamc@1062 74 No
adamc@1062 75
adamc@1062 76 | (PCon (_, PConVar n1, _, SOME p), ECon (_, PConVar n2, _, SOME e)) =>
adamc@1062 77 if n1 = n2 then
adamc@1062 78 match (env, p, e)
adamc@1062 79 else
adamc@1062 80 No
adamc@1062 81
adamc@1062 82 | (PCon (_, PConFfi {mod = m1, con = con1, ...}, _, NONE),
adamc@1062 83 ECon (_, PConFfi {mod = m2, con = con2, ...}, _, NONE)) =>
adamc@1062 84 if m1 = m2 andalso con1 = con2 then
adamc@1062 85 Yes env
adamc@1062 86 else
adamc@1062 87 No
adamc@1062 88
adamc@1062 89 | (PCon (_, PConFfi {mod = m1, con = con1, ...}, _, SOME ep),
adamc@1062 90 ECon (_, PConFfi {mod = m2, con = con2, ...}, _, SOME e)) =>
adamc@1062 91 if m1 = m2 andalso con1 = con2 then
adamc@1062 92 match (env, p, e)
adamc@1062 93 else
adamc@1062 94 No
adamc@1062 95
adamc@1062 96 | (PRecord xps, ERecord xes) =>
adamc@1062 97 if List.exists (fn ((CName _, _), _, _) => false
adamc@1062 98 | _ => true) xes then
adamc@1062 99 Maybe
adamc@1062 100 else
adamc@1062 101 let
adamc@1062 102 fun consider (xps, env) =
adamc@1062 103 case xps of
adamc@1062 104 [] => Yes env
adamc@1062 105 | (x, p, _) :: rest =>
adamc@1062 106 case List.find (fn ((CName x', _), _, _) => x' = x
adamc@1062 107 | _ => false) xes of
adamc@1062 108 NONE => No
adamc@1062 109 | SOME (_, e, _) =>
adamc@1062 110 case match (env, p, e) of
adamc@1062 111 No => No
adamc@1062 112 | Maybe => Maybe
adamc@1062 113 | Yes env => consider (rest, env)
adamc@1062 114 in
adamc@1062 115 consider (xps, env)
adamc@1062 116 end
adamc@1062 117
adamc@1062 118 | _ => Maybe
adamc@1062 119 in
adamc@1062 120 match (env, p, e)
adamc@1062 121 end
adamc@1062 122
adamc@512 123 fun exp env (all as (e, loc)) =
adamc@512 124 case e of
adamc@512 125 EPrim _ => all
adamc@512 126 | ERel n =>
adamc@512 127 let
adamc@512 128 fun find (n', env, nudge, lift) =
adamc@512 129 case env of
adamc@642 130 [] => (ERel (n + nudge), loc)
adamc@512 131 | Lift lift' :: rest => find (n', rest, nudge + lift', lift + lift')
adamc@512 132 | Unknown :: rest =>
adamc@512 133 if n' = 0 then
adamc@512 134 (ERel (n + nudge), loc)
adamc@512 135 else
adamc@512 136 find (n' - 1, rest, nudge, lift + 1)
adamc@512 137 | Known e :: rest =>
adamc@512 138 if n' = 0 then
adamc@512 139 ((*print "SUBSTITUTING\n";*)
adamc@512 140 exp (Lift lift :: rest) e)
adamc@512 141 else
adamc@512 142 find (n' - 1, rest, nudge - 1, lift)
adamc@512 143 in
adamc@512 144 find (n, env, 0, 0)
adamc@512 145 end
adamc@512 146 | ENamed _ => all
adamc@512 147 | ECon (dk, pc, cs, eo) => (ECon (dk, pc, cs, Option.map (exp env) eo), loc)
adamc@512 148 | EFfi _ => all
adamc@512 149 | EFfiApp (m, f, es) => (EFfiApp (m, f, map (exp env) es), loc)
adamc@512 150
adamc@721 151 | EApp ((ECApp ((ECAbs (_, _, (EAbs (_, (CRel 0, _), _,
adamc@721 152 (ECon (dk, pc, [(CRel 0, loc)], SOME (ERel 0, _)), _)), _)), _),
adamc@721 153 t), _), e) =>
adamc@721 154 (ECon (dk, pc, [t], SOME (exp env e)), loc)
adamc@721 155
adamc@512 156 | EApp (e1, e2) =>
adamc@512 157 let
adamc@512 158 val e1 = exp env e1
adamc@512 159 val e2 = exp env e2
adamc@512 160 in
adamc@512 161 case #1 e1 of
adamc@512 162 EAbs (_, _, _, b) => exp (Known e2 :: deKnown env) b
adamc@512 163 | _ => (EApp (e1, e2), loc)
adamc@512 164 end
adamc@512 165
adamc@512 166 | EAbs (x, dom, ran, e) => (EAbs (x, dom, ran, exp (Unknown :: env) e), loc)
adamc@512 167
adamc@721 168 | ECApp ((ECAbs (_, _, (ECon (dk, pc, [(CRel 0, loc)], NONE), _)), _), t) =>
adamc@721 169 (ECon (dk, pc, [t], NONE), loc)
adamc@721 170
adamc@512 171 | ECApp (e, c) => (ECApp (exp env e, c), loc)
adamc@626 172 | ECAbs (x, k, e) => (ECAbs (x, k, exp env e), loc)
adamc@512 173
adamc@626 174 | EKApp (e, k) => (EKApp (exp env e, k), loc)
adamc@626 175 | EKAbs (x, e) => (EKAbs (x, exp env e), loc)
adamc@512 176
adamc@512 177 | ERecord xcs => (ERecord (map (fn (x, e, t) => (x, exp env e, t)) xcs), loc)
adamc@512 178 | EField (e, c, others) =>
adamc@512 179 let
adamc@512 180 val e = exp env e
adamc@512 181
adamc@512 182 fun default () = (EField (e, c, others), loc)
adamc@512 183 in
adamc@512 184 case (#1 e, #1 c) of
adamc@512 185 (ERecord xcs, CName x) =>
adamc@512 186 (case List.find (fn ((CName x', _), _, _) => x' = x | _ => false) xcs of
adamc@512 187 NONE => default ()
adamc@512 188 | SOME (_, e, _) => e)
adamc@512 189 | _ => default ()
adamc@512 190 end
adamc@512 191
adamc@512 192 | EConcat (e1, c1, e2, c2) => (EConcat (exp env e1, c1, exp env e2, c2), loc)
adamc@512 193 | ECut (e, c, others) => (ECut (exp env e, c, others), loc)
adamc@512 194 | ECutMulti (e, c, others) => (ECutMulti (exp env e, c, others), loc)
adamc@512 195
adamc@512 196 | ECase (e, pes, others) =>
adamc@512 197 let
adamc@512 198 fun patBinds (p, _) =
adamc@512 199 case p of
adamc@512 200 PWild => 0
adamc@512 201 | PVar _ => 1
adamc@512 202 | PPrim _ => 0
adamc@512 203 | PCon (_, _, _, NONE) => 0
adamc@512 204 | PCon (_, _, _, SOME p) => patBinds p
adamc@512 205 | PRecord xpts => foldl (fn ((_, p, _), n) => n + patBinds p) 0 xpts
adamc@1062 206
adamc@1062 207 fun push () =
adamc@1062 208 (ECase (exp env e,
adamc@1062 209 map (fn (p, e) => (p,
adamc@1062 210 exp (List.tabulate (patBinds p,
adamc@1062 211 fn _ => Unknown) @ env) e))
adamc@1062 212 pes, others), loc)
adamc@1062 213
adamc@1062 214 fun search pes =
adamc@1062 215 case pes of
adamc@1062 216 [] => push ()
adamc@1062 217 | (p, body) :: pes =>
adamc@1062 218 case match (env, p, e) of
adamc@1062 219 No => search pes
adamc@1062 220 | Maybe => push ()
adamc@1062 221 | Yes env' => exp env' body
adamc@512 222 in
adamc@1062 223 search pes
adamc@512 224 end
adamc@512 225
adamc@512 226 | EWrite e => (EWrite (exp env e), loc)
adamc@512 227 | EClosure (n, es) => (EClosure (n, map (exp env) es), loc)
adamc@512 228
adamc@512 229 | ELet (x, t, e1, e2) => (ELet (x, t, exp env e1, exp (Unknown :: env) e2), loc)
adamc@512 230
adamc@1020 231 | EServerCall (n, es, t) => (EServerCall (n, map (exp env) es, t), loc)
adamc@607 232
adamc@512 233 fun reduce file =
adamc@482 234 let
adamc@512 235 fun doDecl (d as (_, loc)) =
adamc@512 236 case #1 d of
adamc@512 237 DCon _ => d
adamc@512 238 | DDatatype _ => d
adamc@512 239 | DVal (x, n, t, e, s) =>
adamc@512 240 let
adamc@512 241 val e = exp [] e
adamc@512 242 in
adamc@512 243 (DVal (x, n, t, e, s), loc)
adamc@512 244 end
adamc@512 245 | DValRec vis =>
adamc@512 246 (DValRec (map (fn (x, n, t, e, s) => (x, n, t, exp [] e, s)) vis), loc)
adamc@512 247 | DExport _ => d
adamc@512 248 | DTable _ => d
adamc@512 249 | DSequence _ => d
adamc@754 250 | DView _ => d
adamc@512 251 | DDatabase _ => d
adamc@512 252 | DCookie _ => d
adamc@718 253 | DStyle _ => d
adamc@1075 254 | DTask (e1, e2) => (DTask (exp [] e1, exp [] e2), loc)
adamc@482 255 in
adamc@512 256 map doDecl file
adamc@482 257 end
adamc@482 258
adamc@642 259 val reduceExp = exp []
adamc@642 260
adamc@482 261 end