add sicstus proxy

.gitignore

@@ -14,3 +14,4 @@ _obuild
 *.markdown
 gen/*
 testdir_*
+oracle

runtime/dune

@@ -1,7 +1,5 @@
-(include_subdirs unqualified)
-
 (library
-  (public_name testify_runtime)
-  (name testify_runtime)
-  (foreign_stubs (language c) (names sicstus_stubs))
-  (libraries qcheck arbogen))
+ (public_name testify_runtime)
+ (name testify_runtime)
+ (libraries sicstus_proxy qcheck arbogen)
+)

runtime/sicstus/old_setup/sicstus.ml

@@ -0,0 +1,32 @@
+(* external get_increasing_list : int -> int -> int list
+ *   = "stub_sicstus_get_increasing_list"
+ *
+ * external get_decreasing_list : int -> int -> int list
+ *   = "stub_sicstus_get_decreasing_list"
+ *
+ * external get_increasing_strict_list : int -> int -> int list
+ *   = "stub_sicstus_get_increasing_strict_list"
+ *
+ * external get_decreasing_strict_list : int -> int -> int list
+ *   = "stub_sicstus_get_decreasing_strict_list"
+ *
+ * external get_alldiff_list : int -> int -> int list
+ *   = "stub_sicstus_get_alldiff_list"
+ *
+ * external initialize : unit -> unit = "stub_sicstus_initialize"
+ *
+ * let () = initialize () *)
+
+(* let () =
+ *   let pp_list fmt l =
+ *     Format.fprintf fmt "@[<h>%a@]"
+ *       Format.(pp_print_list ~pp_sep:pp_print_space pp_print_int)
+ *       l
+ *   in
+ *   Format.printf "increasing list: %a@." pp_list (get_increasing_list 10 0) ;
+ *   Format.printf "decreasing list: %a@." pp_list (get_decreasing_list 10 0) ;
+ *   Format.printf "increasing strict list: %a@." pp_list
+ *     (get_increasing_strict_list 10 0) ;
+ *   Format.printf "decreasing strict list: %a@." pp_list
+ *     (get_decreasing_strict_list 10 0) ;
+ *   Format.printf "all diff list: %a@." pp_list (get_alldiff_list 10 0) *)

runtime/sicstus/old_setup/sicstus_stubs.c

@@ -0,0 +1,71 @@
+#include <stdio.h>
+#include <stdlib.h>
+
+#define CAML_NAME_SPACE
+
+#include <caml/mlvalues.h>
+#include <caml/memory.h>
+#include <caml/alloc.h>
+#include <caml/custom.h>
+#include <sicstus/sicstus.h>
+#include <prt.h>
+
+value to_caml_list(SP_term_ref seq){
+  CAMLparam0 ();
+  CAMLlocal1 (r);
+
+  SP_term_ref head = SP_new_term_ref();
+  SP_term_ref tail = SP_new_term_ref();
+  int res = SP_get_list(seq, head, tail);
+  if (res == 0)
+    r = Val_emptylist;
+  else {
+    r = caml_alloc_small(2, 0);
+    SP_integer itg;
+    SP_get_integer(head, &itg);
+    Field(r, 0) = Val_int(itg);
+    Field(r, 1) = to_caml_list(tail);
+  }
+  CAMLreturn(r);
+}
+
+CAMLprim value stub_sicstus_get_increasing_list(value length, value seed){
+  CAMLparam2(length, seed);
+  SP_term_ref l = sicstus_increasing_list(Int_val(length), Int_val(seed));
+  value lml = to_caml_list(l);
+  // How to free l ? Can/Should we ?
+  CAMLreturn(lml);
+}
+
+CAMLprim value stub_sicstus_get_decreasing_list(value length, value seed){
+  CAMLparam2(length, seed);
+  SP_term_ref l = sicstus_decreasing_list(Int_val(length), Int_val(seed));
+  value lml = to_caml_list(l);
+  CAMLreturn(lml);
+}
+
+CAMLprim value stub_sicstus_get_increasing_strict_list(value length, value seed){
+  CAMLparam2(length, seed);
+  SP_term_ref l = sicstus_increasing_strict_list(Int_val(length), Int_val(seed));
+  value lml = to_caml_list(l);
+  CAMLreturn(lml);
+}
+
+CAMLprim value stub_sicstus_get_decreasing_strict_list(value length, value seed){
+  CAMLparam2(length, seed);
+  SP_term_ref l = stub_sicstus_get_decreasing_strict_list(Int_val(length), Int_val(seed));
+  value lml = to_caml_list(l);
+  CAMLreturn(lml);
+}
+
+CAMLprim value stub_sicstus_get_alldiff_list(value length, value seed){
+  CAMLparam2(length, seed);
+  SP_term_ref l = sicstus_alldiff_list(Int_val(length), Int_val(seed));
+  value lml = to_caml_list(l);
+  CAMLreturn(lml);
+}
+
+CAMLprim value stub_sicstus_initialize(value unit) {
+  sicstus_prt_initialize(0, NULL);
+  return Val_unit;
+}

runtime/sicstus/old_setup/test.c

@@ -0,0 +1,7 @@
+#include <prt.h>
+
+int main(){
+
+  test();
+  return 0;
+}

runtime/sicstus/sicstus_oracle/Makefile

@@ -0,0 +1,13 @@
+SPLD=/usr/local/sicstus4.7.1/bin/spld
+SICSTUS=/usr/local/sicstus4.7.1/bin/sicstus
+
+all: oracle
+
+oracle: prt.c oracle.c prt.sav
+	@$(SPLD) --main=user --resources=prt.sav=/prt.sav prt.c oracle.c -o oracle
+
+prt.sav: prt.pl
+	@$(SICSTUS) --goal "compile(prt), save_program('prt.sav'), halt." --noinfo --nologo
+
+clean:
+	@rm -rf oracle prt.sav

runtime/sicstus/sicstus_oracle/dune

@@ -0,0 +1,14 @@
+(rule
+ (deps (source_tree .))
+ (targets ghost.ml)
+ (action (progn
+          (system make)
+          (run touch ghost.ml)))
+)
+
+(library
+ (name sicstus_proxy)
+ (public_name sicstus_proxy)
+ (libraries lwt.unix)
+ (modules Proxy Ghost)
+)

runtime/sicstus/sicstus_oracle/oracle.c

@@ -0,0 +1,87 @@
+#include <stdio.h>
+#include <stdlib.h>
+#include "prt.h"
+
+#define MAX 128
+
+#ifdef DEBUG
+#define DEBUG_TEST 1
+#else
+#define DEBUG_TEST 0
+#endif
+#define LOG(X...)\
+            do { if (DEBUG_TEST) fprintf(stderr, X); } while (0)
+
+unsigned char buff[MAX];
+
+void output_list(SP_term_ref list, int nb){
+  SP_term_ref head = SP_new_term_ref();
+  SP_term_ref tail = SP_new_term_ref();
+  SP_integer itg;
+  int i;
+  for (i = 0; i < nb; i++){
+    SP_get_list(list, head, tail);
+    SP_get_integer(head, &itg);
+    int j = write(1, &itg, 4);
+    list = tail;
+  }
+  fflush(stdout);
+  LOG("wrote %d bytes\n", nb * 4);
+}
+
+// writes length and seed
+void setup (int fd, sint* length, sint* seed){
+  int i = read(fd, buff, 4);
+  *length = (buff[0] << 8) + buff[1];
+  *seed = (buff[2] << 8) + buff[3];
+}
+
+// dispatch the request to the corresponding sictus functionnality
+void answer(int fd){
+  bzero(buff, MAX);
+  int i = read(fd, buff, 1);
+  sint length;
+  sint seed;
+  SP_term_ref list;
+  switch(buff[0]){
+  case 1:
+    LOG("exiting\n");
+    exit(0);
+  case 2:
+    setup(fd, &length, &seed);
+    list = sicstus_increasing_list(length, seed);
+    break;
+  case 3:
+    setup(fd, &length, &seed);
+    list = sicstus_decreasing_list(length, seed);
+    break;
+  case 4:
+    setup(fd, &length, &seed);
+    list = sicstus_increasing_strict_list(length, seed);
+    break;
+  case 5:
+    setup(fd, &length, &seed);
+    list = sicstus_decreasing_strict_list(length, seed);
+    break;
+  case 6:
+    setup(fd, &length, &seed);
+    list = sicstus_alldiff_list(length, seed);
+    break;
+  default:
+    LOG("unrecognized message %d\n", buff[0]);
+    exit (0);
+    break;
+  }
+  output_list(list, length);
+  fflush(stdin);
+}
+
+// main loop
+int user_main(int argc, char **argv){
+  LOG("starting\n");
+  sicstus_prt_initialize(argc, argv);
+  for (;;){
+    answer(0);
+  }
+  return 0;
+}

runtime/sicstus/sicstus_oracle/proxy.ml

@@ -0,0 +1,91 @@
+let debug = ref false
+
+let seed = ref 0
+
+let set_seed x = seed := x
+
+let log x =
+  if !debug then (Format.printf "[proxy] " ; Format.printf x)
+  else Format.ifprintf Format.std_formatter x
+
+let out_buff = Bytes.create (1 + 2 + 2)
+
+let in_buff = Bytes.create ((1 lsl 16) * 4)
+
+type global_constraint =
+  | Increasing_list
+  | Decreasing_list
+  | Increasing_strict_list
+  | Decreasing_strict_list
+  | Alldiff_list
+
+let gc_opcode = function
+  | Increasing_list -> '\002'
+  | Decreasing_list -> '\003'
+  | Increasing_strict_list -> '\004'
+  | Decreasing_strict_list -> '\005'
+  | Alldiff_list -> '\006'
+
+let exit_code = '\001'
+
+let process =
+  lazy
+    (let () = Unix.putenv "LD_LIBRARY_PATH" "/usr/local/sicstus4.7.1/lib" in
+     let ((p_out, p_in) as process) = Unix.open_process "./oracle" in
+     let pid = Unix.process_pid process in
+     let p_out, p_in =
+       (Unix.descr_of_in_channel p_out, Unix.descr_of_out_channel p_in)
+     in
+     at_exit (fun () ->
+         log "terminating sicstus process@." ;
+         Bytes.set out_buff 0 '\001' ;
+         Unix.write p_in out_buff 0 1 |> ignore ;
+         Unix.waitpid [] pid |> ignore ) ;
+     log "sicstus process started (pid: %d)@." pid ;
+     (p_out, p_in) )
+
+let really_read p_out n =
+  let rec loop ofs =
+    if ofs = n then (log "end reading@." ; ())
+    else (
+      log "try reading %d at ofs %d@." (n - ofs) ofs ;
+      let nb = Unix.read p_out in_buff ofs (n - ofs) in
+      log "read %d, %d left to read@." nb (ofs + nb) ;
+      if nb = 0 then raise End_of_file else loop (ofs + nb) )
+  in
+  loop 0
+
+let call_sicstus length seed gc =
+  let p_out, p_in = Lazy.force process in
+  Bytes.set out_buff 0 (gc_opcode gc) ;
+  Bytes.set_int16_be out_buff 1 length ;
+  Bytes.set_int16_be out_buff (1 + 2) seed ;
+  Unix.write p_in out_buff 0 5 |> log "wrote %d@." ;
+  really_read p_out (4 * length) ;
+  List.init length (fun i ->
+      Bytes.get_int32_le in_buff (i * 4) |> Int32.to_int )
+
+let increasing_list ?(seed = !seed) length =
+  call_sicstus length seed Increasing_list
+
+let increasing_strict_list ?(seed = !seed) length =
+  call_sicstus length seed Increasing_strict_list
+
+let decreasing_list ?(seed = !seed) length =
+  call_sicstus length seed Decreasing_list
+
+let decreasing_strict_list ?(seed = !seed) length =
+  call_sicstus length seed Decreasing_strict_list
+
+let all_diff_list ?(seed = !seed) length =
+  call_sicstus length seed Decreasing_strict_list
+
+let test () =
+  Random.self_init () ;
+  let length () = Random.int (1 lsl 3) in
+  let pp_list l = log "@[<v>%a@]@." Format.(pp_print_list pp_print_int) l in
+  pp_list @@ increasing_list (length ()) ;
+  pp_list @@ increasing_strict_list (length ()) ;
+  pp_list @@ decreasing_list (length ()) ;
+  pp_list @@ decreasing_strict_list (length ()) ;
+  pp_list @@ all_diff_list (length ())