From 249150abcfb531c55fafc2e4907b8a6bb90292d4 Mon Sep 17 00:00:00 2001
From: Jakob L. Kreuze
Date: Wed, 4 Oct 2023 19:40:24 -0400
Subject: Validate VersionType

---
 xacml-proofs/compiler/bin/dune    | 2 +-
 xacml-proofs/compiler/bin/main.ml | 4 ++++
 2 files changed, 5 insertions(+), 1 deletion(-)

diff --git a/xacml-proofs/compiler/bin/dune b/xacml-proofs/compiler/bin/dune
index c8c6569..6d76295 100644
--- a/xacml-proofs/compiler/bin/dune
+++ b/xacml-proofs/compiler/bin/dune
@@ -1,5 +1,5 @@
 (executable
  (public_name compiler)
  (name main)
- (libraries base compiler xml-light)
+ (libraries base compiler str xml-light)
  (preprocess (pps ppx_let)))
diff --git a/xacml-proofs/compiler/bin/main.ml b/xacml-proofs/compiler/bin/main.ml
index 9d1cce4..5df7864 100644
--- a/xacml-proofs/compiler/bin/main.ml
+++ b/xacml-proofs/compiler/bin/main.ml
@@ -1,5 +1,7 @@
 open Base
 
+let version_regex = Str.regexp "^\\([0-9]+\\.\\)*[0-9]+$"
+
 let policy = {|<?xml version="1.0" encoding="UTF-8"?>
 <Policy
   xmlns="urn:oasis:names:tc:xacml:3.0:core:schema:wd-17"
@@ -397,6 +399,7 @@ let compile_policy (elt : xml_element) : (lean_expression list) * lean_expressio
   assert (String.equal tag_name "Policy");
   let identifier = get_attr_exn "PolicyId" attrs in
   let version = get_attr_exn "Version" attrs in
+  assert (Str.string_match version_regex version 0);
   let variables =
     List.fold (get_children "VariableDefinition" children)
       ~init:[]
@@ -435,6 +438,7 @@ let rec compile_policyset (elt : xml_element) : (lean_expression list) * lean_ex
   assert (String.equal tag_name "Rule");
   let identifier = get_attr_exn "PolicySetId" attrs in
   let version = get_attr_exn "Version" attrs in
+  assert (Str.string_match version_regex version 0);
   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
-- 
cgit v1.3