Add missing components

1 files changed, 138 insertions, 16 deletions

diff --git a/xacml-proofs/compiler/bin/main.ml b/xacml-proofs/compiler/bin/main.ml
index ad1e6c4..49fef95 100644
--- a/xacml-proofs/compiler/bin/main.ml
+++ b/xacml-proofs/compiler/bin/main.ml
@@ -62,11 +62,6 @@ let rec fmt_lean_expression : lean_expression -> string = function
   | Tuple xs -> Printf.sprintf "(%s)" (String.concat ~sep:", " (List.map ~f:fmt_lean_expression xs))
   | Application (head, args) -> Printf.sprintf "(%s %s)" (fmt_lean_expression head) (String.concat ~sep:" " (List.map ~f:fmt_lean_expression args))
 
-let option_to_lean_expr (opt : lean_expression option) : lean_expression =
-  match opt with
-  | Some expr -> Application (Identifier "some", [expr])
-  | None -> Application (Identifier "none", [])
-
 let get_exn opt message =
   match opt with
   | Some x -> x
@@ -102,7 +97,7 @@ let compile_rule_combinator_algorithm : string -> lean_expression = function
   | "urn:oasis:names:tc:xacml:3.0:rule-combining-algorithm:ordered-deny-overrides" ->
      (Identifier "RuleCombinatorAlgorithm.ordered_deny_overrides")
   | "urn:oasis:names:tc:xacml:3.0:rule-combining-algorithm:permit-overrides" ->
-     (Identifier "RuleCombinatorAlgorithm.ordered_deny_overrides")
+     (Identifier "RuleCombinatorAlgorithm.permit_overrides")
   | "urn:oasis:names:tc:xacml:3.0:rule-combining-algorithm:ordered-permit-overrides" ->
      (Identifier "RuleCombinatorAlgorithm.ordered_permit_overrides")
   | "urn:oasis:names:tc:xacml:3.0:rule-combining-algorithm:deny-unless-permit" ->
@@ -121,6 +116,32 @@ let compile_rule_combinator_algorithm : string -> lean_expression = function
      (Identifier "RuleCombinatorAlgorithm.legacy_ordered_permit_overrides")
   | _ -> failwith "unknown rule combinator"
 
+let compile_policy_combinator_algorithm : string -> lean_expression = function
+  | "urn:oasis:names:tc:xacml:3.0:policy-combining-algorithm:deny-overrides" ->
+     (Identifier "PolicyCombinatorAlgorithm.deny_overrides")
+  | "urn:oasis:names:tc:xacml:3.0:policy-combining-algorithm:ordered-deny-overrides" ->
+     (Identifier "PolicyCombinatorAlgorithm.ordered_deny_overrides")
+  | "urn:oasis:names:tc:xacml:3.0:policy-combining-algorithm:permit-overrides" ->
+     (Identifier "PolicyCombinatorAlgorithm.permit_overrides")
+  | "urn:oasis:names:tc:xacml:3.0:policy-combining-algorithm:ordered-permit-overrides" ->
+     (Identifier "PolicyCombinatorAlgorithm.ordered_permit_overrides")
+  | "urn:oasis:names:tc:xacml:3.0:policy-combining-algorithm:deny-unless-permit" ->
+     (Identifier "PolicyCombinatorAlgorithm.deny_unless_permit")
+  | "urn:oasis:names:tc:xacml:3.0:policy-combining-algorithm:permit-unless-deny" ->
+     (Identifier "PolicyCombinatorAlgorithm.permit_unless_deny")
+  | "urn:oasis:names:tc:xacml:1.0:policy-combining-algorithm:first-applicable" ->
+     (Identifier "PolicyCombinatorAlgorithm.first_applicable")
+  | "urn:oasis:names:tc:xacml:1.0:policy-combining-algorithm:only-one-applicable" ->
+     (Identifier "PolicyCombinatorAlgorithm.only_one_applicable")
+  | "urn:oasis:names:tc:xacml:1.0:policy-combining-algorithm:deny-overrides" ->
+     (Identifier "PolicyCombinatorAlgorithm.legacy_deny_overrides")
+  | "urn:oasis:names:tc:xacml:1.1:policy-combining-algorithm:ordered-deny-overrides" ->
+     (Identifier "PolicyCombinatorAlgorithm.legacy_ordered_deny_overrides")
+  | "urn:oasis:names:tc:xacml:1.0:policy-combining-algorithm:permit-overrides" ->
+     (Identifier "PolicyCombinatorAlgorithm.legacy_permit_overrides")
+  | "urn:oasis:names:tc:xacml:1.1:policy-combining-algorithm:ordered-permit-overrides" ->
+     (Identifier "PolicyCombinatorAlgorithm.legacy_ordered_permit_overrides")
+  | _ -> failwith "unknown policy combinator"
 
 (* let (tag_name, attributes, children) = elt in *)
 
@@ -180,7 +201,6 @@ let compile_attribute_designator (elt : xml_element) : lean_expression =
       (Bool (Bool.of_string must_be_present))])
 
 let compile_match (elt : xml_element) : lean_expression =
-  (* TODO: Can the match contain multiple value/designator pairs? *)
   let (tag_name, attrs, children) = elt in
   assert (String.equal tag_name "Match");
   let alg_id = get_attr_exn "MatchId" attrs in
@@ -211,15 +231,89 @@ let compile_target (elt : xml_element) : lean_expression =
 
 
 
+let rec compile_expression (elt : xml_element) : lean_expression =
+  let (tag_name, attrs, children) = elt in
+  match tag_name with
+  | "Apply" ->
+     let args = List.filter_map children ~f:(function
+                    | Element ("Description", _, _) -> None
+                    | Element elt -> Some (compile_expression elt)
+                    | _ -> None) in
+     Application (Identifier "Expression.apply", args)
+  | "Function" ->
+     let name = get_attr_exn "FunctionID" attrs in
+     Application (Identifier "Expression.function", [String name])
+  | "AttributeDesignator" ->
+     Application
+       (Identifier "Expression.attribute_designator",
+        [compile_attribute_designator elt])
+  | "AttributeValue" ->
+     Application
+       (Identifier "Expression.attribute_value",
+        [compile_attribute_value elt])
+  | "VariableReference" -> failwith "unimplemented"
+  | _ -> failwith "unknown expression type"
+
 let compile_condition (elt : xml_element) : lean_expression =
   let (tag_name, _, children) = elt in
   assert (String.equal tag_name "Condition");
-  assert (phys_equal (List.length children) 1);
-  List [] (* TODO: Implement compile_expression *)
+  match children with
+  | [Element elt] -> compile_expression elt
+  | _ -> failwith "invalid <Condition> form"
+
+let compile_attribute_assignment_expression (elt : xml_element) : lean_expression =
+  let (tag_name, attrs, children) = elt in
+  assert (String.equal tag_name "AdviceExpression");
+  let category = get_attr_exn "Category" attrs in
+  let identifier = get_attr_exn "Identifier" attrs in
+  let expression = get_child_exn "Expression" children in
+  let issuer = (match get_attr "Identifier" attrs with
+                | Some issuer -> Application (Identifier "some", [String issuer])
+                | None -> Application (Identifier "none", [])) in
+  Application
+    (Identifier "AttributeAssignmentExpression.mk",
+     [String category;
+      String identifier;
+      issuer;
+      compile_expression expression])
+
+let compile_obligation_expression (elt : xml_element) : lean_expression =
+  let (tag_name, attrs, children) = elt in
+  assert (String.equal tag_name "ObligationExpression");
+  let identifier = get_attr_exn "ObligationId" attrs in
+  let assignments = get_children "AttributeAssignmentExpression" children in
+  let fulfill_on = match get_attr_exn "FullfillOn" attrs with
+    | "Permit" -> Identifier "EffectType.permit"
+    | "Deny" -> Identifier "EffectType.deny"
+    | _ -> failwith "invalid <EffectType>"
+  in
+  Application
+    (Identifier "ObligationExpression.mk",
+     [List (List.map assignments ~f:compile_attribute_assignment_expression);
+      String identifier;
+      fulfill_on])
+
+let compile_advice_expression (elt : xml_element) : lean_expression =
+  let (tag_name, attrs, children) = elt in
+  assert (String.equal tag_name "AdviceExpression");
+  let identifier = get_attr_exn "AdviceId" attrs in
+  let assignments = get_children "AttributeAssignmentExpression" children in
+  let applies_to = match get_attr_exn "AppliesTo" attrs with
+    | "Permit" -> Identifier "EffectType.permit"
+    | "Deny" -> Identifier "EffectType.deny"
+    | _ -> failwith "invalid <EffectType>"
+  in
+  Application
+    (Identifier "ObligationExpression.mk",
+     [List (List.map assignments ~f:compile_attribute_assignment_expression);
+      String identifier;
+      applies_to])
 
 let compile_rule (elt : xml_element) : lean_expression =
   let (tag_name, attrs, children) = elt in
   assert (String.equal tag_name "Rule");
+  let obligation_expressions = get_children "ObligationExpression" children in
+  let advice_expressions = get_children "AdviceExpression"children  in
   let effect = match get_attr_exn "Effect" attrs with
     | "Permit" -> Identifier "EffectType.permit"
     | "Deny" -> Identifier "EffectType.deny"
@@ -237,15 +331,19 @@ let compile_rule (elt : xml_element) : lean_expression =
        [target;
         condition;
         effect;
-         (List []);  (* TODO: Compile obligation expressions *)
-         (List [])]) (* TODO: Compile advice expressions *) in
+        List (List.map ~f:compile_obligation_expression obligation_expressions);
+        List (List.map ~f:compile_advice_expression advice_expressions);]) in
   let wrapped =
     Application
       ((Identifier "PolicyElement.Rule"), [metadata]) in
   Application
       ((Identifier "ElementTree.Node"), [wrapped; List []])
 
-let compile_policy (attrs : (string * string) list) (children : Xml.xml list) : lean_expression =
+let compile_policy (elt : xml_element) : lean_expression =
+  let (tag_name, attrs, children) = elt in
+  assert (String.equal tag_name "Policy");
+  let obligation_expressions = get_children "ObligationExpression" children in
+  let advice_expressions = get_children "AdviceExpression" children in
   let alg_id = get_attr_exn "RuleCombiningAlgId" attrs in
   let target = get_child_exn "Target" children in
   let metadata =
@@ -253,8 +351,8 @@ let compile_policy (attrs : (string * string) list) (children : Xml.xml list) :
       ((Identifier "Policy.mk"),
        [compile_rule_combinator_algorithm alg_id;
         compile_target target;
-        (List []);  (* TODO: Compile obligation expressions *)
-        (List [])]) (* TODO: Compile advice expressions *) in
+        List (List.map ~f:compile_obligation_expression obligation_expressions);
+        List (List.map ~f:compile_advice_expression advice_expressions);])in
   let wrapped =
     Application
       ((Identifier "PolicyElement.Policy"), [metadata]) in
@@ -263,11 +361,35 @@ let compile_policy (attrs : (string * string) list) (children : Xml.xml list) :
      [wrapped;
       List (List.map ~f:compile_rule (get_children "Rule" children))])
 
+let compile_policyset (elt : xml_element) : lean_expression =
+  let (tag_name, attrs, children) = elt in
+  assert (String.equal tag_name "Rule");
+  let obligation_expressions = get_children "ObligationExpression" children in
+  let advice_expressions = get_children "AdviceExpression" children in
+  let alg_id = get_attr_exn "PolicyCombiningAlgId" attrs in
+  let target = get_child_exn "Target" children in
+  let metadata =
+    Application
+      ((Identifier "PolicySet.mk"),
+       [compile_policy_combinator_algorithm alg_id;
+        compile_target target;
+        List (List.map ~f:compile_obligation_expression obligation_expressions);
+        List (List.map ~f:compile_advice_expression advice_expressions);])in
+  let wrapped =
+    Application
+      ((Identifier "PolicyElement.PolicySet"), [metadata]) in
+  Application
+    ((Identifier "ElementTree.Node"),
+     [wrapped;
+      (* FIXME: This doesn't preserve order. *)
+      List ((List.map ~f:compile_policy (get_children "Policy" children))
+            @ (List.map ~f:compile_rule (get_children "Rule" children)))])
 
 let compile : Xml.xml -> lean_expression = function
-  | Element (tag_name, attributes, children) ->
+  | Element ((tag_name, attributes, children) as elt) ->
      (match tag_name with
-      | "Policy" -> compile_policy attributes children
+      | "PolicySet" -> compile_policyset elt
+      | "Policy" -> compile_policy elt
       | _ -> failwith (Printf.sprintf "(%s)" tag_name))
   | PCData s -> failwith s