Rare problems with DoubleInRange

[agroce]

TRACE: BETWEEN -0.000000 and 0.000000 = 78804012392788958424558080200287227610159478540930893335896586808491443542994421222828532509769831281613255980613632.000000

CRITICAL: flcheck.cpp(38): 78804012392788958424558080200287227610159478540930893335896586808491443542994421222828532509769831281613255980613632.000000 > 0.000000

[agroce]

This is probably the only problematic case, and as @pgoodman notes: "this kind of makes sense because +0 is 0ull and -0.0 is 1ULL << 63u"

[agroce]

One fix is "don't ask for a double between -0.0 and 0.0, that's stupid" but we can probably special case it pretty easy.

[agroce]

There are other cases, not just -0.0 - 0.0, alas.

A fix will make this harness:

#include <deepstate/DeepState.hpp>
#include <cmath>

using namespace deepstate;
using namespace std;

TEST(DoubleGen, Ranges) {
  double low = DeepState_Double();
  assume (!isnan(low));
  double high = DeepState_Double();
  assume (!isnan(high));  
  if (low > high) {
    double temp = low;
    low = high;
    high = temp;
  }
  double v = DeepState_DoubleInRange(low, high);
  assume (!isnan(v));
  //printf ("BETWEEN %lf and %lf = %lf\n", low, high, v);
  ASSERT (v >= low) << v << " < [" << low << " - " << high << "]";
  ASSERT (v <= high) << v << " > [" << low << " - " << high << "]";
}

always pass. At present, it finds numerous violations, most (not all) with 0.0 upper bound. AFL or libfuzzer with value profiles works well for checking solutions.

[agroce]

Temporary fix is in 25de870: just add an assume guard, but it'd be better to just actually generate right values. Actually satisfying the assume can be very low probability...

[agroce]

at a guess int range fix may fix this, but have not checked yet

[agroce]

No, it looks like #264 does not fix this:

CRITICAL: double.cpp(21): 158845932543134348732211030624061342767482643708365862543045166703181164221537311888589860438825602654693210650114262884928937943579407249347164656507448609178181446582526984502085347877257757065216.000000 > [-232754180105407551188173433384396072032925198706333416049138060003638628753111617085696335862949826050839787585228955700210590405154411712445048717174863189751864940353823819732267921562910762991616.000000 - 0.000000]
ERROR: Failed: DoubleGen_Ranges
ERROR: Test case lf/3dd00a27cea108bb0889cb64579d0021cd13dfe3 failed
CRITICAL: double.cpp(21): 153705941638131736194094034974490215389264367465120785766906130196403780885907438447763769263035686284428923978252949875077856370807576954338962094192350844465752572877078528.000000 > [-600518360289889546855020274328008443117871764283410847920068600455100235399738602076987959280223438175532680060458159306108326737533007036763168981571818232127265429258240.000000 - 0.000000]
ERROR: Failed: DoubleGen_Ranges
ERROR: Test case lf/34ed697bbb6fef23c91f6958dec5f7f0712d0863 failed
CRITICAL: double.cpp(21): 9125942899359056246564024697408073638597257517041302303464008398315303934672175517795520312124070648584485307245653739467438932922166784435065401879634946012099247571968576684230823516198404096.000000 > [-65505129898969588832360452135241602288181575357032336969064529371027805108980834612884253584581843681686022284037094367457445117240570182483013568315774203709598644779521411636855562734903206338519073775522152448.000000 - 0.000000]
ERROR: Failed: DoubleGen_Ranges
ERROR: Test case lf/59a7c3257f781930832f499ae84d3759f057ee0e failed
CRITICAL: double.cpp(21): 409123878010212677875946606547773203366188278185100459146997674500662718602763203110486836643089003772322278285047066370185829900624805519101165305856.000000 > [-88796758757214309154594952557223076005090226223463941120537257967942839133650429861816452348400447245877136269146007560362859480525217044692843857477604990760703378692335164691700475042553561403817812537735797564953946241859231056943672660452653097820900210966539934965026663957869278275040425541632.000000 - 0.000000]
ERROR: Failed: DoubleGen_Ranges
ERROR: Test case lf/8b45f8a625fae17b7db553deda4d195d395b62bb failed
CRITICAL: double.cpp(21): 99167235282984300021178828709162510247907183535774410773135166005211431304284525125940613754409117690813290378576857512018929478624112222147887832019360948304508585438697024000889059706994256876450199823895294139626313206268352790528.000000 > [-107730874267432137203343331820822035577514310242782965586097631855966576162301880634213986293205127792322062538351156704152182839736964151026851280176102232488321269248467172131803507875122376996725092200401040958124190100858265776685056.000000 - 0.000000]
ERROR: Failed: DoubleGen_Ranges
ERROR: Test case lf/b42664b9218210ad651d8f9e4e348add20ccdc37 failed
CRITICAL: double.cpp(21): 44711155163161174811548414004481093657177888323996977805735387676084223311525186987966165558359501835429355235277514850560665174126562332836586425550540987224619401204591779084629141942016743096805992639754141696.000000 > [-224253081237366139386650866763380719201151967588281217707828470639785173018640910901538626501871439041919826800161312308134971214465045528490114809186986271780962042234155742826473432297305068797952.000000 - 0.000000]
ERROR: Failed: DoubleGen_Ranges
ERROR: Test case lf/5eaca4b45433175c6f04a70c47c3306c4caf0180 failed

[agroce]

I am 90% sure you can totally avoid this by not asking for a float/double in the range [BIGGISH NEGATIVE INT - 0.0000] but still don't understand the issue; fairly certain int ranges are fixed, so it's the floating point transform itself that is the problem