From 2b8b55de4a18757e8d6769e458c84f7c1df1e261 Mon Sep 17 00:00:00 2001 From: Jed Barber Date: Mon, 13 Feb 2017 18:27:13 +1100 Subject: Swapped out crypto package for something smaller, revised other code and readme/notes slightly --- src/multi_precision_integers-check.adb | 141 +++++++++++++++++++++++++++++++++ 1 file changed, 141 insertions(+) create mode 100644 src/multi_precision_integers-check.adb (limited to 'src/multi_precision_integers-check.adb') diff --git a/src/multi_precision_integers-check.adb b/src/multi_precision_integers-check.adb new file mode 100644 index 0000000..ac0efc4 --- /dev/null +++ b/src/multi_precision_integers-check.adb @@ -0,0 +1,141 @@ +with Ada.Text_IO; use Ada.Text_IO; +-- !! will disappear in favour of Ada.Exceptions + +with Multi_precision_integers.IO; + +package body Multi_precision_integers.Check is + + package IOi renames Multi_precision_integers.IO; + + -- Don't be afraid by the bug reporting tools, + -- they are unlikely to pop out of a programme ;-) + + Bug_file: Ada.Text_IO.File_type; + Bug_file_name: constant String:= "mupreint.bug"; + + -- The flaw detection (DEBUG mode) could suffer from + -- a chicken-and-egg problem: e.g. "*" works, but the "/" + -- to verify it doesn't ! + + Multiply_flawed_div1_has_rest : exception; + Multiply_flawed_div1_wrong_quotient : exception; + Multiply_flawed_div2_has_rest : exception; + Multiply_flawed_div2_wrong_quotient : exception; + + Div_Rem_flawed : exception; + + procedure Open_Bug_Report is + begin + Create( Bug_file, out_file, Bug_file_name ); + Put_Line( Bug_file, "Bug in Multi_precision_integers"); + end Open_Bug_Report; + + procedure Close_Bug_Report is + begin + Close( Bug_file ); + -- These console messages can provoke a silent quit in GUI apps, + -- so we put them after closing the report. + Put_Line( "Bug in Multi_precision_integers !"); + Put_Line( "For details, read file: " & Bug_file_name); + end Close_Bug_Report; + + procedure Test( m: multi_int; test_last: Boolean:= True ) is + last_nz: index_int:= 0; + Negative_block, + Last_index_has_zero, + Field_last_outside_range, Field_last_is_negative: exception; + begin + if m.zero then return; end if; -- 0, nothing to test + if m.last_used > m.n then raise Field_last_outside_range; end if; + if m.last_used < 0 then raise Field_last_is_negative; end if; + for i in 0 .. m.last_used loop + if m.blk(i) < 0 then + raise Negative_block; + end if; + if m.blk(i) /= 0 then + last_nz:= i; + end if; + end loop; + if test_last and then 0 < last_nz and then last_nz < m.last_used then + raise Last_index_has_zero; + end if; + end Test; + + procedure Check_Multiplication(i1,i2,i3: in multi_int) is + jeu: constant:= 5; -- 0 suffit + q1: Multi_int( i2.last_used + jeu ); + r1: Multi_int( i1.last_used + i2.last_used + jeu ); + q2: Multi_int( jeu ); + r2: Multi_int( i2.last_used + jeu ); + + procedure Bug_Report is + begin + Open_Bug_Report; + Put_Line( Bug_file, "Multiply_and_verify"); + Put( Bug_file, "i1 ="); IOi.Put_in_blocks(Bug_file, i1); New_Line(Bug_file); + Put( Bug_file, "i2 ="); IOi.Put_in_blocks(Bug_file, i2); New_Line(Bug_file); + Put( Bug_file, "i3 ="); IOi.Put_in_blocks(Bug_file, i3); New_Line(Bug_file); + end Bug_Report; + + begin + Test(i1); + Test(i2); + + if not (i1.zero or i2.zero) then + -- Now we divide i3 by i1, q1 should be = i2 + Div_Rem_internal_both_export(i3,i1, q1,r1); + if not r1.zero then + Bug_Report; + Close_Bug_Report; + raise Multiply_flawed_div1_has_rest; + end if; + if not Equal( q1, i2 ) then + Bug_Report; + Put( Bug_file, "q1 ="); IOi.Put_in_blocks(Bug_file, q1); New_Line(Bug_file); + Close_Bug_Report; + raise Multiply_flawed_div1_wrong_quotient; + end if; + -- Now we divide q1 by i2, should be = 1 + Div_Rem_internal_both_export(q1,i2, q2,r2); + if not r2.zero then + Bug_Report; + Close_Bug_Report; + raise Multiply_flawed_div2_has_rest; + end if; + if not Equal( q2, Multi(1) ) then + Bug_Report; + Put( Bug_file, "q2 ="); IOi.Put_in_blocks(Bug_file, q1); New_Line(Bug_file); + Close_Bug_Report; + raise Multiply_flawed_div2_wrong_quotient; + end if; + end if; + + end Check_Multiplication; + + procedure Check_Div_Rem(i1,i2,q,r: in multi_int) is + + procedure Bug_Report is + begin + Open_Bug_Report; + Put_Line( Bug_file, "Div_Rem_and_verify"); + Put( Bug_file, "i1 ="); IOi.Put_in_blocks(Bug_file, i1); New_Line(Bug_file); + Put( Bug_file, "i2 ="); IOi.Put_in_blocks(Bug_file, i2); New_Line(Bug_file); + Put( Bug_file, "q ="); IOi.Put_in_blocks(Bug_file, q); New_Line(Bug_file); + Put( Bug_file, "r ="); IOi.Put_in_blocks(Bug_file, r); New_Line(Bug_file); + end Bug_Report; + + begin + Test(i1); + Test(i2); + + if not Equal( i1, i2*q + r ) then + Bug_Report; + Close_Bug_Report; + raise Div_Rem_flawed; + end if; + + Test(q); + Test(r); + end Check_Div_Rem; + +end Multi_precision_integers.Check; -- cgit