Whippersnapper

synthesis/bin/Main.ml

@@ -527,6 +527,202 @@ let onf_real : Command.t =
     ONFReal.spec
     ONFReal.run
 
+module ToOBT = struct
+  let spec = Command.Spec.(
+      empty
+      +> flag "-DEBUG" no_arg ~doc:"print debugging statements"
+      +> flag "--thrift" no_arg ~doc:"parse & write bmv2/thrift commands"
+      +> flag "-i" no_arg ~doc:"interactive mode"
+      +> flag "-data" (required string) ~doc:"the input log"
+      +> flag "-p" no_arg ~doc:"show_result_at_end"
+      +> anon ("p4file" %: string)
+      +> anon ("log-edits" %: string)
+      +> anon ("phys-edits" %: string)
+      +> anon ("fvs" %: string)
+      +> anon ("assume" %: string)
+      +> flag "-I" (listed string) ~doc:"<dir> add directory to include search path for file"
+      ++ opt_flags)
+
+let run debug thrift_mode interactive data print
+        p4file log_edits phys_edits fvs assume inc
+        widening
+        do_slice
+        semantic_slicing
+        edits_depth
+        search_width
+        monotonic
+        injection
+        fastcx
+        vcache
+        ecache
+        shortening
+        above
+        minimize
+        hints
+        only_holes
+        allow_annotations
+        nlp
+        unique_edits
+        domain
+        restrict_mask
+        no_defaults
+        no_deletes
+        use_all_cexs
+        reach_restrict
+        reach_filter
+        hot_start
+    () =
+    let res = Benchmark.to_obt
+              Parameters.({
+          widening;
+          do_slice;
+          semantic_slicing;
+          edits_depth;
+          search_width;
+          debug;
+          thrift_mode;
+          monotonic;
+          interactive;
+          injection;
+          fastcx;
+          vcache;
+          ecache;
+          shortening;
+          above;
+          minimize;
+          hints = Option.is_some hints;
+          hint_type = Option.value hints ~default:"exact";
+          only_holes;
+          allow_annotations;
+          nlp;
+          unique_edits;
+          domain;
+          restrict_mask;
+          no_defaults;
+          no_deletes;
+          use_all_cexs;
+          reach_restrict;
+          reach_filter;
+          timeout = None;
+          hot_start})
+              data p4file log_edits phys_edits fvs assume inc
+    in
+    match res with
+    | None -> Core.Printf.printf "no example could be found\n"
+    | Some r when print ->
+       Core.Printf.printf "Edits\n";
+       List.iter r ~f:(fun edit ->
+           Tables.Edit.to_string edit
+           |> Core.Printf.printf "%s\n%!"
+         )
+    | Some _ -> ()
+
+end
+
+let to_obt : Command.t =
+  Command.basic_spec
+    ~summary: "Run the onf benchmark on the real p4 programs"
+    ToOBT.spec
+    ToOBT.run
+
+module FromOBT = struct
+  let spec = Command.Spec.(
+      empty
+      +> flag "-DEBUG" no_arg ~doc:"print debugging statements"
+      +> flag "--thrift" no_arg ~doc:"parse & write bmv2/thrift commands"
+      +> flag "-i" no_arg ~doc:"interactive mode"
+      +> flag "-data" (required string) ~doc:"the input log"
+      +> flag "-p" no_arg ~doc:"show_result_at_end"
+      +> anon ("p4file" %: string)
+      +> anon ("log-edits" %: string)
+      +> anon ("phys-edits" %: string)
+      +> anon ("fvs" %: string)
+      +> anon ("assume" %: string)
+      +> flag "-I" (listed string) ~doc:"<dir> add directory to include search path for file"
+      ++ opt_flags)
+
+let run debug thrift_mode interactive data print
+        p4file log_edits phys_edits fvs assume inc
+        widening
+        do_slice
+        semantic_slicing
+        edits_depth
+        search_width
+        monotonic
+        injection
+        fastcx
+        vcache
+        ecache
+        shortening
+        above
+        minimize
+        hints
+        only_holes
+        allow_annotations
+        nlp
+        unique_edits
+        domain
+        restrict_mask
+        no_defaults
+        no_deletes
+        use_all_cexs
+        reach_restrict
+        reach_filter
+        hot_start
+    () =
+    let res = Benchmark.from_obt
+              Parameters.({
+          widening;
+          do_slice;
+          semantic_slicing;
+          edits_depth;
+          search_width;
+          debug;
+          thrift_mode;
+          monotonic;
+          interactive;
+          injection;
+          fastcx;
+          vcache;
+          ecache;
+          shortening;
+          above;
+          minimize;
+          hints = Option.is_some hints;
+          hint_type = Option.value hints ~default:"exact";
+          only_holes;
+          allow_annotations;
+          nlp;
+          unique_edits;
+          domain;
+          restrict_mask;
+          no_defaults;
+          no_deletes;
+          use_all_cexs;
+          reach_restrict;
+          reach_filter;
+          timeout = None;
+          hot_start})
+              data p4file log_edits phys_edits fvs assume inc
+    in
+    match res with
+    | None -> Core.Printf.printf "no example could be found\n"
+    | Some r when print ->
+       Core.Printf.printf "Edits\n";
+       List.iter r ~f:(fun edit ->
+           Tables.Edit.to_string edit
+           |> Core.Printf.printf "%s\n%!"
+         )
+    | Some _ -> ()
+
+end
+
+let from_obt : Command.t =
+  Command.basic_spec
+    ~summary: "Run the onf benchmark on the real p4 programs"
+    FromOBT.spec
+    FromOBT.run
+
 module Equality = struct
   let spec = Command.Spec.(
       empty
@@ -1417,6 +1613,8 @@ let main : Command.t =
     ; ("onf-real", onf_real)
     ; ("obt", obt)
     ; ("obt-real", obt_real)
+    ; ("to-obt", to_obt)
+    ; ("from-obt", from_obt)
     ; ("eq", equality)
     ; ("eq-real", equality_real)
     ; ("wp", wp_cmd)]

synthesis/lib/Benchmark.ml

@@ -225,6 +225,63 @@ let rec basic_onf_ipv4_real params data_file log_p4 phys_p4 log_edits_file phys_
   assert (implements params (ProfData.zero ()) (problem ()) = `Yes);
   measure params None problem (onos_to_edits var_mapping data_file "routing_v6" "hdr.ipv6.dst_addr")
 
+and to_obt params data_file p4_file log_edits_file phys_edits_file fvs_file _ inc =
+  let var_mapping = parse_fvs fvs_file in
+  let fvs = List.map var_mapping ~f:snd in
+  let assume = Skip (* parse_file assume_file *) in
+
+  (* let print_fvs = printf "fvs = %s" (Sexp.to_string ([%sexp_of: (string * int) list] fvs)) in *)
+
+  let log = (assume %:% Encode.encode_from_p4 inc p4_file false)
+            |> Encode.unify_names var_mapping |> zero_init fvs |> drop_handle fvs in
+
+  let phys = OneBigTable.mk_one_big_table (ConstantProp.propogate log) |> zero_init fvs |> drop_handle fvs in
+             (* |> CompilerOpts.optimize fvs *)
+  (* let maxN n = Bigint.(of_int_exn n ** of_int_exn 2 - one) in *)
+  (* let fvs = parse_fvs fvs in *)
+  let log_edits = Runtime.parse_whippersnapper log log_edits_file in
+  let phys_edits = Runtime.parse phys phys_edits_file in
+
+  let problem =
+    Problem.make
+      ~log  ~phys ~fvs
+      ~log_inst:Instance.(update_list params empty log_edits)
+      ~phys_inst:Instance.(update_list params empty phys_edits)
+      ~log_edits:[]
+  in
+  (* Core.Printf.printf "\n\n------------\n%s\n----------\n" (Problem.to_string params problem); *)
+  assert (implements params (ProfData.zero ()) (problem ()) = `Yes);
+  measure params None problem (List.map (Runtime.parse_whippersnapper log data_file) ~f:(fun r -> [r]))
+
+and from_obt params data_file p4_file log_edits_file phys_edits_file fvs_file _ inc =
+  let var_mapping = parse_fvs fvs_file in
+  let fvs = List.map var_mapping ~f:snd in
+  let assume = Skip (* parse_file assume_file *) in
+
+  (* let print_fvs = printf "fvs = %s" (Sexp.to_string ([%sexp_of: (string * int) list] fvs)) in *)
+
+  let phys = (assume %:% Encode.encode_from_p4 inc p4_file false)
+            |> Encode.unify_names var_mapping |> zero_init fvs |> drop_handle fvs in
+
+  let log = OneBigTable.mk_one_big_table (ConstantProp.propogate phys) |> zero_init fvs |> drop_handle fvs in
+             (* |> CompilerOpts.optimize fvs *)
+  (* let maxN n = Bigint.(of_int_exn n ** of_int_exn 2 - one) in *)
+  (* let fvs = parse_fvs fvs in *)
+  let log_edits = Runtime.parse_whippersnapper log log_edits_file in
+  let phys_edits = Runtime.parse phys phys_edits_file in
+
+  let problem =
+    Problem.make
+      ~log  ~phys ~fvs
+      ~log_inst:Instance.(update_list params empty log_edits)
+      ~phys_inst:Instance.(update_list params empty phys_edits)
+      ~log_edits:[]
+  in
+  (* Core.Printf.printf "\n\n------------\n%s\n----------\n" (Problem.to_string params problem); *)
+  assert (implements params (ProfData.zero ()) (problem ()) = `Yes);
+  measure params None problem (List.map (Runtime.parse log data_file) ~f:(fun r -> [r]))
+
+
 and zero_init fvs cmd =
   let fvs = StringSet.of_list @@ fsts @@ fvs in
   let vs = free_of_cmd `Var cmd

synthesis/lib/FastCX.ml

@@ -41,8 +41,8 @@ let is_reachable encode_tag params problem fvs in_pkt tbl_name keys =
   passive_hoare_triple ~fvs
     (Packet.to_test in_pkt ~fvs)
     trunc
-    (Hole.match_holes_table encode_tag tbl_name keys
-     %&% Instance.negate_rows phys_inst tbl_name)
+    (Hole.match_holes_table encode_tag tbl_name keys)
+     (* %&% Instance.negate_rows phys_inst tbl_name) *)
 
 
 let hits_pred params (_: ProfData.t ref) prog inst edits e : test =