FIXME: Create a list of structs

[weaversa]

I was trying to create a list of numElements entries, all initialized the same (by init_function with some params), and came across a "FIXME" from saw.

rec init_list numElements init_function params = do {
  list <- if (eval_bool {{ `numElements : [32] == 0 }}) then []
          else (concat [init_function params]
               (init_list (eval_int {{ `numElements : [32] - 1 }}) init_function params));
  return list;
};

[20:13:43.132] Loading file "blah.saw"
[20:13:43.174] Type errors:
 Type Mismatch, expected: t.1 -> (t.3 -> t.15) -> t.3 -> t.18 t.19 but got: Int -> (t.3 -> t.15) -> t.3 -> [t.15]
FIXME

Am I doing this right? If so, consider this FIXME a bug report. If I'm not doing it right, how can I do this?

[brianhuffman]

Grepping through the sources, the only places I can see that have the "FIXME" as a Haskell string literal are this bogus source position value:

saw-script/src/SAWScript/Builtins.hs

Line 955 in 2398963

fixPos = PosInternal "FIXME"

and this call to error in the saw-script type checker:

saw-script/src/SAWScript/MGU.hs

Line 628 in 2398963

sequence_ $ zipWith (constrainTypeWithPattern (error "FIXME")) ts pats'

I imagine the second occurrence is the one you're hitting here. I'll need to investigate to see whether this is supposed to indicate a user error or an internal panic; we should consider this a bug in either case.

[brianhuffman]

How embarrassing: git blame says that call to error "FIXME" is totally my fault, from 4 years ago. I'll take responsibility for fixing it.

[weaversa]

I got FIXME again. The error is correct here. I'm just reporting in case it helps at all.

Type Mismatch, expected: t.1 -> (t.3 -> CrucibleSetup {c : Term, s : SetupValue}) -> t.3 -> CrucibleSetup {s : [SetupValue]} but got: Int -> (t.3 -> CrucibleSetup {c : Term, s : SetupValue}) -> t.3 -> CrucibleSetup {c : Term, s : [SetupValue]}
FIXME

[brianhuffman]

In PR #716, running saw on the example from the original post now gives an appropriate type error message with appropriate location information, and does not crash:

[15:57:17.477] Loading file "/Users/huffman/Documents/saw/issue698.saw"
[15:57:17.479] Type errors:
  /Users/huffman/Documents/saw/issue698.saw:1:5-6:2: Type Mismatch, expected: t.1 -> (t.3 -> t.15) -> t.3 -> t.18 t.19 but got: Int -> (t.3 -> t.15) -> t.3 -> [t.15]
 at "init_list" (/Users/huffman/Documents/saw/issue698.saw:1:5-1:14)
Type constructors mismatch. Expected: <Block> but got ([]) at "init_list" (/Users/huffman/Documents/saw/issue698.saw:1:5-1:14)

  /Users/huffman/Documents/saw/issue698.saw:1:50-6:2: Type Mismatch, expected: t.4 t.5 but got: [t.15]
 at "init_list" (/Users/huffman/Documents/saw/issue698.saw:1:5-1:14)
Type constructors mismatch. Expected: <Block> but got ([]) at "init_list" (/Users/huffman/Documents/saw/issue698.saw:1:5-1:14)