Weird results of sat_tcons and sat_lincons

[skcho]

I encountered some weird cases with sat_tcons and sat_lincons and don't know how to understand its return values. This is sample code showing the weirdness.

open Apron

let test_tcons man abs tcons =
  let res = Abstract1.sat_tcons man abs tcons in
  Format.fprintf Format.err_formatter "tcons(%a):%b@." Tcons1.print tcons res

let test_lincons man abs lincons =
  let res = Abstract1.sat_lincons man abs lincons in
  Format.fprintf Format.err_formatter "lincons(%a):%b@." Lincons1.print lincons
    res

let _ =
  let man = Elina_poly.manager_alloc_loose () in
  let var_x = Var.of_string "x" in
  let var_y = Var.of_string "y" in
  let env = Environment.make [|var_x; var_y|] [||] in
  let tab = Parser.lincons1_of_lstring env ["x>=0"] in
  let abs = Abstract1.of_lincons_array man env tab in
  Format.fprintf Format.err_formatter "abs:%a@." Abstract1.print abs ;
  let tcons1 = Parser.tcons1_of_string env "x-y>=0" in
  test_tcons man abs tcons1 ;
  let tcons2 = Parser.tcons1_of_string env "y-x>=0" in
  test_tcons man abs tcons2 ;
  let lincons1 = Parser.lincons1_of_string env "x-y>=0" in
  test_lincons man abs lincons1 ;
  let lincons2 = Parser.lincons1_of_string env "y-x>=0" in
  test_lincons man abs lincons2

It tests the satisfiabilities of x-y>=0 and y-x>=0 under the abstract state x>=0. I expect all return false, because there is no information about y in the abstract state. However, the result is:

abs:[|x>=0|]
tcons(x - y - 0 >= 0):true
tcons(y - x - 0 >= 0):false
lincons(x-y>=0):true
lincons(-x+y>=0):false

If I change the manager to Apron's (by Oct.manager_alloc), it returns all false. Am I missing something for calling sat_tcons and sat_lincons?

[GgnDpSngh]

Hi,

I quickly tested with the C interface and ELINA returns false for me. I will check what goes wrong with the OCaml interface and let you know soon.

Cheers, Gagan

[skcho]

Well, I don't think it is an OCaml interface issue, because when I tested the same thing with the C interface, it also returned weird values.

#include "opt_pk.h"

int main(int argc, char **argv){
  elina_manager_t* man = opt_pk_manager_alloc(false);
  char* name_of_dim[2] = {"x", "y"};

  elina_linexpr0_t* x = elina_linexpr0_alloc(ELINA_LINEXPR_DENSE, 1);
  elina_linexpr0_set_coeff_scalar_int(x, 0, 1);  
  elina_lincons0_t lincons = elina_lincons0_make(ELINA_CONS_SUPEQ, x, NULL);
  elina_lincons0_array_t lincons_array = elina_lincons0_array_make(1);
  lincons_array.p[0] = lincons;
  opt_pk_array_t* abs = opt_pk_top(man, 2, 0);
  abs = opt_pk_meet_lincons_array(man, true, abs, &lincons_array);
  elina_lincons0_array_t lincons_array2 = opt_pk_to_lincons_array(man, abs);
  elina_lincons0_array_fprint(stdout, &lincons_array2, name_of_dim); fflush(stdout);

  elina_linexpr0_t* x_minus_y = elina_linexpr0_alloc(ELINA_LINEXPR_DENSE, 2);
  elina_linexpr0_set_coeff_scalar_int(x_minus_y, 0, 1);
  elina_linexpr0_set_coeff_scalar_int(x_minus_y, 1, -1);
  elina_lincons0_t lincons2 = elina_lincons0_make(ELINA_CONS_SUPEQ, x_minus_y, NULL);
  elina_lincons0_fprint(stdout, &lincons2, name_of_dim); printf("\n"); fflush(stdout);
  bool sat = opt_pk_sat_lincons(man, abs, &lincons2);
  printf("sat: %d\n",sat);

  elina_linexpr0_t* y_minus_x = elina_linexpr0_alloc(ELINA_LINEXPR_DENSE, 2);
  elina_linexpr0_set_coeff_scalar_int(y_minus_x, 0, -1);
  elina_linexpr0_set_coeff_scalar_int(y_minus_x, 1, 1);
  elina_lincons0_t lincons3 = elina_lincons0_make(ELINA_CONS_SUPEQ, y_minus_x, NULL);
  elina_lincons0_fprint(stdout, &lincons3, name_of_dim); printf("\n"); fflush(stdout);
  bool sat2 = opt_pk_sat_lincons(man, abs, &lincons3);
  printf("sat: %d\n",sat2);

  return 0;
}

1
array of constraints of size 1
 0: x >= 0
x - y >= 0
sat: 1
-x + y >= 0
sat: 0

I tried them on Mac(10.13.4) and CentOS(7.4.1708) and installed apron and elina using opam. My machines all returned like above. It is strange... :flushed:

[GgnDpSngh]

Hi,

You are right, my C test case was incorrect and I spotted a bug in the ELINA code. I am working on fixing it and will let you know soon.

Cheers, Gagan

[GgnDpSngh]

Hi Sungkeun,

Thanks for your feedback. I have fixed the bug and now it should return false. The bug occurs when the input abstract element contains unconstrained variables as in your example. We did not have any analyzers requiring "sat_lincons" and "sat_tcons" so could not detect it earlier with our random examples. Let me know if there are any further issues.

Cheers, Gagan

[skcho]

Hi Gagan,

Thank you for the quick fix. It works!

Sincerely, Sungkeun

[skcho]

Hi Gagan,

I reopened the issue because I encountered another related issue: When the abstract value is top, sat_lincons and sat_tcons have crash, in both C and OCaml.

#include "opt_pk.h"

int main(int argc, char **argv){
  elina_manager_t* man = opt_pk_manager_alloc(false);
  char* name_of_dim[2] = {"x", "y"};

  opt_pk_array_t* abs = opt_pk_top(man, 2, 0);
  elina_lincons0_array_t lincons_array = opt_pk_to_lincons_array(man, abs);
  elina_lincons0_array_fprint(stdout, &lincons_array, name_of_dim); fflush(stdout);

  elina_linexpr0_t* x = elina_linexpr0_alloc(ELINA_LINEXPR_DENSE, 1);
  elina_linexpr0_set_coeff_scalar_int(x, 0, 1);
  elina_lincons0_t lincons = elina_lincons0_make(ELINA_CONS_SUPEQ, x, NULL);
  elina_lincons0_fprint(stdout, &lincons, name_of_dim); printf("\n"); fflush(stdout);

  bool sat = opt_pk_sat_lincons(man, abs, &lincons);
  printf("sat: %d\n", sat);

  return 0;
}

empty array of constraints
x >= 0
segmentation fault: 11

Sincerely, Sungkeun

[GgnDpSngh]

Hi Sungkeun,

Thanks for reporting. The previous fix introduced the crash. I fixed it now and there should be no crash. Let me know if there are any further inputs for which there are bugs.

Cheers, Gagan

[skcho]

Thank you, Gagan. I will try the new one! 😃