0001003: conditional expression (?:) raises uncaught exception under why-2.30

(0002428)
Jochen (reporter)
2011-10-27 16:08

The same exception is raised also on the following program:

int ftest2(int n) { return 0 < n && n < 9; }

And also on that one:

void ftest3(int n) { if (0 < n) n = 1; else n = 2; }

(0002429)
pascal (reporter)
2011-10-27 18:03

If this is a regression in Nitrogen (is it?), this could be a consequence of switching to multiprecision integers in the AST for Nitrogen. In this case, the fix would be to change the = somewhere in the implementation to My_bigint.equal.

(0002433)
cmarche (developer)
2011-10-28 07:05

I can't reproduce that behavior. My guess is that it may occur only if an quite old version of Ocaml was used to compile the tools.

(0002453)
pascal (reporter)
2011-11-07 01:30

Following e-mails to the wrong person (that is, me), this issue is still open, and has been reproduced on a clean Linux installation. I also see others on the internet discussing this bug, most likely because it affects them.

Claude, I am guessing that you perhaps have OCaml 3.12.1, GMP and Zarith installed, and HAS_ZARITH defined to "yes". In this case, for you, (=) can be applied to big ints. This is one of the problem with Zarith: it makes (=) work (and makes it work correctly) between big ints.

The problem is that people who do not have Zarith, or do not have OCaml 3.12.1, still will see errors on applications of (=) to big ints.

Jochen, please try to substitute "frama-c.byte" to "frama-c" and see if you obtain a backtrace (please keep using "export OCAMLRUNPARAM=b". In fact, put it in your .profile, there is no reason not to want backtraces).

(0002463)
Jochen (reporter)
2011-11-10 15:24

I put "export OCAMLRUNPARAM=b" into my .profile and ran "frama-c.byte", as suggested by Pascal; however, I didn't obtain a backtrace (see file typescript1).

Frama-c.byte calls /usr/local/bin/jessie as a subprocess. I found out its args and env and called it again manyally, with an extra option "-d". This produced slightly more output (see file typescript2), but still no backtrace.

(0002477)
Jochen (reporter)
2011-11-18 15:02

While I gave up my attempts to produce a backtrace, I happened to find a new strange property: the error disappears if an assert-clause is inserted at the end of the then- or else-part, or both.

See the newly uploaded file ftest3.c. Put a "@" in line 6 or 10 to get it verified by Jessie(2.30) and Simplify.

None of the asserts in line 2,4,8,12 can cause this effect, even if they are weakened to \true. On the other hand, the asserts in line 6,10 work well also with formulas different from \true. In fact, the asserted formulas seem to have no influence.

(0002706)
flecsim (reporter)
2012-02-15 15:16

While attempting to circumvent issue 0001093, i triggered the same message, and in search for remedy i found this issue. I was able to retrieve a backtrace, but unfortunately i cannot supply the input (confidential).
However, i was able to trace this into jc_typing.mintype, where i added two patches in hope to find whats going on. The problem arised on (attempt to) evaluating "mintype _ int32 int32" for whatever reason.

Patch and output have been attached as "Output1003.txt". Maybe this helps in nailing down the problem.

(0002752)
flecsim (reporter)
2012-03-06 11:34

For me, the error disappeared on patching the definition of expr in jc_typing.ml, lines 2156-2167:
Before:

  | JCTnative Tboolean ->
    let te2,te3 =
      if same_type_no_coercion te2#typ te3#typ then
        te2,te3
      else
        unit_expr te2, unit_expr te3
    in
      let t = mintype e#pos
                      te2#typ
                      te3#typ
      in
        t, te2#region, JCEif(te1, te2, te3)

After:

  | JCTnative Tboolean ->
    let te2,te3 = unit_expr te2, unit_expr te3
    in
      let t = mintype e#pos
                      te2#typ
                      te3#typ
      in
        t, te2#region, JCEif(te1, te2, te3)

I am not sure whether this change may cause malfunction of Jessie, but i had quite some
"abstract value" errors collected among various projects. As none of them held up against
the patch, chances are the problem is located in that area of code.

(0003094)
yakobowski (manager)
2012-06-10 14:06

I have never been able to reproduce this bug myself, but there is something suspicious in the body of same_type_no_coercion

let same_type_no_coercion t1 t2 =
  match t1,t2 with
    | JCTnative t1, JCTnative t2 -> t1=t2
    | JCTenum ei1, JCTenum ei2 -> ei1.jc_enum_info_name = ei2.jc_enum_info_name
    | JCTlogic s1, JCTlogic s2 -> (* ?? *) s1=s2 (* ?? *)
[...]

Can you try again with this definition instead?

let rec same_type_no_coercion t1 t2 =
  match t1,t2 with
    | JCTnative t1, JCTnative t2 -> t1=t2
    | JCTenum ei1, JCTenum ei2 -> ei1.jc_enum_info_name = ei2.jc_enum_info_name
    | JCTlogic (name1, args1), JCTlogic (name2, args2) ->
        name1=name2 && List.for_all2 same_type_no_coercion args1 args2
(* following identical *)

(0003191)
cmarche (developer)
2012-06-22 18:01

I applied the modifications suggested by Boris into the SVN. No tests in the regression suite is affected, so I guees it is hamless ans the issue can be assumed as resolved.

(0003780)
signoles (manager)
2013-03-27 09:43

Fixed in Frama-C Oxygen + Why 2.32.

Issue History
Date Modified	Username	Field	Change
2011-10-27 15:49	Jochen	New Issue
2011-10-27 15:49	Jochen	Status	new => assigned
2011-10-27 15:49	Jochen	Assigned To	=> cmarche
2011-10-27 15:49	Jochen	File Added: ftest.c
2011-10-27 16:08	Jochen	Note Added: 0002428
2011-10-27 18:03	pascal	Note Added: 0002429
2011-10-28 07:05	cmarche	Note Added: 0002433
2011-10-28 07:05	cmarche	Status	assigned => closed
2011-10-28 07:05	cmarche	Resolution	open => unable to reproduce
2011-11-07 01:30	pascal	Note Added: 0002453
2011-11-07 01:30	pascal	Status	closed => feedback
2011-11-07 01:30	pascal	Resolution	unable to reproduce => reopened
2011-11-10 15:20	Jochen	File Added: typescript1
2011-11-10 15:20	Jochen	File Added: typescript2
2011-11-10 15:24	Jochen	Note Added: 0002463
2011-11-18 14:53	Jochen	File Added: ftest3.c
2011-11-18 15:02	Jochen	Note Added: 0002477
2012-02-15 15:15	flecsim	File Added: Output1003.txt
2012-02-15 15:16	flecsim	Note Added: 0002706
2012-03-06 11:34	flecsim	Note Added: 0002752
2012-06-10 14:06	yakobowski	Note Added: 0003094
2012-06-22 18:01	cmarche	Note Added: 0003191
2012-06-22 18:02	cmarche	Status	feedback => resolved
2012-06-22 18:02	cmarche	Resolution	reopened => fixed
2013-03-27 09:43	signoles	Note Added: 0003780
2013-03-27 09:44	signoles	Fixed in Version	=> Frama-C Oxygen-20120901
2013-03-27 09:44	signoles	Status	resolved => closed

Notes
(0002428) Jochen (reporter) 2011-10-27 16:08	The same exception is raised also on the following program: int ftest2(int n) { return 0 < n && n < 9; } And also on that one: void ftest3(int n) { if (0 < n) n = 1; else n = 2; }

(0002429) pascal (reporter) 2011-10-27 18:03	If this is a regression in Nitrogen (is it?), this could be a consequence of switching to multiprecision integers in the AST for Nitrogen. In this case, the fix would be to change the = somewhere in the implementation to My_bigint.equal.

(0002433) cmarche (developer) 2011-10-28 07:05	I can't reproduce that behavior. My guess is that it may occur only if an quite old version of Ocaml was used to compile the tools.

(0002453) pascal (reporter) 2011-11-07 01:30	Following e-mails to the wrong person (that is, me), this issue is still open, and has been reproduced on a clean Linux installation. I also see others on the internet discussing this bug, most likely because it affects them. Claude, I am guessing that you perhaps have OCaml 3.12.1, GMP and Zarith installed, and HAS_ZARITH defined to "yes". In this case, for you, (=) can be applied to big ints. This is one of the problem with Zarith: it makes (=) work (and makes it work correctly) between big ints. The problem is that people who do not have Zarith, or do not have OCaml 3.12.1, still will see errors on applications of (=) to big ints. Jochen, please try to substitute "frama-c.byte" to "frama-c" and see if you obtain a backtrace (please keep using "export OCAMLRUNPARAM=b". In fact, put it in your .profile, there is no reason not to want backtraces).

(0002463) Jochen (reporter) 2011-11-10 15:24	I put "export OCAMLRUNPARAM=b" into my .profile and ran "frama-c.byte", as suggested by Pascal; however, I didn't obtain a backtrace (see file typescript1). Frama-c.byte calls /usr/local/bin/jessie as a subprocess. I found out its args and env and called it again manyally, with an extra option "-d". This produced slightly more output (see file typescript2), but still no backtrace.

(0002477) Jochen (reporter) 2011-11-18 15:02	While I gave up my attempts to produce a backtrace, I happened to find a new strange property: the error disappears if an assert-clause is inserted at the end of the then- or else-part, or both. See the newly uploaded file ftest3.c. Put a "@" in line 6 or 10 to get it verified by Jessie(2.30) and Simplify. None of the asserts in line 2,4,8,12 can cause this effect, even if they are weakened to \true. On the other hand, the asserts in line 6,10 work well also with formulas different from \true. In fact, the asserted formulas seem to have no influence.

(0002706) flecsim (reporter) 2012-02-15 15:16	While attempting to circumvent issue 0001093, i triggered the same message, and in search for remedy i found this issue. I was able to retrieve a backtrace, but unfortunately i cannot supply the input (confidential). However, i was able to trace this into jc_typing.mintype, where i added two patches in hope to find whats going on. The problem arised on (attempt to) evaluating "mintype _ int32 int32" for whatever reason. Patch and output have been attached as "Output1003.txt". Maybe this helps in nailing down the problem.

(0002752) flecsim (reporter) 2012-03-06 11:34	For me, the error disappeared on patching the definition of expr in jc_typing.ml, lines 2156-2167: Before: \| JCTnative Tboolean -> let te2,te3 = if same_type_no_coercion te2#typ te3#typ then te2,te3 else unit_expr te2, unit_expr te3 in let t = mintype e#pos te2#typ te3#typ in t, te2#region, JCEif(te1, te2, te3) After: \| JCTnative Tboolean -> let te2,te3 = unit_expr te2, unit_expr te3 in let t = mintype e#pos te2#typ te3#typ in t, te2#region, JCEif(te1, te2, te3) I am not sure whether this change may cause malfunction of Jessie, but i had quite some "abstract value" errors collected among various projects. As none of them held up against the patch, chances are the problem is located in that area of code.

(0003094) yakobowski (manager) 2012-06-10 14:06	I have never been able to reproduce this bug myself, but there is something suspicious in the body of same_type_no_coercion let same_type_no_coercion t1 t2 = match t1,t2 with \| JCTnative t1, JCTnative t2 -> t1=t2 \| JCTenum ei1, JCTenum ei2 -> ei1.jc_enum_info_name = ei2.jc_enum_info_name \| JCTlogic s1, JCTlogic s2 -> (* ?? ) s1=s2 ( ?? ) [...] Can you try again with this definition instead? let rec same_type_no_coercion t1 t2 = match t1,t2 with \| JCTnative t1, JCTnative t2 -> t1=t2 \| JCTenum ei1, JCTenum ei2 -> ei1.jc_enum_info_name = ei2.jc_enum_info_name \| JCTlogic (name1, args1), JCTlogic (name2, args2) -> name1=name2 && List.for_all2 same_type_no_coercion args1 args2 ( following identical *)

(0003191) cmarche (developer) 2012-06-22 18:01	I applied the modifications suggested by Boris into the SVN. No tests in the regression suite is affected, so I guees it is hamless ans the issue can be assumed as resolved.

(0003780) signoles (manager) 2013-03-27 09:43	Fixed in Frama-C Oxygen + Why 2.32.

Relationships