Merge branch 'feature/aymeric/record_node_parser' into 'master'

Add handling for records in property files

Closes #32

See merge request laiser/caisar!105

examples/acasxu/property_5_aimos.why

@@ -3,6 +3,7 @@ theory ACASXU_P5
   use ieee_float.Float64
   use caisar.DatasetClassification
   use caisar.DatasetClassificationProps
+  use option.Option
 
-  goal G: meta_robust model dataset (1.0:t) ("reluplex_rotation":string) ("config/custom_transformations.py":string) ("classif_min":string) (0:int) (0:int) (0:int)
+  goal G: meta_robust model dataset (1.0:t) "reluplex_rotation" "config/custom_transformations.py" "classif_min" None
 end

src/dataset.ml

@@ -51,13 +51,15 @@ let term_of_eps env eps =
 
 type threshold = float [@@deriving yojson, show]
 
-type amplitude = {
-  start : int option;
+type amplitude_record = {
+  start : int;
   stop : int;
-  step : int option;
+  step : int;
 }
 [@@deriving yojson, show]
 
+type amplitude = amplitude_record option [@@deriving yojson, show]
+
 type aimos_params = {
   perturbation : string;
   ctp : string;
@@ -69,20 +71,12 @@ type aimos_params = {
 let string_of_threshold threshold = Float.to_string threshold
 
 let string_of_amplitude amplitude =
-  let start = match amplitude.start with Some a -> a | None -> 0 in
-  if start = amplitude.stop
-  then None
-  else
-    let start_str =
-      Option.value_map amplitude.start ~default:"" ~f:Int.to_string
-    in
-    let step_str =
-      Option.value_map amplitude.step ~default:"" ~f:Int.to_string
-    in
+  match amplitude with
+  | Some a ->
     Some
-      (Fmt.str "range(%s, %s, %s)" start_str
-         (Int.to_string amplitude.stop)
-         step_str)
+      (Fmt.str "range(%s, %s, %s)" (Int.to_string a.start)
+         (Int.to_string a.stop) (Int.to_string a.step))
+  | None -> None
 
 type property =
   | Correct
@@ -107,6 +101,10 @@ let find_predicate_ls env p =
   let th = Pmodule.read_module env [ "caisar" ] "DatasetClassificationProps" in
   Theory.ns_find_ls th.mod_theory.th_export [ p ]
 
+let find_option_ls env p =
+  let th = Pmodule.read_module env [ "option" ] "Option" in
+  Theory.ns_find_ls th.mod_theory.th_export [ p ]
+
 let failwith_unsupported_term t =
   failwith (Fmt.str "Unsupported term %a" Pretty.print_term t)
 
@@ -143,27 +141,48 @@ let interpret_predicate env ~on_model ~on_dataset task =
        { t_node = Tconst (Constant.ConstStr p); _ };
        { t_node = Tconst (Constant.ConstStr ctp); _ };
        { t_node = Tconst (Constant.ConstStr om); _ };
-       { t_node = Tconst (Constant.ConstInt start); _ };
-       { t_node = Tconst (Constant.ConstInt stop); _ };
-       { t_node = Tconst (Constant.ConstInt step); _ };
+       ampli_node;
       ] ->
         let meta_robust_predicate = find_predicate_ls env "meta_robust" in
+        let some_ls = find_option_ls env "Some" in
+        let none_ls = find_option_ls env "None" in
         let f = float_of_real_constant e in
         if Term.ls_equal ls meta_robust_predicate
         then
-          MetaRobust
-            ( f,
-              {
-                perturbation = p;
-                ctp;
-                om;
-                amplitude =
-                  {
-                    start = Some (Number.to_small_integer start);
-                    stop = Number.to_small_integer stop;
-                    step = Some (Number.to_small_integer step);
-                  };
-              } )
+          let ampli =
+            match ampli_node with
+            | {
+             t_node =
+               Term.Tapp
+                 ( option_ls,
+                   [
+                     {
+                       t_node =
+                         Term.Tapp
+                           ( _,
+                             [
+                               { t_node = Tconst (Constant.ConstInt start); _ };
+                               { t_node = Tconst (Constant.ConstInt stop); _ };
+                               { t_node = Tconst (Constant.ConstInt step); _ };
+                             ] );
+                       _;
+                     };
+                   ] );
+             _;
+            }
+              when Term.ls_equal option_ls some_ls ->
+              Some
+                {
+                  start = Number.to_small_integer start;
+                  stop = Number.to_small_integer stop;
+                  step = Number.to_small_integer step;
+                }
+            | { t_node = Term.Tapp (option_ls, _); _ }
+              when Term.ls_equal option_ls none_ls ->
+              None
+            | _ -> failwith_unsupported_term ampli_node
+          in
+          MetaRobust (f, { perturbation = p; ctp; om; amplitude = ampli })
         else failwith_unsupported_ls ls
       | _ -> failwith_unsupported_term term
     in

src/dataset.mli

@@ -30,13 +30,15 @@ val term_of_eps : Env.env -> eps -> Term.term
 
 type threshold [@@deriving yojson, show]
 
-type amplitude = {
-  start : int option;
+type amplitude_record = {
+  start : int;
   stop : int;
-  step : int option;
+  step : int;
 }
 [@@deriving yojson, show]
 
+type amplitude = amplitude_record option [@@deriving yojson, show]
+
 type aimos_params = {
   perturbation : string;
   ctp : string;

stdlib/caisar.mlw

@@ -24,11 +24,14 @@ theory DatasetClassification
   use ieee_float.Float64
   use int.Int
   use array.Array
+  use option.Option
 
   type features = array t
   type label_ = int
   type record = (features, label_)
   type dataset = array record
+  type amplitude_record = { start: int; stop: int; step: int }
+  type amplitude = option amplitude_record
 
   constant dataset: dataset
 
@@ -69,7 +72,7 @@ theory DatasetClassificationProps
   predicate cond_robust (m: model) (d: dataset) (eps: t) =
     correct m d /\ robust m d eps
 
-  predicate meta_robust (m: model) (d: dataset) (threshold: t) (perturbation: string) (pert_path: string) (out_mode: string) (start: int) (stop: int) (step: int)
+  predicate meta_robust (m: model) (d: dataset) (threshold: t) (perturbation: string) (pert_path: string) (out_mode: string) (ampli: amplitude)
 end
 
 theory NN

tests/aimos.t

@@ -16,8 +16,9 @@ Test verify
   >   use ieee_float.Float64
   >   use caisar.DatasetClassification
   >   use caisar.DatasetClassificationProps
+  >   use option.Option
   > 
-  >   goal G: meta_robust model dataset (1.0:t) ("reluplex_rotation":string) ("config/custom_transformations.py":string) ("classif_min":string) (0:int) (0:int) (0:int)
+  >   goal G: meta_robust model dataset (1.0:t) "reluplex_rotation" "config/custom_transformations.py" "classif_min" None
   > end
   > EOF
   Goal G: Valid