Tipo di punto fisso che non si moltiplica correttamente

Question

Sono nuovo di Ada e ho provato i tipi "delta" a virgola fissa. In particolare, ho creato un intervallo di tipo delta a 32 bit 0.0 .. 1.0. Tuttavia, quando provo a quadrare determinati valori, ottengo un CONSTRAINT_ERROR. Per quanto ne so, questo non dovrebbe accadere con la mia gamma specificata. La soglia per questo errore sembra essere sqrt(1/2). Sto usando GNAT da MinGW-w64 versione 4.8.0.

Codice di prova (tutti compila in forma di gnatmake <file> senza avvisi/errori):

types.ads:

pragma Ada_2012; 

with Ada.Unchecked_Conversion; 
with Ada.Text_IO; 

package Types is 
    type Fixed_Type is delta 1.0/2**32 range 0.0 .. 1.0 
     with Size => 32; 
    type Modular_Type is mod 2**32 
     with Size => 32; 
    function Fixed_To_Mod is new Ada.Unchecked_Conversion(Fixed_Type, Modular_Type); 
    package MIO is new Ada.Text_IO.Modular_IO(Modular_Type); 
    package FIO is new Ada.Text_IO.Fixed_IO(Fixed_Type); 
end Types; 

specifics.adb:

pragma Ada_2012; 

with Ada.Text_IO; 

with Types; use Types; 

procedure Specifics is 
    package TIO renames Ada.Text_IO; 

    procedure TestValue(val: in Fixed_Type) is 
     square : Fixed_Type; 
    begin 
     square := val * val; 
     TIO.Put_Line("Value " & Fixed_Type'Image(val) & " squares properly."); 
     TIO.Put_Line("Square: " & Fixed_Type'Image(square)); 
     TIO.New_Line; 
    exception 
     when Constraint_Error => 
      TIO.Put_Line("Value " & Fixed_Type'Image(val) & " does not square properly."); 
      TIO.Put_Line("Square: " & Fixed_Type'Image(val * val)); 
      TIO.Put_Line("Not sure how that worked."); 
      TIO.New_Line; 
    end TestValue; 

    function ParseFixed(s: in String; last: in Natural; val: out Fixed_Type) return Boolean is 
     l : Natural; 
    begin 
     FIO.Get(s(s'First..last), val, l); 
     return TRUE; 
    exception 
     when others => 
      TIO.Put_Line("Parsing failed."); 
      return FALSE; 
    end ParseFixed; 

    buffer : String(1..20); 
    last : Natural; 
    f : Fixed_Type; 
begin 
    loop 
     TIO.Put(">>> "); 
     TIO.Get_Line(buffer, last); 
     exit when buffer(1..last) = "quit"; 
     if ParseFixed(buffer, last, f) then 
      TestValue(f); 
     end if; 
    end loop; 
end Specifics; 

uscita di specifics.adb:

>>> 0.1 
Value 0.1000000001 squares properly. 
Square: 0.0100000000 

>>> 0.2 
Value 0.2000000000 squares properly. 
Square: 0.0399999998 

>>> 0.4 
Value 0.3999999999 squares properly. 
Square: 0.1599999999 

>>> 0.6 
Value 0.6000000001 squares properly. 
Square: 0.3600000001 

>>> 0.7 
Value 0.7000000000 squares properly. 
Square: 0.4899999998 

>>> 0.75 
Value 0.7500000000 does not square properly. 
Square: -0.4375000000 
Not sure how that worked. 

>>> quit 

In qualche modo, moltiplicando val da solo ha dato un numero negativo, che spiega il CONSTRAINT_ERROR ... ma non importa, perché sto ricevendo un numero negativo in primo luogo?

Ho quindi deciso di verificare il punto in cui squadratura i numeri hanno cominciato in mancanza, così ho scritto il seguente frammento:

fixedpointtest.adb:

pragma Ada_2012; 

with Ada.Text_IO; 

with Types; use Types; 

procedure FixedPointTest is 
    package TIO renames Ada.Text_IO; 

    test, square : Fixed_Type := 0.0; 
begin 
    while test /= Fixed_Type'Last loop 
     square := test * test; 
     test := test + Fixed_Type'Delta; 
    end loop; 
exception 
    when Constraint_Error => 
     TIO.Put_Line("Last valid value: " & Fixed_Type'Image(test-Fixed_Type'Delta)); 
     TIO.Put("Hex value: "); 
     MIO.Put(Item => Fixed_To_Mod(test-Fixed_Type'Delta), Base => 16); 
     TIO.New_Line; 
     TIO.Put("Binary value: "); 
     MIO.Put(Item => Fixed_To_Mod(test-Fixed_Type'Delta), Base => 2); 
     TIO.New_Line; 
     TIO.New_Line; 
     TIO.Put_Line("First invalid value: " & Fixed_Type'Image(test)); 
     TIO.Put("Hex value: "); 
     MIO.Put(Item => Fixed_To_Mod(test), Base => 16); 
     TIO.New_Line; 
     TIO.Put("Binary value: "); 
     MIO.Put(Item => Fixed_To_Mod(test), Base => 2); 
     TIO.New_Line; 
     TIO.New_Line; 
end FixedPointTest; 

e ottenuto il seguente risultato:

Last valid value: 0.7071067810 
Hex value: 16#B504F333# 
Binary value: 2#10110101000001001111001100110011# 

First invalid value: 0.7071067812 
Hex value: 16#B504F334# 
Binary value: 2#10110101000001001111001100110100# 

Quindi, sqrt(1/2), ci incontriamo di nuovo. Qualcuno potrebbe spiegarmi perché il mio codice sta facendo questo? C'è un modo per farlo moltiplicare correttamente?

Answer 1

Penso che tu stia chiedendo 1 ulteriore bit di precisione di quanto sia effettivamente disponibile "sotto il cofano".

vostra dichiarazione

type Fixed_Type is delta 1.0/2**32 range 0.0 .. 1.0 
     with Size => 32; 

è accettato solo perché GNAT ha usato una rappresentazione distorta; non c'è spazio per un segno. È possibile visualizzare questo perché 0.7071067810 è rappresentato come 16#B504F333#, con il bit di bit più significativo. Quindi, moltiplicando 0,71 per 0,71, il risultato ha il bit più significativo impostato; e il codice di basso livello pensa che questo deve essere il bit del segno, quindi abbiamo un overflow.

Se si dichiara Fixed_Type come

type Fixed_Type is delta 1.0/2**31 range 0.0 .. 1.0 
     with Size => 32; 

tutti dovrebbero essere bene.

Un ulteriore punto: nel report del comportamento di specifics con un input di 0.75, si citano il risultato

>>> 0.75 
Value 0.7500000000 does not square properly. 
Square: -0.4375000000 
Not sure how that worked. 

ho ricostruito con gnatmake specifics.adb -g -gnato -bargs -E, e il risultato è ora

>>> 0.75 
Value 0.7500000000 does not square properly. 

Execution terminated by unhandled exception 
Exception name: CONSTRAINT_ERROR 
Message: 64-bit arithmetic overflow 
Call stack traceback locations: 
0x100020b79 0x10000ea80 0x100003520 0x100003912 0x10000143e 

e il traceback decodifica come

system__arith_64__raise_error (in specifics) (s-arit64.adb:364) 
__gnat_mulv64 (in specifics) (s-arit64.adb:318) 
specifics__testvalue.2581 (in specifics) (specifics.adb:20)  <<<<<<<<<< 
_ada_specifics (in specifics) (specifics.adb:45) 
main (in specifics) (b~specifics.adb:246) 

e specifics.adb:20 è

 TIO.Put_Line("Square: " & Fixed_Type'Image(val * val)); 

nel gestore di eccezioni, che coinvolge nuovamente il quadrato problematico (non è una buona cosa da fare in un gestore di eccezioni). È possibile vedere che il valore 0.75 è stato stampato senza alcun problema nella riga sopra: e in fixedpointtest.adb non è stato riscontrato alcun problema nelle aggiunte che hanno portato all'ultimo valore valido 0.7071067810.

Sono rimasto piuttosto sorpreso nel constatare che -gnato rileva questo errore, poiché pensavo che fosse applicato solo all'intero aritmetico; ma in effetti c'è una discussione nel GNAT User Guide che afferma che si applica anche all'aritmetica a virgola fissa. Si scopre che si può evitare l'errore di vincolo e ottenere il risultato aritmetico corretta utilizzando -gnato3:

>>> 0.75 
Value 0.7500000000 squares properly. 
Square: 0.5625000000 

ma solo a costo di usare arbitraria aritmetica precisione multipla - non è una buona idea per un sistema con limitazioni di tempo !