diff options
| -rw-r--r-- | xacml-proofs/compiler/bin/main.ml | 89 |
1 files changed, 59 insertions, 30 deletions
diff --git a/xacml-proofs/compiler/bin/main.ml b/xacml-proofs/compiler/bin/main.ml index 66a7145..a4661b9 100644 --- a/xacml-proofs/compiler/bin/main.ml +++ b/xacml-proofs/compiler/bin/main.ml @@ -260,13 +260,10 @@ let rec compile_expression (Identifier "Expression.attribute_value", [compile_attribute_value elt]) | "VariableReference" -> - (match children with - | [PCData identifier] -> - (match List.Assoc.find ~equal:String.equal env identifier with - | Some value -> value - (* TODO: Delayed referencing of variables? *) - | _ -> failwith "unbound variable") - | _ -> failwith "invalid <VariableReference>") + let identifier = get_attr_exn "VariableId" attrs in + (match List.Assoc.find ~equal:String.equal env identifier with + | Some value -> value + | _ -> failwith "unbound variable") | _ -> failwith "unknown expression type" let compile_condition @@ -418,6 +415,36 @@ let compile_variable_definition let value = get_child_exn "Expression" children in (identifier, compile_expression env value) +let order_variable_definitions elts = + let rec find_variable_references identifier : Xml.xml -> (string * string) list = + function + | Element ("VariableReference", attrs, _) -> + let referenced_identifier = get_attr_exn "VariableId" attrs in + [(identifier, referenced_identifier)] + | Element (_, _, children) -> + List.map ~f:(find_variable_references identifier) + children + |> List.concat + | _ -> [] + in + let nodes = + List.map + ~f:(function + | ("VariableDefinition", attrs, _) -> get_attr_exn "VariableId" attrs) + elts in + let edges = + List.map + ~f:(function + | ("VariableDefinition", attrs, children) as elt -> + find_variable_references (get_attr_exn "VariableId" attrs) (Element elt) + | _ -> failwith "unreachable") + elts + |> List.concat + in + let open Topological_sort in + let edges = List.map edges ~f:(fun (from, to_) -> { Topological_sort.Edge.from; to_ }) in + sort (module String) nodes edges + let compile_policy (elt : xml_element) : compilation_intermediate = let (tag_name, attrs, children) = elt in assert (String.equal tag_name "Policy"); @@ -425,7 +452,12 @@ let compile_policy (elt : xml_element) : compilation_intermediate = let version = get_attr_exn "Version" attrs in assert (Str.string_match version_regex version 0); let variables = - List.fold (get_children "VariableDefinition" children) + match order_variable_definitions (get_children "VariableDefinition" children) with + | Ok variables -> variables + | _ -> failwith "failed to order variable definitions" + in + let variables = + List.fold variables ~init:[] ~f:(fun x y -> let (key, value) = compile_variable_definition x y in @@ -581,28 +613,25 @@ let rec policy_element_names (root : xml_element) = [`Policy (identifier, version)] | _ -> [] -let find_edges (elts : lean_expression list) : (string * string) list = - List.map - ~f:(function - | Define (parent, Application (_, [_; List children])) -> - List.map ~f:(function - | Identifier child -> (child, parent) - | _ -> failwith "badly formed list of expressions") - children - | _ -> failwith "badly formed list of expressions") - elts - |> List.concat - -let find_nodes (elts : lean_expression list) : string list = - List.map - ~f:(function - | Define (identifier, _) -> identifier - | _ -> failwith "badly formed list of expressions") - elts - -let order_element_definitions element_definitions = - let nodes = find_nodes element_definitions in - let edges = find_edges element_definitions in +let order_element_definitions elts = + let nodes = + List.map + ~f:(function + | Define (identifier, _) -> identifier + | _ -> failwith "badly formed list of expressions") + elts in + let edges = + List.map + ~f:(function + | Define (parent, Application (_, [_; List children])) -> + List.map ~f:(function + | Identifier child -> (child, parent) + | _ -> failwith "badly formed list of expressions") + children + | _ -> failwith "badly formed list of expressions") + elts + |> List.concat + in let open Topological_sort in let edges = List.map edges ~f:(fun (from, to_) -> { Topological_sort.Edge.from; to_ }) in sort (module String) nodes edges |