Mercurial > urweb

comparison src/iflow.sml @ 1210:c5bd970e77a5

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Parsing more comparison operators
author Adam Chlipala <adamc@hcoop.net>
date Tue, 06 Apr 2010 12:04:08 -0400
parents 775357041e48
children 1d4d65245dd3
comparison
equal deleted inserted replaced
1209:775357041e48 1210:c5bd970e77a5
66 66
67 datatype reln = 67 datatype reln =
68 Known 68 Known
69 | Sql of string 69 | Sql of string
70 | Eq 70 | Eq
71 | Ne
72 | Lt
73 | Le
74 | Gt
75 | Ge
71 76
72 datatype prop = 77 datatype prop =
73 True 78 True
74 | False 79 | False
75 | Unknown 80 | Unknown
90 | Lvar n => string ("X" ^ Int.toString n) 95 | Lvar n => string ("X" ^ Int.toString n)
91 | Func (f, es) => box [string (f ^ "("), 96 | Func (f, es) => box [string (f ^ "("),
92 p_list p_exp es, 97 p_list p_exp es,
93 string ")"] 98 string ")"]
94 | Recd xes => box [string "{", 99 | Recd xes => box [string "{",
95 p_list (fn (x, e) => box [string "x", 100 p_list (fn (x, e) => box [string x,
96 space, 101 space,
97 string "=", 102 string "=",
98 space, 103 space,
99 p_exp e]) xes, 104 p_exp e]) xes,
100 string "}"] 105 string "}"]
101 | Proj (e, x) => box [p_exp e, 106 | Proj (e, x) => box [p_exp e,
102 string ("." ^ x)] 107 string ("." ^ x)]
103 | Finish => string "FINISH" 108 | Finish => string "FINISH"
109
110 fun p_bop s es =
111 case es of
112 [e1, e2] => box [p_exp e1,
113 space,
114 string s,
115 space,
116 p_exp e2]
117 | _ => raise Fail "Iflow.p_bop"
104 118
105 fun p_reln r es = 119 fun p_reln r es =
106 case r of 120 case r of
107 Known => 121 Known =>
108 (case es of 122 (case es of
111 string ")"] 125 string ")"]
112 | _ => raise Fail "Iflow.p_reln: Known") 126 | _ => raise Fail "Iflow.p_reln: Known")
113 | Sql s => box [string (s ^ "("), 127 | Sql s => box [string (s ^ "("),
114 p_list p_exp es, 128 p_list p_exp es,
115 string ")"] 129 string ")"]
116 | Eq => 130 | Eq => p_bop "=" es
117 (case es of 131 | Ne => p_bop "<>" es
118 [e1, e2] => box [p_exp e1, 132 | Lt => p_bop "<" es
119 space, 133 | Le => p_bop "<=" es
120 string "=", 134 | Gt => p_bop ">" es
121 space, 135 | Ge => p_bop ">=" es
122 p_exp e2]
123 | _ => raise Fail "Iflow.p_reln: Eq")
124 136
125 fun p_prop p = 137 fun p_prop p =
126 case p of 138 case p of
127 True => string "True" 139 True => string "True"
128 | False => string "False" 140 | False => string "False"
658 670
659 val t_ident = wrap ident (fn s => if String.isPrefix "T_" s then 671 val t_ident = wrap ident (fn s => if String.isPrefix "T_" s then
660 String.extract (s, 2, NONE) 672 String.extract (s, 2, NONE)
661 else 673 else
662 raise Fail "Iflow: Bad table variable") 674 raise Fail "Iflow: Bad table variable")
663 val uw_ident = wrap ident (fn s => if String.isPrefix "uw_" s then 675 val uw_ident = wrap ident (fn s => if String.isPrefix "uw_" s andalso size s >= 4 then
664 String.extract (s, 3, NONE) 676 str (Char.toUpper (String.sub (s, 3)))
677 ^ String.extract (s, 4, NONE)
665 else 678 else
666 raise Fail "Iflow: Bad uw_* variable") 679 raise Fail "Iflow: Bad uw_* variable")
667 680
668 val sitem = wrap (follow t_ident 681 val sitem = wrap (follow t_ident
669 (follow (const ".") 682 (follow (const ".")
679 | Field of string * string 692 | Field of string * string
680 | Binop of Rel * sqexp * sqexp 693 | Binop of Rel * sqexp * sqexp
681 | SqKnown of sqexp 694 | SqKnown of sqexp
682 | Inj of Mono.exp 695 | Inj of Mono.exp
683 696
684 val sqbrel = altL [wrap (const "=") (fn () => Exps (fn (e1, e2) => Reln (Eq, [e1, e2]))), 697 fun cmp s r = wrap (const s) (fn () => Exps (fn (e1, e2) => Reln (r, [e1, e2])))
698
699 val sqbrel = altL [cmp "=" Eq,
700 cmp "<>" Ne,
701 cmp "<=" Le,
702 cmp "<" Lt,
703 cmp ">=" Ge,
704 cmp ">" Gt,
685 wrap (const "AND") (fn () => Props And), 705 wrap (const "AND") (fn () => Props And),
686 wrap (const "OR") (fn () => Props Or)] 706 wrap (const "OR") (fn () => Props Or)]
687 707
688 datatype ('a, 'b) sum = inl of 'a | inr of 'b 708 datatype ('a, 'b) sum = inl of 'a | inr of 'b
689 709
786 806
787 fun queryProp env rv oe e = 807 fun queryProp env rv oe e =
788 case parse query e of 808 case parse query e of
789 NONE => (print ("Warning: Information flow checker can't parse SQL query at " 809 NONE => (print ("Warning: Information flow checker can't parse SQL query at "
790 ^ ErrorMsg.spanToString (#2 e) ^ "\n"); 810 ^ ErrorMsg.spanToString (#2 e) ^ "\n");
791 Unknown) 811 (Unknown, []))
792 | SOME r => 812 | SOME r =>
793 let 813 let
794 val p = 814 val p =
795 foldl (fn ((t, v), p) => 815 foldl (fn ((t, v), p) =>
796 And (p, 816 And (p,
824 | _ => raise Fail "Iflow: non-variable injected into query" 844 | _ => raise Fail "Iflow: non-variable injected into query"
825 in 845 in
826 inl (deinj e) 846 inl (deinj e)
827 end 847 end
828 848
849 fun usedFields e =
850 case e of
851 SqConst _ => []
852 | Field (v, f) => [Proj (Proj (Lvar rv, v), f)]
853 | Binop (_, e1, e2) => usedFields e1 @ usedFields e2
854 | SqKnown _ => []
855 | Inj _ => []
856
829 val p = case #Where r of 857 val p = case #Where r of
830 NONE => p 858 NONE => p
831 | SOME e => 859 | SOME e =>
832 case expIn e of 860 case expIn e of
833 inr p' => And (p, p') 861 inr p' => And (p, p')
834 | _ => p 862 | _ => p
835 in 863 in
836 case oe of 864 (case oe of
837 NONE => p 865 NONE => p
838 | SOME oe => 866 | SOME oe =>
839 And (p, foldl (fn ((v, f), p) => 867 And (p, foldl (fn ((v, f), p) =>
840 Or (p, 868 Or (p,
841 Reln (Eq, [oe, Proj (Proj (Lvar rv, v), f)]))) 869 Reln (Eq, [oe, Proj (Proj (Lvar rv, v), f)])))
842 False (#Select r)) 870 False (#Select r)),
871
872 case #Where r of
873 NONE => []
874 | SOME e => usedFields e)
843 end 875 end
844 876
845 fun evalExp env (e as (_, loc), st as (nv, p, sent)) = 877 fun evalExp env (e as (_, loc), st as (nv, p, sent)) =
846 let 878 let
847 fun default () = 879 fun default () =
977 1009
978 val (b, st') = evalExp (Var acc :: Var r :: env) (b, st') 1010 val (b, st') = evalExp (Var acc :: Var r :: env) (b, st')
979 1011
980 val r' = newLvar () 1012 val r' = newLvar ()
981 val acc' = newLvar () 1013 val acc' = newLvar ()
982 val qp = queryProp env r' NONE q 1014 val (qp, used) = queryProp env r' NONE q
983 1015
984 val doSubExp = subExp (r, r') o subExp (acc, acc') 1016 val doSubExp = subExp (r, r') o subExp (acc, acc')
985 val doSubProp = subProp (r, r') o subProp (acc, acc') 1017 val doSubProp = subProp (r, r') o subProp (acc, acc')
986 1018
987 val p = doSubProp (#2 st') 1019 val p = doSubProp (#2 st')
988 val p = And (p, qp) 1020 val p' = And (p, qp)
989 val p = Select (r, r', acc', p, doSubExp b) 1021 val p = Select (r, r', acc', p', doSubExp b)
990 in 1022
991 (Var r, (#1 st + 1, And (#2 st, p), map (fn (loc, e, p) => (loc, 1023 val sent = map (fn (loc, e, p) => (loc,
992 doSubExp e, 1024 doSubExp e,
993 And (qp, doSubProp p))) (#3 st'))) 1025 And (qp, doSubProp p))) (#3 st')
1026 val sent = map (fn e => (loc, e, p')) used @ sent
1027 in
1028 (Var r, (#1 st + 1, And (#2 st, p), sent))
994 end 1029 end
995 | EDml _ => default () 1030 | EDml _ => default ()
996 | ENextval _ => default () 1031 | ENextval _ => default ()
997 | ESetval _ => default () 1032 | ESetval _ => default ()
998 1033
1034 val (e, (_, p, sent)) = evalExp env (e, (nv, p, [])) 1069 val (e, (_, p, sent)) = evalExp env (e, (nv, p, []))
1035 in 1070 in
1036 (sent @ vals, pols) 1071 (sent @ vals, pols)
1037 end 1072 end
1038 1073
1039 | DPolicy (PolQuery e) => (vals, queryProp [] 0 (SOME (Var 0)) e :: pols) 1074 | DPolicy (PolQuery e) => (vals, #1 (queryProp [] 0 (SOME (Var 0)) e) :: pols)
1040 1075
1041 | _ => (vals, pols) 1076 | _ => (vals, pols)
1042 1077
1043 val () = reset () 1078 val () = reset ()
1044 1079