Implementation Issues

Trying to implement Issue 26:

To decide which prover should be called first we need:

• The file a given entity is concerned with.
• The prover name(s) and their associated times which have been run on the same check.
• The names of the provers the user would like to choose from
  • "Trivial" and possibly others (i.e. manual/interactive proofs don't help much)

The simple approach (Ada like pseudo code):

Entities := SPARK_Info.List_Entities_By_File (File_Name => ...); --  w/o Xref info inefficient to implement.
Prover_List := SPARK_Info.List_Provers (File_Name => ...);       --  This list is likely short (altergo, CVC4, Trivial, Z3, ..., and could be build when the tree is being built)

Times : array (Prover_List) of Duration := (others => 0.0);

for E of all Entities loop
   if E.Has_Failed_Attempts then --  If there are no failed attempts, we don't even know if it would make a difference.
     for all A of E.Attempts loop
        if A.Has_Failed_Attempts then --  Same reasoning as above
          if A.Prover in User_Selected_List then --  "Trivial" is not really a prover, it just means that no prover was needed.
          Times (A.Prover) := @ + A.Max_Time (Prover);
        end if;
     end loop;
   end;
end loop;

--  The "optimal" prover should now be the one with the shortest time, matching one of the user selections

After that, Times should contain the accumulated time each prover spent on checks and we can suggest the one taking less total time for that file.

Advanced Features

Give the user a list of entities which should go into different files (so, an "optimum" by entity), but that would require knowledge about the code itself, we don't even know what the identifier is (it could be pretty much anything, even types have predicate checks etc. attached to it). In theory we could infer the kind of entity from the checks involved, but this also requires knowledge about what the check names actually indicate.

And usually there is a reason, why a certain set of items is in the same file, so suggesting to split a type and it's primitive operation into separate packages would be rather stupid. Even if one could do with separates, I don't think gnatprove handles separates, I suspect it handles these just like the GNAT compiler, so not really differently that bodies declared within the package.