Merge branch 'cocospec' of https://cavale.enseeiht.fr/git/lustrec into cocospec

doc/integer_division.org

@@ -26,20 +26,14 @@ Some properties:
 
 * From C to Euclidian
 
-a mod_M b = (a mod_C b) + (a < 0 ? abs(b) : 0) 
+a mod_M b = (a mod_C b) + (a mod_C b < 0 ? abs(b) : 0) 
 
 a div_M b = (a - (a mod_M b)) div_C b
-          = (a - ((a mod_C b) + (a < 0 ? abs(b) : 0))) div_C b
+          = (a - ((a mod_C b) + (a mod_C b < 0 ? abs(b) : 0))) div_C b
 
 * From Euclidian to C
 
-a mod_C b = (a >= 0 ? a mod_M b : - ((-a) mod_M b)) 
-            (using math def to ensure positiveness of remainder))
-          = (a mod_M b) - (a < 0 ? abs(b) : 0)
-            (using the def of mod_M above)
+a mod_C b = a mod_M b - ((a mod_M b <> 0 && a <= 0) ? abs(b) : 0)
 
 a div_C b = (a - (a mod_C b)) div_M b
-          = (a - ((a mod_M b) - (a < 0 ? abs(b) : 0))) div_M b
-          
-Let's chosse the second, simpler, def of mod_C
-
+          = (a mod_M b <> 0 && a <= 0)?((a - a mod_M b + abs(b)) div_M b) :((a - a mod_M b) div_M b)

src/backends/C/c_backend_common.ml

@@ -110,19 +110,21 @@ let pp_machine_step_name fmt id = fprintf fmt "%s_step" id
 
 let pp_mod pp_val v1 v2 fmt =
   if !Options.integer_div_euclidean then
-    (* (a mod_C b) + (a < 0 ? abs(b) : 0) *)
-    Format.fprintf fmt "((%a %% %a) + (%a < 0?(abs(%a)):0))"
+    (* (a mod_C b) + (a mod_C b < 0 ? abs(b) : 0) *)
+    Format.fprintf fmt "((%a %% %a) + ((%a %% %a) < 0?(abs(%a)):0))"
       pp_val v1 pp_val v2
       pp_val v1 pp_val v2
+      pp_val v2
   else (* Regular behavior: printing a % *)
     Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2
 
 let pp_div pp_val v1 v2 fmt =
   if !Options.integer_div_euclidean then
-    (* (a - ((a mod_C b) + (a < 0 ? abs(b) : 0))) div_C b *)
-    Format.fprintf fmt "(%a - ((%a %% %a) + (%a < 0 ? abs(%a) : 0))) / %a"
-      pp_val v1 pp_val v1 pp_val v2
-      pp_val v1 pp_val v2 pp_val v2
+    (* (a - ((a mod_C b) + (a mod_C b < 0 ? abs(b) : 0))) div_C b *)
+    Format.fprintf fmt "(%a - %t) / %a"
+      pp_val v1
+      (pp_mod pp_val v1 v2)
+      pp_val v2
   else (* Regular behavior: printing a / *)
     Format.fprintf fmt "(%a / %a)" pp_val v1 pp_val v2
   

src/backends/Horn/horn_backend_printers.ml

@@ -67,22 +67,26 @@ let rec pp_default_val fmt t =
 
 let pp_mod pp_val v1 v2 fmt =
   if Types.is_int_type v1.value_type &&  not !Options.integer_div_euclidean then
-    (* C semantics: converting it to Euclidian operators
-       (a mod_M b) - (a < 0 ? abs(b) : 0)            
+    (* C semantics: converting it from Euclidean operators
+       (a mod_M b) - ((a mod_M b > 0 && a < 0) ? abs(b) : 0)            
     *)
-    Format.fprintf fmt "(- (mod %a %a) (ite (< %a 0) (abs %a) 0))"
-      pp_val v1 pp_val v2 pp_val v1 pp_val v2
+    Format.fprintf fmt "(- (mod %a %a) (ite (and (> (mod %a %a) 0) (< %a 0)) (abs %a) 0))"
+      pp_val v1 pp_val v2
+      pp_val v1 pp_val v2
+      pp_val v1
+      pp_val v2
   else
     Format.fprintf fmt "(mod %a %a)" pp_val v1 pp_val v2
 
 let pp_div pp_val v1 v2 fmt =
   if Types.is_int_type v1.value_type &&  not !Options.integer_div_euclidean then
-    (* C semantics: converting it to Euclidian operators
-       (a - ((a mod_M b) - (a < 0 ? abs(b) : 0))) div_M b
+    (* C semantics: converting it from Euclidean operators
+       (a - (a mod_C b)) div_M b
     *)
-    Format.fprintf fmt "(div (- %a (- (mod %a %a) (ite (< %a 0) (abs %a) 0))) %a)"
-      pp_val v1 pp_val v1 pp_val v2
-      pp_val v1 pp_val v2 pp_val v2
+    Format.fprintf fmt "(div (- %a %t) %a)"
+      pp_val v1
+      (pp_mod pp_val v1 v2)
+      pp_val v2
   else
     Format.fprintf fmt "(div %a %a)" pp_val v1 pp_val v2