Commit 9a51df55 authored by Sylvain Dailler's avatar Sylvain Dailler

refactoring ce: Value in the else branch of ite are now queried

This commit clean some of the spark specific code for ce replacing it with
more modular algorihtm.
Some type are now given by the model parser in order to get the variables
that are updated by an else branch.
parent 706822ae
......@@ -3,11 +3,12 @@ ce/int32.mlw Ce_int32 WP_parameter dummy_update : Valid
ce/int32.mlw Ce_int32 WP_parameter dummy_update : Unknown (other)
Counter-example model:File int32.mlw:
Line 6:
r = {"type" : "Integer" ,
"val" : "22" }
r = {"type" : "Integer" , "val" : "22" }
Line 8:
the check fails with all inputs
r = {"type" : "Integer" , "val" : "84" }
Line 9:
r = {"type" : "Integer" , "val" : "42" }
Line 10:
r = {"type" : "Integer" ,
"val" : "42" }
"val" : "84" }
......@@ -11,10 +11,17 @@
open Stdlib
open Smt2_model_defs
open Strings
exception Not_value
(* Printing function *)
let print_table t =
Format.eprintf "Table key and value@.";
Mstr.iter (fun key e -> Format.eprintf "%s %a@." key print_def (snd e)) t;
Format.eprintf "End table@."
(* Adds all referenced cvc4 variables found in the term t to table *)
let rec get_variables_term (table: correspondence_table) t =
match t with
......@@ -57,78 +64,76 @@ let get_all_var (table: correspondence_table) =
| _, Function (_, t) -> get_variables_term table t
| _, Term t -> get_variables_term table t) table table
(* Return true if key is s suffixed with a number *)
(* We should change the code of this function (Str still forbidden) *)
let is_prefix_num key s =
if (String.length s >= String.length key) || String.length s = 0 then
false
else
try
let b = ref (has_prefix s key) in
for i = String.length s to String.length key - 1 do
b := !b && (String.get key i <= '9') && (String.get key i >= '0')
done;
!b
with
| _ -> false
(* Add all variables referenced in the model to the table *)
let add_all_cvc s table t =
Mstr.fold (fun key _element acc ->
if is_prefix_num key s then
try
if snd (Mstr.find key acc) = Noelement then
Mstr.add key t acc
else acc
with Not_found -> acc
else
acc) table table
exception Bad_variable
(* Get the "radical" of a variable *)
let remove_end_num s =
let n = ref (String.length s - 1) in
while String.get s !n <= '9' && String.get s !n >= '0' && !n >= 0 do
n := !n - 1
done;
try
String.sub s 0 (!n + 1)
with
| _ -> s
if !n <= 0 then s else
begin
while String.get s !n <= '9' && String.get s !n >= '0' && !n >= 0 do
n := !n - 1
done;
try
String.sub s 0 (!n + 1)
with
| _ -> s
end
(* Add the variables that can be deduced from ITE to the table of variables *)
let add_vars_to_table table value =
let rec add_vars_to_table (table: correspondence_table) value =
let t = match (snd value) with
| Term t -> t
| Function (_, t) -> t
| Noelement -> raise Bad_variable in
match t with
let rec add_vars_to_table ~type_value (table: correspondence_table) value =
match value with
| Ite (Cvc4_Variable cvc, Function_Local_Variable _x, t1, t2) ->
begin
let table = Mstr.add cvc (false, Term t1) table in
add_vars_to_table table (false, Term t2)
add_vars_to_table ~type_value table t2
end
| Ite (Function_Local_Variable _x, Cvc4_Variable cvc, t1, t2) ->
begin
let table = Mstr.add cvc (false, Term t1) table in
add_vars_to_table table (false, Term t2)
add_vars_to_table ~type_value table t2
end
| Ite (t, Function_Local_Variable _x, Cvc4_Variable cvc, t2) ->
begin
let table = Mstr.add cvc (false, Term t) table in
add_vars_to_table table (false, Term t2)
add_vars_to_table ~type_value table t2
end
| Ite (Function_Local_Variable _x, t, Cvc4_Variable cvc, t2) ->
begin
let table = Mstr.add cvc (false, Term t) table in
add_vars_to_table table (false, Term t2)
add_vars_to_table ~type_value table t2
end
| Ite (_, _, _, _) -> table
| _ -> table
| _ ->
begin
match type_value with
| None -> table
| Some type_value ->
Mstr.fold (fun key (_b, elt) acc ->
let match_str = Str.regexp ("_" ^ type_value ^ "_") in
match Str.search_forward match_str (remove_end_num key) 0 with
| exception Not_found -> acc
| _ ->
if elt == Noelement then
Mstr.add key (false, Term value) acc
else
acc)
table table
end
in
add_vars_to_table table value
let type_value, t = match (snd value) with
| Term t -> (None, t)
| Function (cvc_var_list, t) ->
begin
match cvc_var_list with
| [(_, type_value)] -> (type_value, t)
| _ -> (None, t)
end
| Noelement -> raise Bad_variable in
add_vars_to_table ~type_value table t
let rec refine_definition table t =
match t with
......@@ -297,87 +302,6 @@ let convert_to_model_element name t =
let value = convert_to_model_value t in
Model_parser.create_model_element ~name ~value ()
(* Printing function *)
let print_table t =
Format.eprintf "Table key and value@.";
Mstr.iter (fun key e -> Format.eprintf "%s %a@." key print_def (snd e)) t;
Format.eprintf "End table@."
(* Analysis function to get the value of Cvc4 variable contained in the model *)
(* Given a to_rep and its corresponding of_rep in the model gives a guessed
value to unknown variables using constant of_rep/to_rep and "else" case of
the ITE.*)
let corres_else_element table to_rep =
let (_key1, (_b1, to_rep)) = to_rep in
(*let (_key2, (_b2, of_rep)) = of_rep in*)
let to_rep = match to_rep with
| Term t -> t
| Function (_, t) -> t
| Noelement -> raise Not_value in
(*
let of_rep = match of_rep with
| Term t -> t
| Function (_, t) -> t
| Noelement -> raise Not_value in
*)
let cvc = ref None in
let rec corres_else_element table to_rep =
match to_rep with
| Ite (Function_Local_Variable _v, Cvc4_Variable v, _, to_rep) ->
cvc := Some v;
corres_else_element table to_rep
| t ->
(* Make all variables not already guessed equal to the else case *)
begin
match !cvc with
| None -> table
| Some cvc ->
(* Last element of the if is added for all unassigned variables of
same name. *)
let s = remove_end_num cvc in
add_all_cvc s table (false, Term t)
end
in
corres_else_element table to_rep
let to_rep_of_rep (table: correspondence_table) (projections_list: Stdlib.Sstr.t) =
let projections_lists =
Mstr.fold (fun key value acc ->
if Stdlib.Sstr.mem key projections_list then
(key, value) :: acc else acc) table [] in
(*
List.sort (fun x y -> String.compare (fst x) (fst y))
(Mstr.fold (fun key value acc ->
if has_prefix "to_rep" key then
(key,value) :: acc else acc) table []) in
*)
(*
let of_reps =
List.sort (fun x y -> String.compare (fst x) (fst y))
(Mstr.fold (fun key value acc -> if has_prefix "of_rep" key then
(key,value) :: acc else acc) table []) in
*)
List.fold_left (fun table to_rep ->
corres_else_element table to_rep)
table projections_lists
(*
let to_rep_of_rep table to_reps =
List.fold_left (fun table to_rep ->
corres_else_element table to_rep)
table projections_lists
(*
match to_reps with
| to_rep :: tl1 ->
let table = corres_else_element table to_rep in
to_rep_of_rep table tl1
| [] -> table*)
in
to_rep_of_rep table projections_list
*)
let create_list (projections_list: Stdlib.Sstr.t) (table: correspondence_table) =
(* First populate the table with all references to a cvc variable *)
......@@ -392,9 +316,6 @@ let create_list (projections_list: Stdlib.Sstr.t) (table: correspondence_table)
acc)
table table in
(* Recover values from the combination of to_rep and of_rep *)
let table = to_rep_of_rep table projections_list in
(* Then substitute all variables with their values *)
let table =
Mstr.fold (fun key v acc -> refine_variable_value acc key v) table table in
......
......@@ -182,7 +182,7 @@ args_lists:
(* TODO This is inefficient and should be done in a left recursive way *)
args:
| name SPACE ireturn_type { $1 }
| name SPACE ireturn_type { $1, $3 }
name:
| ATOM { $1 }
......@@ -235,8 +235,8 @@ boolean:
(* BEGIN IGNORED TYPES *)
(* Types are badly parsed (for future use) but never saved *)
ireturn_type:
| tname {}
| LPAREN idata_type RPAREN {}
| tname { Some $1 }
| LPAREN idata_type RPAREN { None }
isort_def:
| tname SPACE integer { }
......
......@@ -43,7 +43,7 @@ and term =
| To_array of term
type definition =
| Function of variable list * term
| Function of (variable * string option) list * term
| Term of term
| Noelement
......@@ -121,7 +121,7 @@ and make_local vars_lists t =
match t with
| Variable s ->
begin
if (List.exists (fun x -> s = x) vars_lists) then
if (List.exists (fun x -> s = fst x) vars_lists) then
Function_Local_Variable s
else
try
......
......@@ -43,7 +43,7 @@ and term =
| To_array of term
type definition =
| Function of variable list * term
| Function of (variable * string option) list * term
| Term of term (* corresponding value of a term *)
| Noelement
......@@ -57,7 +57,7 @@ val add_element: (string * definition) option ->
correspondence_table -> bool -> correspondence_table
val make_local: variable list -> term -> term
val make_local: (variable * string option) list -> term -> term
val print_term: Format.formatter -> term -> unit
val print_def: Format.formatter -> definition -> unit
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment