diff options
Diffstat (limited to 'xacml-proofs/compiler/lib/compiler.ml')
| -rw-r--r-- | xacml-proofs/compiler/lib/compiler.ml | 103 |
1 files changed, 93 insertions, 10 deletions
diff --git a/xacml-proofs/compiler/lib/compiler.ml b/xacml-proofs/compiler/lib/compiler.ml index 73ecd6e..7a18643 100644 --- a/xacml-proofs/compiler/lib/compiler.ml +++ b/xacml-proofs/compiler/lib/compiler.ml @@ -7,7 +7,8 @@ let version_match_type_regex = Str.regexp "^\\(\\(\\d+|\\*\\)\\.\\)*\\(\\d+|\\*| type xml_element = (string * (string * string) list * Xml.xml list) -type lean_expression = Identifier of string +type lean_expression = Eval of lean_expression + | Identifier of string | Bool of bool | String of string (* | Number of int *) @@ -17,6 +18,7 @@ type lean_expression = Identifier of string | Define of string * lean_expression let rec fmt_lean_expression : lean_expression -> string = function + | Eval expr -> (Printf.sprintf "#eval %s" (fmt_lean_expression expr)) | Identifier s -> s | Bool b -> if b then "True" else "False" | String s -> Printf.sprintf "\"%s\"" s @@ -202,11 +204,19 @@ let rec compile_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 env elt) - | _ -> None) in - Application (Identifier "Expression.apply", args) + (match get_attr "FunctionId" attrs with + | None -> + let args = List.filter_map children ~f:(function + | Element ("Description", _, _) -> None + | Element elt -> Some (compile_expression env elt) + | _ -> None) in + Application (Identifier "Expression.apply", args) + | Some name -> + let args = List.filter_map children ~f:(function + | Element ("Description", _, _) -> None + | Element elt -> Some (compile_expression env elt) + | _ -> None) in + Application (Identifier "Expression.apply", String name :: args)) | "Function" -> let name = get_attr_exn "FunctionID" attrs in Application (Identifier "Expression.function", [String name]) @@ -528,7 +538,7 @@ let rec compile_policyset | Some identifier -> Some { metadata_definitions = []; element_definitions = []; - root_identifier = identifier; + root_identifier = (Printf.sprintf "%s_element" identifier); edges = [] } | _ -> failwith (Printf.sprintf "unbound reference to %s" identifier)) | Element (("Policy", _, _) as elt) -> Some (compile_policy elt) @@ -541,7 +551,7 @@ let rec compile_policyset | Some identifier -> Some { metadata_definitions = []; element_definitions = []; - root_identifier = identifier; + root_identifier = (Printf.sprintf "%s_element" identifier); edges = [] } | _ -> failwith (Printf.sprintf "unbound reference to %s" identifier)) | _ -> None) @@ -624,7 +634,16 @@ let compile policy_elements : Xml.xml -> lean_expression list = function element_definitions) | _ -> failwith "failed to order definitions") in - metadata_definitions @ element_definitions @ [Identifier root_identifier] + metadata_definitions + @ element_definitions + @ [Eval + (Application (Identifier "IO.println", + [(Application (Identifier "xml_of_response", + [Application (Identifier "Result'.eval", + [Application (Identifier "ElementTree.eval", + [Identifier "request"; + Identifier root_identifier]); + Identifier "request"])]))]))] | PCData s -> failwith s let xml_element_of_Xml : Xml.xml -> xml_element = function @@ -632,7 +651,7 @@ let xml_element_of_Xml : Xml.xml -> xml_element = function | _ -> failwith "not an element" -let compile' (policies : string list) : string = +let compile_policies (policies : string list) : string = let policies = List.map ~f:Xml.parse_string policies in let policy_elements = List.map ~f:xml_element_of_Xml policies |> List.map ~f:policy_element_names @@ -643,3 +662,67 @@ let compile' (policies : string list) : string = |> List.concat |> List.map ~f:fmt_lean_expression |> String.concat ~sep:"\n" + +(* --- *) + +let xml_type_of_string : string -> lean_expression = function + | "http://www.w3.org/2001/XMLSchema#string" -> Identifier "XmlType.string" + | "http://www.w3.org/2001/XMLSchema#boolean" -> Identifier "XmlType.boolean" + | "http://www.w3.org/2001/XMLSchema#integer" -> Identifier "XmlType.integer" + | "http://www.w3.org/2001/XMLSchema#double" -> Identifier "XmlType.double" + | "http://www.w3.org/2001/XMLSchema#time" -> Identifier "XmlType.time" + | "http://www.w3.org/2001/XMLSchema#date" -> Identifier "XmlType.date" + | "http://www.w3.org/2001/XMLSchema#dateTime" -> Identifier "XmlType.dateTime" + | "http://www.w3.org/2001/XMLSchema#dayTimeDuration" -> Identifier "XmlType.dayTimeDuration" + | "http://www.w3.org/2001/XMLSchema#yearMonthDuration" -> Identifier "XmlType.yearMonthDuration" + | "http://www.w3.org/2001/XMLSchema#anyURI" -> Identifier "XmlType.anyURI" + | "http://www.w3.org/2001/XMLSchema#hexBinary" -> Identifier "XmlType.hexBinary" + | "http://www.w3.org/2001/XMLSchema#base64Binary" -> Identifier "XmlType.base64Binary" + | "urn:oasis:names:tc:xacml:1.0:data-type:rfc822Name" -> Identifier "XmlType.rfc822Name" + | "urn:oasis:names:tc:xacml:1.0:data-type:x500Name" -> Identifier "XmlType.x500Name" + | "urn:oasis:names:tc:xacml:2.0:data-type:ipAddress" -> Identifier "XmlType.ipAddress" + | "urn:oasis:names:tc:xacml:2.0:data-type:dnsName" -> Identifier "XmlType.dnsName" + | s -> failwith (Printf.sprintf "unsupported type: (%s)" s) + +let compile_attribute_value category identifier issuer ((tag_name, attributes, children) : xml_element) : lean_expression list = + assert String.(tag_name = "AttributeValue"); + let typ = get_attr_exn "DataType" attributes in + match children with + | [PCData s] -> + [Application (Identifier "Attribute.mk", + [String category; + String identifier; + (match issuer with + | Some issuer -> Application (Identifier "some", [String issuer]) + | None -> Identifier "none"); + Tuple [xml_type_of_string typ; String s]])] + | _ -> failwith "ill-formed attribute value" + +let compile_attribute category ((tag_name, attributes, children) : xml_element) : lean_expression list = + assert String.(tag_name = "Attribute"); + let identifier = get_attr_exn "AttributeId" attributes in + let issuer = get_attr "Issuer" attributes in + compile_attribute_value category identifier issuer (List.nth_exn children 0 |> xml_element_of_Xml) + +let compile_attributes ((tag_name, attributes, children) : xml_element) : lean_expression list = + assert String.(tag_name = "Attributes"); + let category = get_attr_exn "Category" attributes in + children + |> xml_element_of_children + |> List.map ~f:(compile_attribute category) + |> List.concat + +let compile_request' : Xml.xml -> lean_expression list = function + | Element (("Request", _attributes, children)) -> + List.map ~f:xml_element_of_Xml children + |> List.map ~f:compile_attributes + |> List.concat + | Element ((tag_name, _, _)) -> + failwith (Printf.sprintf "(%s)" tag_name) + | PCData s -> failwith s + +let compile_request (request : string) : string = + let request = Xml.parse_string request in + let attributes = compile_request' request in + Define ("request", List attributes) + |> fmt_lean_expression |