Loại điểm cố định không nhân chính xác

Question

Tôi mới sử dụng Ada và đã thử loại "delta" cố định. Cụ thể, tôi đã tạo một phạm vi loại delta 32 bit 0.0 .. 1.0. Tuy nhiên, khi tôi cố gắng tạo một giá trị nhất định, tôi nhận được CONSTRAINT_ERROR. Theo như tôi biết, điều đó không nên xảy ra với phạm vi được chỉ định của tôi. Ngưỡng cho lỗi này có vẻ là sqrt(1/2). Tôi đang sử dụng GNAT từ phiên bản MinGW-w64 4.8.0.

mã kiểm tra (tất cả của nó biên dịch theo hình thức gnatmake <file> không có cảnh báo/lỗi):

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; 

Output của 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 

Bằng cách nào đó, nhân số val bằng chính nó mang lại một số âm, giải thích CONSTRAINT_ERROR ... nhưng không bao giờ nhớ rằng, tại sao tôi nhận được một số âm ngay từ đầu?

sau đó tôi quyết định thử nghiệm cho các điểm mà tại đó bình phương các số bắt đầu thất bại, vì vậy tôi đã viết đoạn sau:

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; 

và nhận được kết quả như sau:

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# 

Vì vậy, sqrt(1/2), chúng tôi sẽ gặp lại. Ai đó có thể vui lòng giải thích cho tôi tại sao mã của tôi đang làm điều này? Có cách nào để làm cho nó nhân lên đúng cách không?

Answer 1

Tôi nghĩ rằng bạn đang yêu cầu thêm một chút chính xác hơn là thực sự có sẵn "dưới mui xe".

khai của bạn

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

chỉ chấp nhận vì GNAT đã sử dụng một đại diện thiên vị; không có chỗ cho một chút dấu. Bạn có thể thấy điều này vì 0.7071067810 được thể hiện là 16#B504F333#, với bộ bit quan trọng nhất. Vì vậy, khi bạn nhân 0.71 với 0.71, kết quả có bộ bit quan trọng nhất; và mã cấp thấp cho rằng đây phải là bit dấu, vì vậy chúng ta có một tràn.

Nếu bạn khai báo Fixed_Type như

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

tất cả nên được tốt.

Điểm khác: trong báo cáo về hành vi của specifics với đầu vào là 0.75 tuổi, bạn trích dẫn kết quả

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

tôi xây dựng lại với gnatmake specifics.adb -g -gnato -bargs -E, và kết quả tại là

>>> 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 

và traceback giải mã như

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) 

và specifics.adb:20 là

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

trong xử lý ngoại lệ, liên quan đến hình vuông có vấn đề một lần nữa (không phải là một điều tốt để làm trong một xử lý ngoại lệ). Bạn có thể thấy rằng giá trị 0.75 được in mà không có bất kỳ sự cố nào trong dòng bên trên: và trong fixedpointtest.adb không có vấn đề gì trong việc bổ sung dẫn đến giá trị hợp lệ cuối cùng 0.7071067810.

Tôi khá ngạc nhiên khi thấy rằng -gnato phát hiện lỗi này, vì tôi nghĩ nó chỉ được áp dụng cho số học số nguyên; nhưng trên thực tế, có một cuộc thảo luận trong số GNAT User Guide tuyên bố rằng nó cũng áp dụng cho số học điểm cố định. Nó chỉ ra rằng bạn có thể tránh được những lỗi khó khăn và nhận được kết quả số học chính xác bằng cách sử dụng -gnato3:

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

nhưng chỉ với chi phí của việc sử dụng tùy tiện nhiều chính xác số học - không phải là một ý tưởng tốt cho một hệ thống thời gian hạn chế !