Ur/Web: src/iflow.sml comparison

comparison src/iflow.sml @ 1202:509a6d7b60fb

Iflow tested with positive and negative cases

author	Adam Chlipala <adamc@hcoop.net>
date	Sun, 04 Apr 2010 16:17:23 -0400
parents	8793fd48968c
children	a75c66dd2aeb

comparison

equal deleted inserted replaced

-:8793fd48968c
+:509a6d7b60fb
 structure Iflow :> IFLOW = struct
 open Mono
+structure IM = IntBinaryMap
 structure SS = BinarySetFn(struct
 type ord_key = string
 val compare = String.compare
 end)
 | Or of prop * prop
 | Reln of reln * exp list
 | Select of int * lvar * lvar * prop * exp
 local
-val count = ref 0
+val count = ref 1
 in
 fun newLvar () =
 let
 val n = !count
 in
 | Reln (r, es) => Reln (r, map (subExp (v, lv)) es)
 | Select (v1, lv1, lv2, p, e) => Select (v1, lv1, lv2, sub p, subExp (v, lv) e)
 in
 sub
 end
-fun eq' (e1, e2) =
-case (e1, e2) of
-(Const p1, Const p2) => Prim.equal (p1, p2)
-| (Var n1, Var n2) => n1 = n2
-| (Lvar n1, Lvar n2) => n1 = n2
-| (Func (f1, es1), Func (f2, es2)) => f1 = f2 andalso ListPair.allEq eq' (es1, es2)
-| (Recd xes1, Recd xes2) => ListPair.allEq (fn ((x1, e1), (x2, e2)) => x1 = x2 andalso eq' (e1, e2)) (xes1, xes2)
-| (Proj (e1, s1), Proj (e2, s2)) => eq' (e1, e2) andalso s1 = s2
-| (Finish, Finish) => true
-| _ => false
 fun isKnown e =
 case e of
 Const _ => true
 | Func (_, es) => List.all isKnown es
 Finish
 else
 Proj (e', s))
 | Finish => Finish
-fun eq (e1, e2) = eq' (simplify e1, simplify e2)
+fun decomp fals or =
-fun decomp or =
 let
 fun decomp p k =
 case p of
 True => k []
-| False => true
+| False => fals
 | Unknown => k []
 | And (p1, p2) =>
 decomp p1 (fn ps1 =>
 decomp p2 (fn ps2 =>
 k (ps1 @ ps2)))
 | Select _ => k []
 in
 decomp
 end
-fun rimp ((r1 : reln, es1), (r2, es2)) =
+val unif = ref (IM.empty : exp IM.map)
-r1 = r2 andalso ListPair.allEq eq (es1, es2)
+fun lvarIn lv =
-fun imp (p1, p2) =
+let
-decomp (fn (e1, e2) => e1 andalso e2 ()) p1
+fun lvi e =
-(fn hyps =>
+case e of
-decomp (fn (e1, e2) => e1 orelse e2 ()) p2
+Const _ => false
-(fn goals =>
+| Var _ => false
-List.all (fn r2 => List.exists (fn r1 => rimp (r1, r2)) hyps) goals))
+| Lvar lv' => lv' = lv
+| Func (_, es) => List.exists lvi es
+| Recd xes => List.exists (lvi o #2) xes
+| Proj (e, _) => lvi e
+| Finish => false
+in
+lvi
+end
+fun eq' (e1, e2) =
+case (e1, e2) of
+(Const p1, Const p2) => Prim.equal (p1, p2)
+| (Var n1, Var n2) => n1 = n2
+| (Lvar n1, _) =>
+(case IM.find (!unif, n1) of
+SOME e1 => eq' (e1, e2)
+| NONE =>
+case e2 of
+Lvar n2 =>
+(case IM.find (!unif, n2) of
+SOME e2 => eq' (e1, e2)
+| NONE => n1 = n2
+orelse (unif := IM.insert (!unif, n1, e2);
+true))
+| _ =>
+if lvarIn n1 e2 then
+false
+else
+(unif := IM.insert (!unif, n1, e2);
+true))
+| (_, Lvar n2) =>
+(case IM.find (!unif, n2) of
+SOME e2 => eq' (e1, e2)
+| NONE =>
+if lvarIn n2 e1 then
+false
+else
+(unif := IM.insert (!unif, n2, e1);
+true))
+| (Func (f1, es1), Func (f2, es2)) => f1 = f2 andalso ListPair.allEq eq' (es1, es2)
+| (Recd xes1, Recd xes2) => ListPair.allEq (fn ((x1, e1), (x2, e2)) => x1 = x2 andalso eq' (e1, e2)) (xes1, xes2)
+| (Proj (e1, s1), Proj (e2, s2)) => eq' (e1, e2) andalso s1 = s2
+| (Finish, Finish) => true
+| _ => false
+fun eq (e1, e2) =
+let
+val saved = !unif
+in
+if eq' (simplify e1, simplify e2) then
+true
+else
+(unif := saved;
+false)
+end
+exception Imply of prop * prop
+fun rimp ((r1, es1), (r2, es2)) =
+case (r1, r2) of
+(Sql r1', Sql r2') =>
+r1' = r2' andalso
+(case (es1, es2) of
+([Recd xes1], [Recd xes2]) =>
+let
+val saved = !unif
+in
+(*print ("Go: " ^ r1' ^ "\n");*)
+(*raise Imply (Reln (r1, es1), Reln (r2, es2));*)
+if List.all (fn (f, e2) =>
+List.exists (fn (f', e1) =>
+f' = f andalso eq (e1, e2)) xes1) xes2 then
+true
+else
+(unif := saved;
+false)
+end
+| _ => false)
+| (Eq, Eq) =>
+(case (es1, es2) of
+([x1, y1], [x2, y2]) =>
+let
+val saved = !unif
+in
+if eq (x1, x2) andalso eq (y1, y2) then
+true
+else
+(unif := saved;
+(*raise Imply (Reln (Eq, es1), Reln (Eq, es2));*)
+eq (x1, y2) andalso eq (y1, x2))
+end
+| _ => false)
+| _ => false
+fun imply (p1, p2) =
+(unif := IM.empty;
+(*raise (Imply (p1, p2));*)
+decomp true (fn (e1, e2) => e1 andalso e2 ()) p1
+(fn hyps =>
+decomp false (fn (e1, e2) => e1 orelse e2 ()) p2
+(fn goals =>
+let
+fun gls goals onFail =
+case goals of
+[] => true
+| g :: goals =>
+let
+fun hps hyps =
+case hyps of
+[] => onFail ()
+| h :: hyps =>
+let
+val saved = !unif
+in
+if rimp (h, g) then
+let
+val changed = IM.numItems (!unif) = IM.numItems saved
+in
+gls goals (fn () => (unif := saved;
+changed andalso hps hyps))
+end
+else
+hps hyps
+end
+in
+hps hyps
+end
+in
+gls goals (fn () => false)
+end)))
 fun patCon pc =
 case pc of
 PConVar n => "C" ^ Int.toString n
 | PConFfi {mod = m, datatyp = d, con = c, ...} => m ^ "." ^ d ^ "." ^ c
-exception Summaries of (string * exp * prop * (exp * prop) list) list
 datatype chunk =
 String of string
 | Exp of Mono.exp
 type 'a parser = chunk list -> ('a * chunk list) option
 fun always v chs = SOME (v, chs)
-fun parse p chs =
+fun parse p s =
-case p chs of
+case p (chunkify s) of
 SOME (v, []) => SOME v
 | _ => NONE
 fun const s chs =
 case chs of
 (fn ((), ls) => ls)
 val query = wrap (follow select from)
 (fn (fs, ts) => {Select = fs, From = ts})
-fun queryProp rv e =
+fun queryProp rv oe e =
-case parse query (chunkify e) of
+case parse query e of
 NONE => Unknown
 | SOME r =>
-foldl (fn ((t, v), p) =>
+let
-And (p,
+val p =
-Reln (Sql t,
+foldl (fn ((t, v), p) =>
-[Recd (foldl (fn ((v', f), fs) =>
+And (p,
-if v' = v then
+Reln (Sql t,
-(f, Proj (Proj (Lvar rv, v), f)) :: fs
+[Recd (foldl (fn ((v', f), fs) =>
-else
+if v' = v then
-fs) [] (#Select r))])))
+(f, Proj (Proj (Lvar rv, v), f)) :: fs
-True (#From r)
+else
+fs) [] (#Select r))])))
-fun evalExp env (e : Mono.exp, st as (nv, p, sent)) =
+True (#From r)
+in
+case oe of
+NONE => p
+| SOME oe =>
+And (p,
+foldl (fn ((v, f), p) =>
+Or (p,
+Reln (Eq, [oe, Proj (Proj (Lvar rv, v), f)])))
+False (#Select r))
+end
+fun evalExp env (e as (_, loc), st as (nv, p, sent)) =
 let
 fun default () =
 (Var nv, (nv+1, p, sent))
 fun addSent (p, e, sent) =
 if isKnown e then
 sent
 else
-(e, p) :: sent
+(loc, e, p) :: sent
 in
 case #1 e of
 EPrim p => (Const p, st)
 | ERel n => (List.nth (env, n), st)
 | ENamed _ => default ()
 val (b, st') = evalExp (Var acc :: Var r :: env) (b, st')
 val r' = newLvar ()
 val acc' = newLvar ()
-val qp = queryProp r' q
+val qp = queryProp r' NONE q
 val doSubExp = subExp (r, r') o subExp (acc, acc')
 val doSubProp = subProp (r, r') o subProp (acc, acc')
 val p = doSubProp (#2 st')
 val p = And (p, qp)
 val p = Select (r, r', acc', p, doSubExp b)
 in
-(Var r, (#1 st + 1, And (#2 st, p), map (fn (e, p) => (doSubExp e, And (qp, doSubProp p))) (#3 st')))
+(Var r, (#1 st + 1, And (#2 st, p), map (fn (loc, e, p) => (loc,
+doSubExp e,
+And (qp, doSubProp p))) (#3 st')))
 end
 | EDml _ => default ()
 | ENextval _ => default ()
 | ESetval _ => default ()
 | ESpawn _ => default ()
 end
 fun check file =
 let
-fun decl ((d, _), summaries) =
+fun decl ((d, _), (vals, pols)) =
 case d of
 DVal (x, _, _, e, _) =>
 let
 fun deAbs (e, env, nv) =
 case #1 e of
 EAbs (_, _, _, e) => deAbs (e, Var nv :: env, nv + 1)
 | _ => (e, env, nv)
-val (e, env, nv) = deAbs (e, [], 0)
+val (e, env, nv) = deAbs (e, [], 1)
 val (e, (_, p, sent)) = evalExp env (e, (nv, True, []))
 in
-(x, e, p, sent) :: summaries
+((x, e, p, sent) :: vals, pols)
 end
-| _ => summaries
-in
+| DPolicy (PolQuery e) => (vals, queryProp 0 (SOME (Var 0)) e :: pols)
-raise Summaries (foldl decl [] file)
+| _ => (vals, pols)
+val () = unif := IM.empty
+val (vals, pols) = foldl decl ([], []) file
+in
+app (fn (name, _, _, sent) =>
+app (fn (loc, e, p) =>
+let
+val p = And (p, Reln (Eq, [Var 0, e]))
+in
+if List.exists (fn pol => imply (p, pol)) pols then
+()
+else
+ErrorMsg.errorAt loc "The information flow policy may be violated here."
+end) sent) vals
 end
 end

Mercurial > urweb

comparison src/iflow.sml @ 1202:509a6d7b60fb