Commit e4af0ac2 authored by MARCHE Claude's avatar MARCHE Claude

Removed all apparent soundness bugs with integer division

parent 5cd2f3d6
......@@ -7,12 +7,14 @@ theory BuiltIn
meta "eliminate_algebraic" "keep_recs"
end
(*
theory int.EuclideanDivision
syntax function div "(%1 / %2)"
syntax function mod "(%1 % %2)"
end
*)
theory map.Map
syntax type map "(%1,%2) farray"
......
......@@ -10,6 +10,8 @@ theory BuiltIn
meta "eliminate_algebraic" "keep_recs"
end
(*
theory int.EuclideanDivision
(* workaround for the "-1 % 32 = -1" bug *)
......@@ -19,7 +21,7 @@ theory int.EuclideanDivision
syntax function mod "safe_modulo(%1,%2)"
end
*)
(*
Local Variables:
......
......@@ -152,6 +152,7 @@ theory bool.Bool
end
*)
(* CVC4 division does not seem to be the Euclidean one
theory int.EuclideanDivision
syntax function div "(div %1 %2)"
syntax function mod "(mod %1 %2)"
......@@ -160,6 +161,7 @@ theory int.EuclideanDivision
remove prop Mod_1
remove prop Div_1
end
*)
(*
theory real.Truncate
......
......@@ -70,17 +70,25 @@ theory int.Abs
end
(* wrong: Euclidean division is NOT division round down
e.g : div (-1) (-2) is 1, not 0 *)
(*
theory int.EuclideanDivision
syntax function div "int<dn>(%1 / %2)"
end
*)
(* Gappa <- 0.16.4 has a bug,
it says that div (-1) 2 can have any value *)
(*
theory int.ComputerDivision
syntax function div "int<zr>(%1 / %2)"
end
*)
theory real.Real
......
......@@ -132,6 +132,7 @@ theory bool.Bool
syntax function implb "(=> %1 %2)"
end
(* needs to be checked
theory int.EuclideanDivision
syntax function div "(div %1 %2)"
syntax function mod "(mod %1 %2)"
......@@ -140,6 +141,7 @@ theory int.EuclideanDivision
remove prop Mod_1
remove prop Div_1
end
*)
theory real.FromInt
syntax function from_int "(to_real %1)"
......
......@@ -129,6 +129,7 @@ theory bool.Bool
end
(* needs to checked
theory int.EuclideanDivision
syntax function div "(div %1 %2)"
syntax function mod "(mod %1 %2)"
......@@ -137,6 +138,7 @@ theory int.EuclideanDivision
remove prop Mod_1
remove prop Div_1
end
*)
(*
Local Variables:
......
......@@ -133,6 +133,7 @@ theory bool.Bool
end
(* needs to be checked
theory int.EuclideanDivision
syntax function div "(div %1 %2)"
syntax function mod "(mod %1 %2)"
......@@ -141,7 +142,7 @@ theory int.EuclideanDivision
remove prop Mod_1
remove prop Div_1
end
*)
theory map.Map
......
......@@ -132,6 +132,7 @@ theory bool.Bool
syntax function implb "(=> %1 %2)"
end
(* needs to be checked
theory int.EuclideanDivision
syntax function div "(div %1 %2)"
syntax function mod "(mod %1 %2)"
......@@ -140,6 +141,7 @@ theory int.EuclideanDivision
remove prop Mod_1
remove prop Div_1
end
*)
theory real.FromInt
syntax function from_int "(to_real %1)"
......
......@@ -132,6 +132,7 @@ end
*)
(* needs to be checked
theory int.EuclideanDivision
syntax function div "(div %1 %2)"
syntax function mod "(mod %1 %2)"
......@@ -140,6 +141,7 @@ theory int.EuclideanDivision
remove prop Mod_1
remove prop Div_1
end
*)
(*
Local Variables:
......
......@@ -4,10 +4,14 @@ theory EuclideanDivTest
use import int.Int
use import int.EuclideanDivision
goal ok1 : div (-1) (-2) = -1
goal ok2 : mod (-1) (-2) = 1
goal smoke1 : div (-1) (-2) = 0
goal smoke2 : mod (-1) (-2) = -1
goal ok1 : div (-1) 2 = -1
goal ok2 : mod (-1) 2 = 1
goal ok3 : div (-1) (-2) = 1
goal ok4 : mod (-1) (-2) = 1
goal smoke1 : div (-1) 2 = 0
goal smoke2 : mod (-1) 2 = -1
goal smoke3 : div (-1) (-2) = 0
goal smoke4 : mod (-1) (-2) = -1
end
......@@ -16,9 +20,13 @@ theory ComputerDivTest
use import int.Int
use import int.ComputerDivision
goal ok1 : div (-1) (-2) = 0
goal ok2 : mod (-1) (-2) = -1
goal smoke1 : div (-1) (-2) = -1
goal smoke2 : mod (-1) (-2) = 1
goal ok1 : div (-1) 2 = 0
goal ok2 : mod (-1) 2 = -1
goal ok3 : div (-1) (-2) = 0
goal ok4 : mod (-1) (-2) = -1
goal smoke1 : div (-1) 2 = -1
goal smoke2 : mod (-1) 2 = 1
goal smoke3 : div (-1) (-2) = -1
goal smoke4 : mod (-1) (-2) = 1
end
\ No newline at end of file
......@@ -27,16 +27,52 @@
version="1.0"/>
<prover
id="6"
name="Coq"
version="8.4"/>
<prover
id="7"
name="Eprover"
version="1.4"/>
<prover
id="8"
name="Gappa"
version="0.16.0"/>
<prover
id="9"
name="Simplify"
version="1.5.4"/>
<prover
id="10"
name="Vampire"
version="0.6"/>
<prover
id="11"
name="Yices"
version="1.0.25"/>
<prover
id="12"
name="Z3"
version="2.19"/>
<prover
id="7"
id="13"
name="Z3"
version="3.2"/>
<prover
id="8"
id="14"
name="Z3"
version="4.2"/>
<prover
id="15"
name="Z3"
version="4.3.1"/>
<prover
id="16"
name="Zenon"
version="0.7.1"/>
<prover
id="17"
name="iProver"
version="0.8.1"/>
<file
name="../div.why"
verified="false"
......@@ -45,35 +81,35 @@
name="EuclideanDivTest"
locfile="../div.why"
loclnum="2" loccnumb="7" loccnume="23"
verified="true"
verified="false"
expanded="true">
<goal
name="ok1"
locfile="../div.why"
loclnum="7" loccnumb="7" loccnume="10"
sum="bd1d5464857216da4e12f229f8c16af3"
sum="eda768039e7d01cab7cc352411a0b275"
proved="true"
expanded="true"
shape="ainfix =adivaprefix -c1aprefix -c2aprefix -c1">
expanded="false"
shape="ainfix =adivaprefix -c1c2aprefix -c1">
<proof
prover="0"
timelimit="5"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.11"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="1"
timelimit="5"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="2"
timelimit="5"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
......@@ -81,153 +117,136 @@
</proof>
<proof
prover="3"
timelimit="5"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.05"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="4"
timelimit="5"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.06"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="5"
timelimit="5"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.00"/>
</proof>
<proof
prover="6"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.09"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="7"
timelimit="5"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.08"/>
<result status="timeout" time="2.99"/>
</proof>
<proof
prover="8"
timelimit="5"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.13"/>
<result status="unknown" time="0.00"/>
</proof>
</goal>
<goal
name="ok2"
locfile="../div.why"
loclnum="8" loccnumb="7" loccnume="10"
sum="9e8488ed0545855ca9592335972be12a"
proved="true"
expanded="true"
shape="ainfix =amodaprefix -c1aprefix -c2c1">
<proof
prover="0"
timelimit="5"
prover="9"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="1"
timelimit="5"
prover="10"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="unknown" time="3.01"/>
</proof>
<proof
prover="2"
timelimit="5"
prover="11"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="3"
timelimit="5"
prover="12"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="4"
timelimit="5"
prover="13"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="5"
timelimit="5"
prover="14"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="6"
timelimit="5"
prover="15"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="7"
timelimit="5"
prover="16"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="timeout" time="3.14"/>
</proof>
<proof
prover="8"
timelimit="5"
prover="17"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="timeout" time="3.02"/>
</proof>
</goal>
<goal
name="smoke1"
name="ok2"
locfile="../div.why"
loclnum="9" loccnumb="7" loccnume="13"
sum="221247d874c6afe4157d51833127b93a"
loclnum="8" loccnumb="7" loccnume="10"
sum="b4d2e1617531911467f1b60798813040"
proved="true"
expanded="true"
shape="ainfix =adivaprefix -c1aprefix -c2c0">
expanded="false"
shape="ainfix =amodaprefix -c1c2c1">
<proof
prover="0"
timelimit="5"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.06"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="1"
timelimit="5"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
......@@ -235,7 +254,7 @@
</proof>
<proof
prover="2"
timelimit="5"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
......@@ -243,168 +262,145 @@
</proof>
<proof
prover="3"
timelimit="5"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.07"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="4"
timelimit="5"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.06"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="5"
timelimit="5"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="6"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.09"/>
</proof>
<proof
prover="7"
timelimit="5"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.08"/>
<result status="timeout" time="2.99"/>
</proof>
<proof
prover="8"
timelimit="5"
timelimit="3"
memlimit="1000"
edited="div-EuclideanDivTest-ok2_1.gappa"
obsolete="false"
archived="false">
<result status="timeout" time="5.13"/>
<result status="unknown" time="0.00"/>
</proof>
</goal>
<goal
name="smoke2"
locfile="../div.why"
loclnum="10" loccnumb="7" loccnume="13"
sum="b1ddfe4fa8fb15054feea09334b93e53"
proved="true"
expanded="true"
shape="ainfix =amodaprefix -c1aprefix -c2aprefix -c1">
<proof
prover="0"
timelimit="5"
prover="9"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.14"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="1"
timelimit="5"
prover="10"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="unknown" time="3.00"/>
</proof>
<proof
prover="2"
timelimit="5"
prover="11"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="3"
timelimit="5"
prover="12"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.08"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="4"
timelimit="5"
prover="13"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.07"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="5"
timelimit="5"
prover="14"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="6"
timelimit="5"
prover="15"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.09"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="7"
timelimit="5"
prover="16"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.18"/>
<result status="timeout" time="4.03"/>
</proof>
<proof
prover="8"
timelimit="5"
prover="17"
timelimit="3"
memlimit="1000"