GitLab

Bugzilla Link	679
Created on	Feb 08, 2010 21:19
Version	svn
OS	Linux
Architecture	PC
Attachments	bug676A.sac

Extended Description

Created an attachment (id=671)
source code to reproduce fault
This is an attempt to separate Bug #676 into its essential parts...
The attached code was compiled under Build #16761:MODIFIED
with these options:
sac2c -extrema -nowlf -doawlf -check c -b11:uglf >crud
The first three options are not relevant, BTW, except for minor
differences in generated code.
Function main() contains this code:
  _flat_0 = _MAIN::id( _flat_1);
  _isaa_695__flat_0 = _saabind_( _isaa_675__rso_6_TheWorld, _isaa_676__rso_6_TheWorld, _flat_0);
  _pinl_507__flat_5 = [ _isaa_695__flat_0 ];
  _pinl_516__idc_68, _pinl_515__icc_61_pred = _non_neg_val_V_( _pinl_507__flat_5);
  _pinl_510__flat_2 = [ 0 ];
  _pinl_518__idc_69, _pinl_517__icc_60_pred = _non_neg_val_V_( _pinl_510__flat_2);
  _pinl_523__idc_72, _pinl_522__icc_63_pred = _val_le_val_VxV_( _pinl_518__idc_69, _pinl_507__flat_5);
  _pinl_528__idc_75, _pinl_527__icc_65_pred = _val_le_val_VxV_( _pinl_516__idc_68, _pinl_507__flat_5);
  _pinl_575_ub_i = _max_SxS_( _isaa_675__rso_6_TheWorld, _isaa_695__flat_0);
  _pinl_540__wlbsc_490_sc_bound = [ _pinl_575_ub_i ];
  _wlsimp_608 = _sub_SxS_( _isaa_695__flat_0, _pinl_575_ub_i);
  _pinl_506__icc_67 = with {
        (_pinl_540__wlbsc_490_sc_bound <= _pinl_513__flat_6=[_pinl_514_i] < _pinl_507__flat_5 genwidth [ _wlsimp_608 ])
        {
          /* empty */
        } : _isaa_675__rso_6_TheWorld ; ,
        (_pinl_510__flat_2 <= _pinl_513__flat_6=[_pinl_514_i] < _pinl_507__flat_5 genwidth [ _isaa_695__flat_0 ])
        {
          /* empty */
        } : _pinl_514_i ;
 } :
      genarray( _pinl_507__flat_5, _isaa_675__rso_6_TheWorld);
Several things are notable in this code:
1. The unguarded result of id(),  _isaa_695__flat_0, is used as WL
   GENERATOR_BOUND2 and in the _max_SxS_() computation.
   Although semantically correct, due to the _afterguard_() that follows
   the WL (not shown), it means that using the _non_neg_val_() guard 
   as the basis for annotating _pinl_516__idc_68 with
   an AVIS_MINVAL() of zero does us no good in simplifying the
   _max_SxS_() computation.
2. Similarly, the vector result of the val_le_val_VxV_() computation is
   not used at all. Its semantics are saved only by the use of
   its predicate result in the trailing _afterguard_().
What should be done here, I think, is the following;
Each guard should, effectively, replace all following occurrences of its
vector arguments by the appropriate result of that guard.
This would have the effect of allowing array annotations (e.g., 
AVIS_MINVAL, AVIS_MAXVAL) to propagate through the code from each
guard to the actual point(s) of use of the putative variable.