<commit_before>(********************************************************
   This file is part of jStar 
	src/prover/smt.ml
   Release 
        $Release$
   Version 
        $Rev$
   $Copyright$
   
   jStar is distributed under a BSD license,  see, 
      LICENSE.txt
 ********************************************************)
 
(*
SMT TODO list: 

- mark things that are constructors as such in the term structure; 
  at the moment they're treated as predicates. 
  
- get rid of some of the gratuatous calls to the Format module & 
  do all the sexp construction through string-catenation 
  
- check that the SMT has started correctly; at the moment this is 
  assumed and a fault is raised only when the prover tries to read 
  the SMT's output. 

*)

open Psyntax
open Clogic
open Cterm
open Congruence
open Unix
open List
open Smtsyntax

exception SMT_error of string
exception SMT_fatal_error

(*let Config.smt_run = ref true;; *)
let smt_fdepth = ref 0;; 
let smtout = ref Pervasives.stdin;; 
let smtin = ref Pervasives.stderr;;
let smterr = ref Pervasives.stdin;;

let smtout_lex = ref (Lexing.from_string "");; 


let smt_init () : unit = 
  let path = ( if (!Config.solver_path <> "") then !Config.solver_path 
               else System.getenv "JSTAR_SMT_PATH")
  in 
  if path = "" then Config.smt_run := false
  else
    try 
      begin
        if Config.smt_debug() then Format.printf "Initialising SMT@\n"; 
        let s = Unix.stat path in 
        let args = System.getenv "JSTAR_SMT_ARGUMENTS" in 
        let command = Filename.quote path ^ " " ^ args in 
        let o, i, e = Unix.open_process_full command (environment()) in 
        smtout := o;  smtin := i;  smterr := e;
        smtout_lex := Lexing.from_channel !smtout; 
        Config.smt_run := true; 
        if Config.smt_debug() then Format.printf "SMT running...@\n"
      end 
    with 
    | Unix_error(err,f,a) -> 
      match err with 
      | ENOENT -> Format.printf "@,@{<b>ERROR:@} Bad path for SMT solver: %s@," a; 
                  Config.smt_run := false 
      | _ -> raise (Unix_error(err,f,a))


let smt_fatal_recover () : unit  = 
  Format.printf "@,@{<b>SMT ERROR:@} "; 
  Format.printf "Oh noes! The SMT solver died for some reason. This shouldn't happen.@,"; 
  if Config.smt_debug() then 
    begin
      Format.printf "Error report from the solver:@\n";
      try while true do Format.printf "%s@\n" (input_line !smterr) done
      with End_of_file -> ()
    end; 
  Format.printf "Turning off SMT for this example...@]"; 
  Unix.close_process_full (!smtout, !smtin, !smterr); 
  Format.printf "SMT off.@\n"; 
  Format.print_flush(); 
  Config.smt_run := false 



(* concatenate n instances of string s *)
let rec nstr (s : string) (n : int) : string =
  match n with 
  | 0 -> ""
  | _ -> s^(nstr s (n-1))
  
  
(* Partition a list into sublists of equal elements *)
let rec equiv_partition
    (eq : 'a -> 'a -> bool) 
    (xs : 'a list)
    : 'a list list = 
  match xs with 
  | x::xs -> 
     let (e, xs') = partition (eq x) xs in 
     let eqs = equiv_partition eq xs' in 
     (x::e) :: eqs
  | [] -> []


(* construct all (unordered) pairs of list elements *)
let rec list_to_pairs 
    (xs : 'a list) 
    : ('a * 'a) list = 
  match xs with 
  | x::xs -> (map (fun y -> (x,y)) xs) @ list_to_pairs xs
  | [] -> [] 


(* munge out input characters that make z3 die horribly *)
(* We should probably handle this in a more principled way *)

let cmd_munge (s : string) : string = 
  let s = Str.global_replace (Str.regexp "[@\$]") "AT_" s in
  s
  
let str_munge (s : string ) : string = 
  let s = Str.global_replace (Str.regexp "[<> @\*]")  "_" s in
  s


(* Datatype to hold smt type annotations *)

type smt_type = 
  | SMT_Var of Vars.var
  | SMT_Pred of string * int 
  | SMT_Op of string * int


module SMTTypeSet = 
  Set.Make(struct
    type t = smt_type
    let compare = compare
  end)
type smttypeset = SMTTypeSet.t


let smt_union_list (l : smttypeset list) : smttypeset = 
  fold_right SMTTypeSet.union l SMTTypeSet.empty        

let rec args_smttype (arg : Psyntax.args) : smttypeset = 
  match arg with
  | Arg_var v -> SMTTypeSet.singleton (SMT_Var(v)) 
  | Arg_string s -> 
          let rxp = (Str.regexp "^\(-?[0-9]+\)") in 
          if Str.string_match rxp s 0 then SMTTypeSet.empty 
          else SMTTypeSet.singleton (SMT_Op("string_const_"^(str_munge s), 0))

  | Arg_op ("builtin_plus",_) -> SMTTypeSet.empty
  | Arg_op ("builtin_minus",_) -> SMTTypeSet.empty
  | Arg_op ("builtin_mult",_) -> SMTTypeSet.empty

  | Arg_op (name, args) -> 
          let s = SMTTypeSet.singleton (SMT_Op(("op_"^name), (length args))) in 
          smt_union_list (s::(map args_smttype args))
  | Arg_cons (name, args) -> smt_union_list (map args_smttype args)
  | Arg_record fldlist -> SMTTypeSet.empty


(* Functions to convert various things to sexps & get types *)

let rec string_sexp_args (arg : Psyntax.args) : string = 
  match arg with 
  | Arg_var v -> Vars.string_var v
  | Arg_string s -> 
          let rxp = (Str.regexp "^\(-?[0-9]+\)") in 
          if Str.string_match rxp s 0 then (Str.matched_group 1 s)
          else "string_const_"^(str_munge s)
  <commit_msg>Fixed SMT type bug<commit_after>(********************************************************
   This file is part of jStar 
	src/prover/smt.ml
   Release 
        $Release$
   Version 
        $Rev$
   $Copyright$
   
   jStar is distributed under a BSD license,  see, 
      LICENSE.txt
 ********************************************************)
 
(*
SMT TODO list: 

- mark things that are constructors as such in the term structure; 
  at the moment they're treated as predicates. 
  
- get rid of some of the gratuatous calls to the Format module & 
  do all the sexp construction through string-catenation 
  
- check that the SMT has started correctly; at the moment this is 
  assumed and a fault is raised only when the prover tries to read 
  the SMT's output. 

*)

open Psyntax
open Clogic
open Cterm
open Congruence
open Unix
open List
open Smtsyntax

exception SMT_error of string
exception SMT_fatal_error

(*let Config.smt_run = ref true;; *)
let smt_fdepth = ref 0;; 
let smtout = ref Pervasives.stdin;; 
let smtin = ref Pervasives.stderr;;
let smterr = ref Pervasives.stdin;;

let smtout_lex = ref (Lexing.from_string "");; 


let smt_init () : unit = 
  let path = ( if (!Config.solver_path <> "") then !Config.solver_path 
               else System.getenv "JSTAR_SMT_PATH")
  in 
  if path = "" then Config.smt_run := false
  else
    try 
      begin
        if Config.smt_debug() then Format.printf "Initialising SMT@\n"; 
        let s = Unix.stat path in 
        let args = System.getenv "JSTAR_SMT_ARGUMENTS" in 
        let command = Filename.quote path ^ " " ^ args in 
        let o, i, e = Unix.open_process_full command (environment()) in 
        smtout := o;  smtin := i;  smterr := e;
        smtout_lex := Lexing.from_channel !smtout; 
        Config.smt_run := true; 
        if Config.smt_debug() then Format.printf "SMT running...@\n"
      end 
    with 
    | Unix_error(err,f,a) -> 
      match err with 
      | ENOENT -> Format.printf "@,@{<b>ERROR:@} Bad path for SMT solver: %s@," a; 
                  Config.smt_run := false 
      | _ -> raise (Unix_error(err,f,a))


let smt_fatal_recover () : unit  = 
  Format.printf "@,@{<b>SMT ERROR:@} "; 
  Format.printf "Oh noes! The SMT solver died for some reason. This shouldn't happen.@,"; 
  if Config.smt_debug() then 
    begin
      Format.printf "Error report from the solver:@\n";
      try while true do Format.printf "%s@\n" (input_line !smterr) done
      with End_of_file -> ()
    end; 
  Format.printf "Turning off SMT for this example...@]"; 
  Unix.close_process_full (!smtout, !smtin, !smterr); 
  Format.printf "SMT off.@\n"; 
  Format.print_flush(); 
  Config.smt_run := false 



(* concatenate n instances of string s *)
let rec nstr (s : string) (n : int) : string =
  match n with 
  | 0 -> ""
  | _ -> s^(nstr s (n-1))
  
  
(* Partition a list into sublists of equal elements *)
let rec equiv_partition
    (eq : 'a -> 'a -> bool) 
    (xs : 'a list)
    : 'a list list = 
  match xs with 
  | x::xs -> 
     let (e, xs') = partition (eq x) xs in 
     let eqs = equiv_partition eq xs' in 
     (x::e) :: eqs
  | [] -> []


(* construct all (unordered) pairs of list elements *)
let rec list_to_pairs 
    (xs : 'a list) 
    : ('a * 'a) list = 
  match xs with 
  | x::xs -> (map (fun y -> (x,y)) xs) @ list_to_pairs xs
  | [] -> [] 


(* munge out input characters that make z3 die horribly *)
(* We should probably handle this in a more principled way *)

let cmd_munge (s : string) : string = 
  let s = Str.global_replace (Str.regexp "[@\$]") "AT_" s in
  s
  
let str_munge (s : string ) : string = 
  let s = Str.global_replace (Str.regexp "[<> @\*]")  "_" s in
  s


(* Datatype to hold smt type annotations *)

type smt_type = 
  | SMT_Var of Vars.var
  | SMT_Pred of string * int 
  | SMT_Op of string * int


module SMTTypeSet = 
  Set.Make(struct
    type t = smt_type
    let compare = compare
  end)
type smttypeset = SMTTypeSet.t


let smt_union_list (l : smttypeset list) : smttypeset = 
  fold_right SMTTypeSet.union l SMTTypeSet.empty        

let rec args_smttype (arg : Psyntax.args) : smttypeset = 
  match arg with
  | Arg_var v -> SMTTypeSet.singleton (SMT_Var(v)) 
  | Arg_string s -> 
          let rxp = (Str.regexp "^\(-?[0-9]+\)") in 
          if Str.string_match rxp s 0 then SMTTypeSet.empty 
          else SMTTypeSet.singleton (SMT_Op("string_const_"^(str_munge s), 0))

  | Arg_op ("builtin_plus",args) -> smt_union_list (map args_smttype args)
  | Arg_op ("builtin_minus",args) -> smt_union_list (map args_smttype args)
  | Arg_op ("builtin_mult",args) -> smt_union_list (map args_smttype args)

  | Arg_op (name, args) -> 
          let s = SMTTypeSet.singleton (SMT_Op(("op_"^name), (length args))) in 
          smt_union_list (s::(map args_smttype args))
  | Arg_cons (name, args) -> smt_union_list (map args_smttype args)
  | Arg_record fldlist -> SMTTypeSet.empty


(* Functions to convert various things to sexps & get types *)

let rec string_sexp_args (arg : Psyntax.args) : string = 
  match arg with 
  | Arg_var v -> Vars.string_var v
  | Arg_string s -> 
          let rxp = (Str.regexp "^\(-?[0-9]+\)") in 
          if Str.string_match rxp s 0 then (Str.matched_group 1 s)
          else "string_const_"^(str_munge s)
  
{'fraction_non_alphanumeric': 0.13837497615868777, 'fraction_numerical': 0.0022887659736791914, 'mean_word_length': 2.726723525230988, 'pattern_counts': {'":': 0, '<': 11, '<?xml version=': 0, '>': 57, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '1257223', 'n_tokens_mistral': 3885, 'n_tokens_neox': 3636, 'n_words': 1134}