Is there a way to have precise assignments on PPL Grid?

[rmonat]

I'd like the assignment m = n % 12 to be handled precisely by assign_texpr in the PPL Grid domain. It currently does not work precisely, while a similar code meeting constraints work when we use the EQMOD operator. I was wondering if you had any hint as to why this is imprecise, or how to fix it?

open Apron

let man = Ppl.manager_alloc_grid () 
let env = Environment.make [|Var.of_string "n"; Var.of_string "m"|] [||]
let top = Abstract1.top man env
let t3 = Texpr1.binop Mod (Texpr1.var env (Var.of_string "n")) (Texpr1.cst env (Coeff.s_of_int 12)) Int Rnd  (* n % 12 *)
let a3 = Abstract1.assign_texpr_array man top [|(Var.of_string "m")|] [|t3|] None  (* m := n % 12 *)
let () = Format.printf "@.test3: " 
let () = Tcons1.array_print Format.std_formatter (Abstract1.to_tcons_array man a3)
let () = Format.printf "@."

[antoinemine]

The problem is that, currently, due to the modulo operator, the expression is considered as non-linear and goes through the same generic linearisation process that outputs an affine expression, without modulo.

Possible fixes are:

• improve the (C) function ap_ppl_grid_assign_texpr_array in ppl_grid.cc to detect the modulo, apply linearization under the modulo only, and feed directly the result to Grid::generalized_affine_image, instead of always calling ap_generic_assign_texpr_array, which calls ap_ppl_grid_assign_linexpr and ultimately Grid::affine_image after getting rid of the modulo ;
• or change the OCaml client code to detect the modulo and, in that case, translate the assignment into a constraint meet using EQMOD.