Skip to content

Commit

Permalink
Fix is_storable_type for custom ADTs (#411)
Browse files Browse the repository at this point in the history
* Create message with ADT value

* Make ADTs with unstorable constructor arguments unstorable

* fixes based on review comments

* remove redundant test
  • Loading branch information
jjcnn authored and vaivaswatha committed Jan 29, 2019
1 parent 0148f83 commit bcf7299
Show file tree
Hide file tree
Showing 4 changed files with 82 additions and 11 deletions.
44 changes: 33 additions & 11 deletions src/lang/base/TypeUtil.ml
Original file line number Diff line number Diff line change
Expand Up @@ -243,17 +243,39 @@ module TypeUtilities
| PolyFun _ -> false
| _ -> true

let rec is_storable_type t = match t with
| FunType _ -> false
| MapType (kt, vt) -> is_storable_type kt && is_storable_type vt
| TypeVar _ -> false
| ADT (_, ts) -> List.for_all ~f:(fun t -> is_storable_type t) ts
| PolyFun _ -> false
| Unit -> false
| PrimType _ ->
(* Messages/Events when stored or passed in messages cannot be analyzed,
* leading to potential badly constructed Messages/Events. So we disallow. *)
not (t = PrimTypes.msg_typ || t = PrimTypes.event_typ)
let is_storable_type t =
let rec storable_helper t seen_adts =
match t with
| FunType _ -> false
| MapType (kt, vt) -> storable_helper kt seen_adts && storable_helper vt seen_adts
| TypeVar _ ->
(* If we are inside an ADT, then type variable
instantiations are handled outside *)
(match seen_adts with
| [] -> false
| _ -> true)
| ADT (tname, ts) ->
(match List.findi ~f:(fun _ seen -> seen = tname) seen_adts with
| Some _ -> true (* Inductive ADT - ignore this branch *)
| None ->
(* Check that ADT is storable *)
match DataTypeDictionary.lookup_name tname with
| Error _ -> false (* Handle errors outside *)
| Ok adt ->
let adt_storable =
List.for_all ~f:(fun (_, carg_list) ->
List.for_all ~f:(fun carg ->
storable_helper carg (tname :: seen_adts))
carg_list)
adt.tmap in
adt_storable && List.for_all ~f:(fun t -> storable_helper t seen_adts) ts)
| PolyFun _ -> false
| Unit -> false
| PrimType _ ->
(* Messages/Events when stored or passed in messages cannot be analyzed,
* leading to potential badly constructed Messages/Events. So we disallow. *)
not (t = PrimTypes.msg_typ || t = PrimTypes.event_typ) in
storable_helper t []

let get_msgevnt_type m =
if (List.exists ~f:(fun (s, _) -> s = ContractUtil.MessagePayload.tag_label) m)
Expand Down
1 change: 1 addition & 0 deletions tests/checker/bad/TestCheckerFail.ml
Original file line number Diff line number Diff line change
Expand Up @@ -49,6 +49,7 @@ module Tests = TestUtil.DiffBasedTests(
"bad_adt_2.scilla";
"bad_adt_3.scilla";
"bad_adt_4.scilla";
"unstorable_adt.scilla";
]
let exit_code : Unix.process_status = WEXITED 1
end)
Expand Down
29 changes: 29 additions & 0 deletions tests/checker/bad/gold/unstorable_adt.scilla.gold
Original file line number Diff line number Diff line change
@@ -0,0 +1,29 @@
{
"errors": [
{
"error_message": "Type error(s) in contract UnstorableADT:\n",
"start_location": {
"file": "checker/bad/unstorable_adt.scilla",
"line": 15,
"column": 10
},
"end_location": { "file": "", "line": 0, "column": 0 }
},
{
"error_message": "Type error in field last_input:\n",
"start_location": {
"file": "checker/bad/unstorable_adt.scilla",
"line": 19,
"column": 7
},
"end_location": { "file": "", "line": 0, "column": 0 }
},
{
"error_message":
"Values of the type \"Option (Test)\" cannot be stored.",
"start_location": { "file": "", "line": 0, "column": 0 },
"end_location": { "file": "", "line": 0, "column": 0 }
}
],
"warnings": []
}
19 changes: 19 additions & 0 deletions tests/checker/bad/unstorable_adt.scilla
Original file line number Diff line number Diff line change
@@ -0,0 +1,19 @@
scilla_version 0

(***************************************************)
(* Associated library *)
(***************************************************)

library UnstorableADT

type Test =
| Bad of (Uint32 -> Uint32)

(***************************************************)
(* The contract definition *)
(***************************************************)
contract UnstorableADT
(
)

field last_input : Option Test = None {Test}

0 comments on commit bcf7299

Please sign in to comment.