search

AdaCore / spark2014

SPARK 2014 is the new version of SPARK, a software development technology specifically designed for engineering high-reliability applications.
GNU General Public License v3.0
248 stars 33 forks source link

SPARKSkein: check messages for potential problems #10

Closed ghost closed 5 years ago

ghost commented 5 years ago 
$ gnatprove -P/home/iridiumex/ada/spark2014/testsuite/gnatprove/tests/sparkskein/test.gpr -j0 --level=0 > msgs.out

msgs.out:

Phase 1 of 2: generation of Global contracts ...
Phase 2 of 2: flow analysis and proof ...
skein.adb:108:35: medium: range check might fail (e.g. when S = (others => 0) and S'First = 0 and S'Last = 0)
skein.adb:115:35: medium: range check might fail (e.g. when S = (others => 0) and S'First = 0 and S'Last = 0)
skein.adb:121:35: medium: range check might fail (e.g. when S = (others => 0) and S'First = 0 and S'Last = 0)
skein.adb:128:35: medium: range check might fail (e.g. when S = (others => 0) and S'First = 0 and S'Last = 0)
skein.adb:224:29: medium: array index check might fail, in call inlined at skein.adb:857 (e.g. when Hash = (others => 0) and Hash'Last = 0 and N = 0)
skein.adb:233:32: medium: "Dst" might not be initialized in "Get_64_LSB_First"
skein.adb:250:29: medium: "Dst" might not be initialized
skein.adb:251:25: medium: array index check might fail, in call inlined at skein.adb:570 (e.g. when Block = (others => 0) and Block'First = 0 and Block'Last = 0 and Src_Index = 18446744073709551576)
skein.adb:252:47: medium: array index check might fail, in call inlined at skein.adb:570 (e.g. when Block = (others => 0) and Block'First = 0 and Block'Last = 0 and Src_Index = 18446744073709551584)
skein.adb:253:47: medium: array index check might fail, in call inlined at skein.adb:570 (e.g. when Block = (others => 0) and Block'First = 0 and Block'Last = 0 and Src_Index = 18446744073709551592)
skein.adb:254:47: medium: array index check might fail, in call inlined at skein.adb:570 (e.g. when Block = (others => 0) and Block'First = 0 and Block'Last = 0 and Src_Index = 18446744073709551584)
skein.adb:255:47: medium: array index check might fail, in call inlined at skein.adb:570 (e.g. when Block = (others => 0) and Block'First = 0 and Block'Last = 0 and Src_Index = 18446744073709551592)
skein.adb:256:47: medium: array index check might fail, in call inlined at skein.adb:570 (e.g. when Block = (others => 0) and Block'First = 0 and Block'Last = 0 and Src_Index = 18446744073709551592)
skein.adb:257:47: medium: array index check might fail, in call inlined at skein.adb:570 (e.g. when Block = (others => 0) and Block'First = 0 and Block'Last = 0 and Src_Index = 18446744073709551592)
skein.adb:258:47: medium: array index check might fail, in call inlined at skein.adb:570 (e.g. when Block = (others => 0) and Block'First = 0 and Block'Last = 0 and Src_Index = 18446744073709551552)
skein.adb:296:19: medium: postcondition might fail, cannot prove Ctx.H.Hash_Bit_Len in Initialized_Hash_Bit_Length (e.g. when Ctx = (H => (Tweak_Words => (Byte_Count_LSB => 0, Byte_Count_MSB => 0, Reserved => 0, Tree_Level => 0, Bit_Pad => False, Field_Type => 0, First_Block => False, Final_Block => False), Hash_Bit_Len => 0, Byte_Count => 0), X => (others => 0), B => (others => 0)))
skein.adb:685:30: medium: range check might fail, in call inlined at skein.adb:756 (e.g. when Dst = 0 and Final_Dst = 0)
skein.adb:690:36: medium: array index check might fail, in call inlined at skein.adb:756 (e.g. when Ctx = (H => (Tweak_Words => (Byte_Count_LSB => 0, Byte_Count_MSB => 0, Reserved => 0, Tree_Level => 0, Bit_Pad => False, Field_Type => 0, First_Block => False, Final_Block => False), Hash_Bit_Len => 0, Byte_Count => 0), X => (others => 0), B => (others => 0)) and Msg = (others => 0) and Msg'First = 0 and Msg'Last = 0 and Src = 1)
skein.ads:226:28: medium: range check might fail (e.g. when S = (others => 0) and S'First = 0 and S'Last = 0)
Summary logged in /home/iridiumex/ada/spark2014/testsuite/gnatprove/tests/sparkskein/gnatprove/gnatprove.out

gnatprove.out:

Summary of SPARK analysis
=========================

----------------------------------------------------------------------------------------------------------
SPARK Analysis results        Total         Flow   Interval   CodePeer      Provers   Justified   Unproved
----------------------------------------------------------------------------------------------------------
Data Dependencies                 .            .          .          .            .           .          .
Flow Dependencies                 .            .          .          .            .           .          .
Initialization                  191          188          .          .            .           1          2
Non-Aliasing                      .            .          .          .            .           .          .
Run-time Checks                  68            .          .          .    52 (CVC4)           .         16
Assertions                        6            .          .          .     6 (CVC4)           .          .
Functional Contracts             11            .          .          .    10 (CVC4)           .          1
LSP Verification                  .            .          .          .            .           .          .
----------------------------------------------------------------------------------------------------------
Total                           276    188 (68%)          .          .     68 (25%)      1 (0%)    19 (7%)

Analyzed 1 unit
in unit skein, 45 subprograms and packages out of 58 analyzed
  Skein at skein.ads:29 flow analyzed (0 errors, 0 checks and 0 warnings) and proved (1 checks)
  Skein.Add_In_Range at skein.ads:164 flow analyzed (0 errors, 0 checks and 0 warnings) and proved (0 checks)
  Skein.Byte_Count_Of at skein.ads:170 flow analyzed (0 errors, 0 checks and 0 warnings) and proved (0 checks)
  Skein.Byte_SeqPredicate at skein.ads:55 flow analyzed (0 errors, 0 checks and 0 warnings) and proved (0 checks)
  Skein.Byte_Seq_128Predicate at skein.ads:62 flow analyzed (0 errors, 0 checks and 0 warnings) and proved (0 checks)
  Skein.Byte_Seq_16Predicate at skein.ads:60 flow analyzed (0 errors, 0 checks and 0 warnings) and proved (0 checks)
  Skein.Byte_Seq_4Predicate at skein.ads:58 flow analyzed (0 errors, 0 checks and 0 warnings) and proved (0 checks)
  Skein.Byte_Seq_64Predicate at skein.ads:61 flow analyzed (0 errors, 0 checks and 0 warnings) and proved (0 checks)
  Skein.Byte_Seq_8Predicate at skein.ads:59 flow analyzed (0 errors, 0 checks and 0 warnings) and proved (0 checks)
  Skein.Get_64_LSB_First at skein.adb:233 flow analyzed (0 errors, 2 checks and 0 warnings) and proved (0 checks)
  Skein.Hash_Bit_Len_Of at skein.ads:167 flow analyzed (0 errors, 0 checks and 0 warnings) and proved (0 checks)
  Skein.Put_64_LSB_First at skein.adb:207 flow analyzed (0 errors, 0 checks and 0 warnings) and proved (0 checks)
  Skein.Set_Debug_Flags at skein.ads:215 flow analyzed (0 errors, 0 checks and 0 warnings) and proved (0 checks)
  Skein.Show_Msg_8 at skein.ads:220 flow analyzed (0 errors, 0 checks and 0 warnings) and not proved, 1 checks out of 2 proved
  Skein.Skein_512_Block_BytesPredicate at skein.ads:106 flow analyzed (0 errors, 0 checks and 0 warnings) and proved (0 checks)
  Skein.Skein_512_Context at skein.ads:119 flow analyzed (0 errors, 0 checks and 0 warnings) and proved (0 checks)
  Skein.Skein_512_Final at skein.ads:194 flow analyzed (0 errors, 0 checks and 0 warnings) and not proved, 34 checks out of 35 proved
  Skein.Skein_512_Final.Set_Counter at skein.adb:788 flow analyzed (0 errors, 0 checks and 0 warnings) and proved (0 checks)
  Skein.Skein_512_Final.Zero_Pad at skein.adb:778 flow analyzed (0 errors, 0 checks and 0 warnings) and proved (0 checks)
  Skein.Skein_512_Hash at skein.ads:204 flow analyzed (0 errors, 0 checks and 0 warnings) and proved (3 checks)
  Skein.Skein_512_Init at skein.ads:173 flow analyzed (0 errors, 0 checks and 0 warnings) and proved (2 checks)
  Skein.Skein_512_Process_Block at skein.adb:280 flow analyzed (0 errors, 0 checks and 0 warnings) and not proved, 3 checks out of 12 proved
   suppressed messages:
    skein.adb:312:24: array KS is initialized at index 8, then from 0 to 7
  Skein.Skein_512_Process_Block.Do_First_Key_Injection at skein.adb:335 flow analyzed (0 errors, 0 checks and 0 warnings) and proved (0 checks)
  Skein.Skein_512_Process_Block.Initialize_Key_Schedule at skein.adb:306 flow analyzed (0 errors, 0 checks and 0 warnings) and proved (0 checks)
  Skein.Skein_512_Process_Block.Initialize_TS at skein.adb:324 flow analyzed (0 errors, 0 checks and 0 warnings) and proved (0 checks)
  Skein.Skein_512_Process_Block.Threefish_Block at skein.adb:349 flow analyzed (0 errors, 0 checks and 0 warnings) and proved (6 checks)
  Skein.Skein_512_Process_Block.Threefish_Block.Inject_Key at skein.adb:353 flow analyzed (0 errors, 0 checks and 0 warnings) and proved (0 checks)
  Skein.Skein_512_Process_Block.Threefish_Block.Round_1 at skein.adb:368 flow analyzed (0 errors, 0 checks and 0 warnings) and proved (0 checks)
  Skein.Skein_512_Process_Block.Threefish_Block.Round_2 at skein.adb:387 flow analyzed (0 errors, 0 checks and 0 warnings) and proved (0 checks)
  Skein.Skein_512_Process_Block.Threefish_Block.Round_3 at skein.adb:406 flow analyzed (0 errors, 0 checks and 0 warnings) and proved (0 checks)
  Skein.Skein_512_Process_Block.Threefish_Block.Round_4 at skein.adb:425 flow analyzed (0 errors, 0 checks and 0 warnings) and proved (0 checks)
  Skein.Skein_512_Process_Block.Threefish_Block.Round_5 at skein.adb:444 flow analyzed (0 errors, 0 checks and 0 warnings) and proved (0 checks)
  Skein.Skein_512_Process_Block.Threefish_Block.Round_6 at skein.adb:463 flow analyzed (0 errors, 0 checks and 0 warnings) and proved (0 checks)
  Skein.Skein_512_Process_Block.Threefish_Block.Round_7 at skein.adb:482 flow analyzed (0 errors, 0 checks and 0 warnings) and proved (0 checks)
  Skein.Skein_512_Process_Block.Threefish_Block.Round_8 at skein.adb:501 flow analyzed (0 errors, 0 checks and 0 warnings) and proved (0 checks)
  Skein.Skein_512_Process_Block.Update_Context at skein.adb:543 flow analyzed (0 errors, 0 checks and 0 warnings) and proved (0 checks)
  Skein.Skein_512_State_BytesPredicate at skein.ads:110 flow analyzed (0 errors, 0 checks and 0 warnings) and proved (0 checks)
  Skein.Skein_512_Update at skein.ads:181 flow analyzed (0 errors, 0 checks and 0 warnings) and not proved, 18 checks out of 20 proved
  Skein.Skein_512_Update.Copy_Msg_To_B at skein.adb:659 flow analyzed (0 errors, 0 checks and 0 warnings) and proved (0 checks)
  Skein.Skein_Start_New_Type at skein.adb:263 flow analyzed (0 errors, 0 checks and 0 warnings) and proved (0 checks)
  Skein.Sub_In_Range at skein.ads:161 flow analyzed (0 errors, 0 checks and 0 warnings) and proved (0 checks)
  Skein.To_LittleEndian at skein.adb:192 flow analyzed (0 errors, 0 checks and 0 warnings) and proved (0 checks)
  Skein.To_LittleEndian.lswapGP7701 at skein.adb:195 flow analyzed (0 errors, 0 checks and 0 warnings) and proved (0 checks)
  Skein.To_LittleEndian.lswapGP7701.LSwap at skein.adb:195 skipped
  Skein.Trace at skein.adb:93 skipped
  Skein.Trace.Set_Flags at skein.adb:100 skipped
  Skein.Trace.Show_64 at skein.adb:117 skipped
  Skein.Trace.Show_8 at skein.adb:104 skipped
  Skein.Trace.Show_Block at skein.adb:150 skipped
  Skein.Trace.Show_Final at skein.adb:131 skipped
  Skein.Trace.Show_Key at skein.adb:167 skipped
  Skein.Trace.Show_Msg_64 at skein.adb:123 skipped
  Skein.Trace.Show_Msg_8 at skein.adb:110 skipped
  Skein.Trace.Show_Round at skein.adb:141 skipped
  Skein.skein_512_state_words_to_bytesGP7369 at skein.adb:183 flow analyzed (0 errors, 0 checks and 0 warnings) and proved (0 checks)
  Skein.skein_512_state_words_to_bytesGP7369.Skein_512_State_Words_To_Bytes at skein.adb:183 skipped
  Skein.tweak_to_wordsGP7273 at skein.adb:180 flow analyzed (0 errors, 0 checks and 0 warnings) and proved (0 checks)
  Skein.tweak_to_wordsGP7273.Tweak_To_Words at skein.adb:180 skipped
yannickmoy commented 5 years ago

???

ghost commented 5 years ago

Sorry, I might not have been clear. I would like your help to eliminate the messages of medium severity as they could point to potential issues. If you believe that this is not the case, would you please say so with an explanation as to why? Of course they very well could be false positives. In any case, I thought I should let you know.

kanigsson commented 5 years ago

You ran the tool at the lowest level 0. In fact the file "test.py" (file which is part of our testing framework, gives info specific to this test) gives a hint that this is not sufficient. You need this command:

gnatprove -P test --prover=cvc4,altergo,z3 -j 16 --timeout=120 --steps=0

Note that with the sparkskein sources of current master, but using the 2018 community version, you get a spurious warning about initialization of some variable. You can ignore this message or use the version of the sparkskein sources that is distributed with 2018 community, or use the "gpl-2018" branch.