adamc@1200: (* Copyright (c) 2010, Adam Chlipala
adamc@1200:  * All rights reserved.
adamc@1200:  *
adamc@1200:  * Redistribution and use in source and binary forms, with or without
adamc@1200:  * modification, are permitted provided that the following conditions are met:
adamc@1200:  *
adamc@1200:  * - Redistributions of source code must retain the above copyright notice,
adamc@1200:  *   this list of conditions and the following disclaimer.
adamc@1200:  * - Redistributions in binary form must reproduce the above copyright notice,
adamc@1200:  *   this list of conditions and the following disclaimer in the documentation
adamc@1200:  *   and/or other materials provided with the distribution.
adamc@1200:  * - The names of contributors may not be used to endorse or promote products
adamc@1200:  *   derived from this software without specific prior written permission.
adamc@1200:  *
adamc@1200:  * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
adamc@1200:  * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
adamc@1200:  * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
adamc@1200:  * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
adamc@1200:  * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR 
adamc@1200:  * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
adamc@1200:  * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
adamc@1200:  * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
adamc@1200:  * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
adamc@1200:  * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
adamc@1200:  * POSSIBILITY OF SUCH DAMAGE.
adamc@1200:  *)
adamc@1200: 
adamc@1200: structure Iflow :> IFLOW = struct
adamc@1200: 
adamc@1200: open Mono
adamc@1200: 
adamc@1200: structure SS = BinarySetFn(struct
adamc@1200:                            type ord_key = string
adamc@1200:                            val compare = String.compare
adamc@1200:                            end)
adamc@1200: 
adamc@1200: val writers = ["htmlifyInt_w",
adamc@1200:                "htmlifyFloat_w",
adamc@1200:                "htmlifyString_w",
adamc@1200:                "htmlifyBool_w",
adamc@1200:                "htmlifyTime_w",
adamc@1200:                "attrifyInt_w",
adamc@1200:                "attrifyFloat_w",
adamc@1200:                "attrifyString_w",
adamc@1200:                "attrifyChar_w",
adamc@1200:                "urlifyInt_w",
adamc@1200:                "urlifyFloat_w",
adamc@1200:                "urlifyString_w",
adamc@1200:                "urlifyBool_w"]
adamc@1200: 
adamc@1200: val writers = SS.addList (SS.empty, writers)
adamc@1200: 
adamc@1200: type lvar = int
adamc@1200: 
adamc@1200: datatype exp =
adamc@1200:          Const of Prim.t
adamc@1200:        | Var of int
adamc@1200:        | Lvar of lvar
adamc@1200:        | Func of string * exp list
adamc@1200:        | Recd of (string * exp) list
adamc@1200:        | Proj of exp * string
adamc@1200:        | Finish
adamc@1200: 
adamc@1200: datatype reln =
adamc@1200:          Sql of string
adamc@1200:        | Eq
adamc@1200: 
adamc@1200: datatype prop =
adamc@1200:          True
adamc@1200:        | False
adamc@1200:        | Unknown
adamc@1200:        | And of prop * prop
adamc@1200:        | Or of prop * prop
adamc@1200:        | Reln of reln * exp list
adamc@1200:        | Select of int * lvar * lvar * prop * exp
adamc@1200: 
adamc@1200: local
adamc@1200:     val count = ref 0
adamc@1200: in
adamc@1200: fun newLvar () =
adamc@1200:     let
adamc@1200:         val n = !count
adamc@1200:     in
adamc@1200:         count := n + 1;
adamc@1200:         n
adamc@1200:     end
adamc@1200: end
adamc@1200: 
adamc@1200: fun subExp (v, lv) =
adamc@1200:     let
adamc@1200:         fun sub e =
adamc@1200:             case e of
adamc@1200:                 Const _ => e
adamc@1200:               | Var v' => if v' = v then Lvar lv else e
adamc@1200:               | Lvar _ => e
adamc@1200:               | Func (f, es) => Func (f, map sub es)
adamc@1200:               | Recd xes => Recd (map (fn (x, e) => (x, sub e)) xes)
adamc@1200:               | Proj (e, s) => Proj (sub e, s)
adamc@1200:               | Finish => Finish
adamc@1200:     in
adamc@1200:         sub
adamc@1200:     end
adamc@1200: 
adamc@1200: fun subProp (v, lv) =
adamc@1200:     let
adamc@1200:         fun sub p =
adamc@1200:             case p of
adamc@1200:                 True => p
adamc@1200:               | False => p
adamc@1200:               | Unknown => p
adamc@1200:               | And (p1, p2) => And (sub p1, sub p2)
adamc@1200:               | Or (p1, p2) => Or (sub p1, sub p2)
adamc@1200:               | Reln (r, es) => Reln (r, map (subExp (v, lv)) es)
adamc@1200:               | Select (v1, lv1, lv2, p, e) => Select (v1, lv1, lv2, sub p, subExp (v, lv) e)
adamc@1200:     in
adamc@1200:         sub
adamc@1200:     end
adamc@1200: 
adamc@1200: fun eq' (e1, e2) =
adamc@1200:     case (e1, e2) of
adamc@1200:         (Const p1, Const p2) => Prim.equal (p1, p2)
adamc@1200:       | (Var n1, Var n2) => n1 = n2
adamc@1200:       | (Lvar n1, Lvar n2) => n1 = n2
adamc@1200:       | (Func (f1, es1), Func (f2, es2)) => f1 = f2 andalso ListPair.allEq eq' (es1, es2)
adamc@1200:       | (Recd xes1, Recd xes2) => ListPair.allEq (fn ((x1, e1), (x2, e2)) => x1 = x2 andalso eq' (e1, e2)) (xes1, xes2)
adamc@1200:       | (Proj (e1, s1), Proj (e2, s2)) => eq' (e1, e2) andalso s1 = s2
adamc@1200:       | (Finish, Finish) => true
adamc@1200:       | _ => false
adamc@1200: 
adamc@1200: fun isKnown e =
adamc@1200:     case e of
adamc@1200:         Const _ => true
adamc@1200:       | Func (_, es) => List.all isKnown es
adamc@1200:       | Recd xes => List.all (isKnown o #2) xes
adamc@1200:       | Proj (e, _) => isKnown e
adamc@1200:       | _ => false
adamc@1200: 
adamc@1200: fun isFinish e =
adamc@1200:     case e of
adamc@1200:         Finish => true
adamc@1200:       | _ => false
adamc@1200: 
adamc@1200: fun simplify e =
adamc@1200:     case e of
adamc@1200:         Const _ => e
adamc@1200:       | Var _ => e
adamc@1200:       | Lvar _ => e
adamc@1200:       | Func (f, es) =>
adamc@1200:         let
adamc@1200:             val es = map simplify es
adamc@1200:         in
adamc@1200:             if List.exists isFinish es then
adamc@1200:                 Finish
adamc@1200:             else
adamc@1200:                 Func (f, es)
adamc@1200:         end
adamc@1200:       | Recd xes =>
adamc@1200:         let
adamc@1200:             val xes = map (fn (x, e) => (x, simplify e)) xes
adamc@1200:         in
adamc@1200:             if List.exists (isFinish o #2) xes then
adamc@1200:                 Finish
adamc@1200:             else
adamc@1200:                 Recd xes
adamc@1200:         end
adamc@1200:       | Proj (e, s) =>
adamc@1200:         (case simplify e of
adamc@1200:              Recd xes =>
adamc@1200:              getOpt (ListUtil.search (fn (x, e') => if x = s then SOME e' else NONE) xes, Recd xes)
adamc@1200:            | e' =>
adamc@1200:              if isFinish e' then
adamc@1200:                  Finish
adamc@1200:              else
adamc@1200:                  Proj (e', s))
adamc@1200:       | Finish => Finish
adamc@1200: 
adamc@1200: fun eq (e1, e2) = eq' (simplify e1, simplify e2)
adamc@1200: 
adamc@1200: fun decomp or =
adamc@1200:     let
adamc@1200:         fun decomp p k =
adamc@1200:             case p of
adamc@1200:                 True => k []
adamc@1200:               | False => true
adamc@1200:               | Unknown => k []
adamc@1200:               | And (p1, p2) => 
adamc@1200:                 decomp p1 (fn ps1 =>
adamc@1200:                               decomp p2 (fn ps2 =>
adamc@1200:                                             k (ps1 @ ps2)))
adamc@1200:               | Or (p1, p2) =>
adamc@1200:                 or (decomp p1 k, fn () => decomp p2 k)
adamc@1200:               | Reln x => k [x]
adamc@1200:               | Select _ => k []
adamc@1200:     in
adamc@1200:         decomp
adamc@1200:     end
adamc@1200: 
adamc@1200: fun rimp ((r1 : reln, es1), (r2, es2)) =
adamc@1200:     r1 = r2 andalso ListPair.allEq eq (es1, es2)
adamc@1200: 
adamc@1200: fun imp (p1, p2) =
adamc@1200:     decomp (fn (e1, e2) => e1 andalso e2 ()) p1
adamc@1200:     (fn hyps =>
adamc@1200:         decomp (fn (e1, e2) => e1 orelse e2 ()) p2
adamc@1200:         (fn goals =>
adamc@1200:             List.all (fn r2 => List.exists (fn r1 => rimp (r1, r2)) hyps) goals))
adamc@1200: 
adamc@1200: fun patCon pc =
adamc@1200:     case pc of
adamc@1200:         PConVar n => "C" ^ Int.toString n
adamc@1200:       | PConFfi {mod = m, datatyp = d, con = c, ...} => m ^ "." ^ d ^ "." ^ c
adamc@1200: 
adamc@1200: exception Summaries of (string * exp * prop * (exp * prop) list) list
adamc@1200: 
adamc@1200: datatype chunk =
adamc@1200:          String of string
adamc@1200:        | Exp of Mono.exp
adamc@1200: 
adamc@1200: fun chunkify e =
adamc@1200:     case #1 e of
adamc@1200:         EPrim (Prim.String s) => [String s]
adamc@1200:       | EStrcat (e1, e2) => chunkify e1 @ chunkify e2
adamc@1200:       | _ => [Exp e]
adamc@1200: 
adamc@1200: fun queryProp rv e =
adamc@1200:     let
adamc@1200:         fun query chs =
adamc@1200:             case chs of
adamc@1200:                 [] => raise Fail "Iflow: Empty query"
adamc@1200:               | Exp _ :: _ => Unknown
adamc@1200:               | String "" :: chs => query chs
adamc@1200:               | String s :: chs => True
adamc@1200:     in
adamc@1200:         query (chunkify e)
adamc@1200:     end
adamc@1200: 
adamc@1200: fun evalExp env (e : Mono.exp, st as (nv, p, sent)) =
adamc@1200:     let
adamc@1200:         fun default () =
adamc@1200:             (Var nv, (nv+1, p, sent))
adamc@1200: 
adamc@1200:         fun addSent (p, e, sent) =
adamc@1200:             if isKnown e then
adamc@1200:                 sent
adamc@1200:             else
adamc@1200:                 (e, p) :: sent
adamc@1200:     in
adamc@1200:         case #1 e of
adamc@1200:             EPrim p => (Const p, st)
adamc@1200:           | ERel n => (List.nth (env, n), st)
adamc@1200:           | ENamed _ => default ()
adamc@1200:           | ECon (_, pc, NONE) => (Func (patCon pc, []), st)
adamc@1200:           | ECon (_, pc, SOME e) =>
adamc@1200:             let
adamc@1200:                 val (e, st) = evalExp env (e, st)
adamc@1200:             in
adamc@1200:                 (Func (patCon pc, [e]), st)
adamc@1200:             end
adamc@1200:           | ENone _ => (Func ("None", []), st)
adamc@1200:           | ESome (_, e) =>
adamc@1200:             let
adamc@1200:                 val (e, st) = evalExp env (e, st)
adamc@1200:             in
adamc@1200:                 (Func ("Some", [e]), st)
adamc@1200:             end
adamc@1200:           | EFfi _ => default ()
adamc@1200:           | EFfiApp (m, s, es) =>
adamc@1200:             if m = "Basis" andalso SS.member (writers, s) then
adamc@1200:                 let
adamc@1200:                     val (es, st) = ListUtil.foldlMap (evalExp env) st es
adamc@1200:                 in
adamc@1200:                     (Func ("unit", []), (#1 st, p, foldl (fn (e, sent) => addSent (#2 st, e, sent)) sent es))
adamc@1200:                 end
adamc@1200:             else if Settings.isEffectful (m, s) andalso not (Settings.isBenignEffectful (m, s)) then
adamc@1200:                 default ()
adamc@1200:             else
adamc@1200:                 let
adamc@1200:                     val (es, st) = ListUtil.foldlMap (evalExp env) st es
adamc@1200:                 in
adamc@1200:                     (Func (m ^ "." ^ s, es), st)
adamc@1200:                 end
adamc@1200:           | EApp _ => default ()
adamc@1200:           | EAbs _ => default ()
adamc@1200:           | EUnop (s, e1) =>
adamc@1200:             let
adamc@1200:                 val (e1, st) = evalExp env (e1, st)
adamc@1200:             in
adamc@1200:                 (Func (s, [e1]), st)
adamc@1200:             end
adamc@1200:           | EBinop (s, e1, e2) =>
adamc@1200:             let
adamc@1200:                 val (e1, st) = evalExp env (e1, st)
adamc@1200:                 val (e2, st) = evalExp env (e2, st)
adamc@1200:             in
adamc@1200:                 (Func (s, [e1, e2]), st)
adamc@1200:             end
adamc@1200:           | ERecord xets =>
adamc@1200:             let
adamc@1200:                 val (xes, st) = ListUtil.foldlMap (fn ((x, e, _), st) =>
adamc@1200:                                                       let
adamc@1200:                                                           val (e, st) = evalExp env (e, st)
adamc@1200:                                                       in
adamc@1200:                                                           ((x, e), st)
adamc@1200:                                                       end) st xets
adamc@1200:             in
adamc@1200:                 (Recd xes, st)
adamc@1200:             end
adamc@1200:           | EField (e, s) =>
adamc@1200:             let
adamc@1200:                 val (e, st) = evalExp env (e, st)
adamc@1200:             in
adamc@1200:                 (Proj (e, s), st)
adamc@1200:             end
adamc@1200:           | ECase _ => default ()
adamc@1200:           | EStrcat (e1, e2) =>
adamc@1200:             let
adamc@1200:                 val (e1, st) = evalExp env (e1, st)
adamc@1200:                 val (e2, st) = evalExp env (e2, st)
adamc@1200:             in
adamc@1200:                 (Func ("cat", [e1, e2]), st)
adamc@1200:             end
adamc@1200:           | EError _ => (Finish, st)
adamc@1200:           | EReturnBlob {blob = b, mimeType = m, ...} =>
adamc@1200:             let
adamc@1200:                 val (b, st) = evalExp env (b, st)
adamc@1200:                 val (m, st) = evalExp env (m, st)
adamc@1200:             in
adamc@1200:                 (Finish, (#1 st, p, addSent (#2 st, b, addSent (#2 st, m, sent))))
adamc@1200:             end
adamc@1200:           | ERedirect (e, _) =>
adamc@1200:             let
adamc@1200:                 val (e, st) = evalExp env (e, st)
adamc@1200:             in
adamc@1200:                 (Finish, (#1 st, p, addSent (#2 st, e, sent)))
adamc@1200:             end
adamc@1200:           | EWrite e =>
adamc@1200:             let
adamc@1200:                 val (e, st) = evalExp env (e, st)
adamc@1200:             in
adamc@1200:                 (Func ("unit", []), (#1 st, p, addSent (#2 st, e, sent)))
adamc@1200:             end
adamc@1200:           | ESeq (e1, e2) =>
adamc@1200:             let
adamc@1200:                 val (_, st) = evalExp env (e1, st)
adamc@1200:             in
adamc@1200:                 evalExp env (e2, st)
adamc@1200:             end
adamc@1200:           | ELet (_, _, e1, e2) =>
adamc@1200:             let
adamc@1200:                 val (e1, st) = evalExp env (e1, st)
adamc@1200:             in
adamc@1200:                 evalExp (e1 :: env) (e2, st)
adamc@1200:             end
adamc@1200:           | EClosure (n, es) =>
adamc@1200:             let
adamc@1200:                 val (es, st) = ListUtil.foldlMap (evalExp env) st es
adamc@1200:             in
adamc@1200:                 (Func ("Cl" ^ Int.toString n, es), st)
adamc@1200:             end
adamc@1200: 
adamc@1200:           | EQuery {query = q, body = b, initial = i, ...} =>
adamc@1200:             let
adamc@1200:                 val (_, st) = evalExp env (q, st)
adamc@1200:                 val (i, st) = evalExp env (i, st)
adamc@1200: 
adamc@1200:                 val r = #1 st
adamc@1200:                 val acc = #1 st + 1
adamc@1200:                 val st' = (#1 st + 2, #2 st, #3 st)
adamc@1200: 
adamc@1200:                 val (b, st') = evalExp (Var acc :: Var r :: env) (b, st')
adamc@1200: 
adamc@1200:                 val r' = newLvar ()
adamc@1200:                 val acc' = newLvar ()
adamc@1200:                 val qp = queryProp r' q
adamc@1200: 
adamc@1200:                 val doSubExp = subExp (r, r') o subExp (acc, acc')
adamc@1200:                 val doSubProp = subProp (r, r') o subProp (acc, acc')
adamc@1200: 
adamc@1200:                 val p = doSubProp (#2 st')
adamc@1200:                 val p = And (p, qp)
adamc@1200:                 val p = Select (r, r', acc', p, doSubExp b)
adamc@1200:             in
adamc@1200:                 (Var r, (#1 st + 1, And (#2 st, p), map (fn (e, p) => (doSubExp e, And (qp, doSubProp p))) (#3 st')))
adamc@1200:             end
adamc@1200:           | EDml _ => default ()
adamc@1200:           | ENextval _ => default ()
adamc@1200:           | ESetval _ => default ()
adamc@1200: 
adamc@1200:           | EUnurlify _ => default ()
adamc@1200:           | EJavaScript _ => default ()
adamc@1200:           | ESignalReturn _ => default ()
adamc@1200:           | ESignalBind _ => default ()
adamc@1200:           | ESignalSource _ => default ()
adamc@1200:           | EServerCall _ => default ()
adamc@1200:           | ERecv _ => default ()
adamc@1200:           | ESleep _ => default ()
adamc@1200:           | ESpawn _ => default ()
adamc@1200:     end
adamc@1200: 
adamc@1200: fun check file =
adamc@1200:     let
adamc@1200:         fun decl ((d, _), summaries) =
adamc@1200:             case d of
adamc@1200:                 DVal (x, _, _, e, _) =>
adamc@1200:                 let
adamc@1200:                     fun deAbs (e, env, nv) =
adamc@1200:                         case #1 e of
adamc@1200:                             EAbs (_, _, _, e) => deAbs (e, Var nv :: env, nv + 1)
adamc@1200:                           | _ => (e, env, nv)
adamc@1200: 
adamc@1200:                     val (e, env, nv) = deAbs (e, [], 0)
adamc@1200: 
adamc@1200:                     val (e, (_, p, sent)) = evalExp env (e, (nv, True, []))
adamc@1200:                 in
adamc@1200:                     (x, e, p, sent) :: summaries
adamc@1200:                 end
adamc@1200:               | _ => summaries
adamc@1200:     in
adamc@1200:         raise Summaries (foldl decl [] file)
adamc@1200:     end
adamc@1200: 
adamc@1200: end