Mercurial > urweb

comparison src/iflow.sml @ 1234:e799c8df3146

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Catching lame FFI applications
author Adam Chlipala <adamc@hcoop.net>
date Tue, 13 Apr 2010 11:15:43 -0400
parents 8d1d2f7163c2
children a7b773f1d053
comparison
equal deleted inserted replaced
1233:8d1d2f7163c2 1234:e799c8df3146
2021 2021
2022 val st = foldl (fn ((c, fl), st) => St.addSent (st, (c, Control fl))) st (St.paths st) 2022 val st = foldl (fn ((c, fl), st) => St.addSent (st, (c, Control fl))) st (St.paths st)
2023 in 2023 in
2024 St.clearPaths st 2024 St.clearPaths st
2025 end 2025 end
2026 in 2026
2027 case #1 e of 2027 fun doFfi (m, s, es) =
2028 EPrim p => (Const p, st)
2029 | ERel n => (List.nth (env, n), st)
2030 | ENamed _ => default ()
2031 | ECon (_, pc, NONE) => (Func (DtCon0 (patCon pc), []), st)
2032 | ECon (_, pc, SOME e) =>
2033 let
2034 val (e, st) = evalExp env (e, st)
2035 in
2036 (Func (DtCon1 (patCon pc), [e]), st)
2037 end
2038 | ENone _ => (Func (DtCon0 "None", []), st)
2039 | ESome (_, e) =>
2040 let
2041 val (e, st) = evalExp env (e, st)
2042 in
2043 (Func (DtCon1 "Some", [e]), st)
2044 end
2045 | EFfi _ => default ()
2046
2047 | EFfiApp (m, s, es) =>
2048 if m = "Basis" andalso SS.member (writers, s) then 2028 if m = "Basis" andalso SS.member (writers, s) then
2049 let 2029 let
2050 val (es, st) = ListUtil.foldlMap (evalExp env) st es 2030 val (es, st) = ListUtil.foldlMap (evalExp env) st es
2051 in 2031 in
2052 (Recd [], foldl (fn (e, st) => addSent (St.ambient st, e, st)) st es) 2032 (Recd [], foldl (fn (e, st) => addSent (St.ambient st, e, st)) st es)
2056 else 2036 else
2057 let 2037 let
2058 val (es, st) = ListUtil.foldlMap (evalExp env) st es 2038 val (es, st) = ListUtil.foldlMap (evalExp env) st es
2059 in 2039 in
2060 (Func (Other (m ^ "." ^ s), es), st) 2040 (Func (Other (m ^ "." ^ s), es), st)
2061 end 2041 end
2042 in
2043 case #1 e of
2044 EPrim p => (Const p, st)
2045 | ERel n => (List.nth (env, n), st)
2046 | ENamed _ => default ()
2047 | ECon (_, pc, NONE) => (Func (DtCon0 (patCon pc), []), st)
2048 | ECon (_, pc, SOME e) =>
2049 let
2050 val (e, st) = evalExp env (e, st)
2051 in
2052 (Func (DtCon1 (patCon pc), [e]), st)
2053 end
2054 | ENone _ => (Func (DtCon0 "None", []), st)
2055 | ESome (_, e) =>
2056 let
2057 val (e, st) = evalExp env (e, st)
2058 in
2059 (Func (DtCon1 "Some", [e]), st)
2060 end
2061 | EFfi _ => default ()
2062
2063 | EFfiApp x => doFfi x
2064 | EApp ((EFfi (m, s), _), e) => doFfi (m, s, [e])
2062 2065
2063 | EApp (e1, e2) => 2066 | EApp (e1, e2) =>
2064 let 2067 let
2065 val (e1, st) = evalExp env (e1, st) 2068 val (e1, st) = evalExp env (e1, st)
2066 in 2069 in
2558 ^ (case fl of 2561 ^ (case fl of
2559 Control Where => " (WHERE clause)" 2562 Control Where => " (WHERE clause)"
2560 | Control Case => " (case discriminee)" 2563 | Control Case => " (case discriminee)"
2561 | Data => " (returned data value)"), 2564 | Data => " (returned data value)"),
2562 Print.p_list p_atom hyps); 2565 Print.p_list p_atom hyps);
2563 Print.preface ("DB", Cc.p_database cc); 2566 (*Print.preface ("DB", Cc.p_database cc);*)
2564 false) 2567 false)
2565 end handle Cc.Contradiction => true) then 2568 end handle Cc.Contradiction => true) then
2566 () 2569 ()
2567 else 2570 else
2568 ErrorMsg.errorAt loc "The information flow policy may be violated here." 2571 ErrorMsg.errorAt loc "The information flow policy may be violated here."