Skip to content

Commit 0c369db

Browse files
sim642sim642
authored
Merge pull request #601 from goblint/function-annotation-options
Simplify function annotation options
2 parents 4c51356 + 1808578 commit 0c369db

File tree

9 files changed

+77
-167
lines changed

9 files changed

+77
-167
lines changed

‎src/util/contextUtil.ml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,7 @@ let has_attribute s1 s2 al =
2020
) al
2121

2222
let has_option s1 s2 fd =
23-
List.mem fd.svar.vname (GobConfig.get_string_list ("annotation." ^ s1 ^ "." ^ s2))
23+
List.mem s2 (GobConfig.get_string_list ("annotation." ^ s1 ^ "." ^ fd.svar.vname))
2424

2525
let should_keep ~isAttr ~keepOption ~removeAttr ~keepAttr fd =
2626
let al = fd.svar.vattr in

‎src/util/gobConfig.ml‎

Lines changed: 6 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -181,7 +181,9 @@ struct
181181
| `Assoc m, Select (key,pth) ->
182182
begin
183183
try get_value (List.assoc key m) pth
184-
with Not_found -> raise ConfTypeError
184+
with Not_found ->
185+
try get_value (List.assoc Options.defaults_additional_field m) pth (* if schema specifies additionalProperties, then use the default from that *)
186+
with Not_found -> raise ConfTypeError
185187
end
186188
| `List a, Index (Int i, pth) ->
187189
begin
@@ -225,20 +227,14 @@ struct
225227
match o, pth with
226228
| `Assoc m, Select (key,pth) ->
227229
let rec modify = function
228-
| [] -> raise Not_found
230+
| [] ->
231+
[(key, create_new v pth)] (* create new key, validated by schema *)
229232
| (key', v') :: kvs when key' = key ->
230233
(key, set_value v v' pth) :: kvs
231234
| (key', v') :: kvs ->
232235
(key', v') :: modify kvs
233236
in
234-
begin try `Assoc (modify m)
235-
with Not_found ->
236-
(* TODO: allow unknown paths to create subobjects, will be validated against schema anyway *)
237-
(* if !build_config then
238-
`Assoc (m @ [(key, create_new v pth)])
239-
else *)
240-
raise @@ ConfigError ("Unknown path "^ (sprintf2 "%a" print_path orig_pth))
241-
end
237+
`Assoc (modify m)
242238
| `List a, Index (Int i, pth) ->
243239
`List (List.modify_at i (fun o -> set_value v o pth) a)
244240
| `List a, Index (App, pth) ->

‎src/util/jsonSchema.ml‎

Lines changed: 50 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,21 @@ module JS = Json_schema.Make (Json_repr.Yojson)
44
module JE = Json_encoding.Make (Json_repr.Yojson)
55
module JQ = Json_query.Make (Json_repr.Yojson)
66

7+
(* copied & modified from json_encoding.ml *)
8+
let unexpected kind expected =
9+
let kind =
10+
match Json_repr.from_yojson kind with
11+
| `O [] -> "empty object"
12+
| `A [] -> "empty array"
13+
| `O _ -> "object"
14+
| `A _ -> "array"
15+
| `Null -> "null"
16+
| `String _ -> "string"
17+
| `Float _ -> "number"
18+
| `Bool _ -> "boolean"
19+
in
20+
Json_encoding.Cannot_destruct ([], Json_encoding.Unexpected (kind, expected))
21+
722
let schema_to_yojson schema = JS.to_json schema
823
let schema_of_yojson json = JS.of_json json
924

@@ -33,15 +48,36 @@ let rec encoding_of_schema_element (top: unit Json_encoding.encoding) (schema_el
3348
| Id_ref "" ->
3449
top
3550
| Object object_specs ->
36-
List.fold_left (fun acc (name, element, required, _) ->
51+
let properties_encoding = List.fold_left (fun acc (name, element, required, _) ->
3752
let field =
3853
if required then
3954
req name (encoding_of_schema_element top element)
4055
else
4156
dft name (encoding_of_schema_element top element) ()
4257
in
4358
erase @@ merge_objs acc (obj1 field)
44-
) (Option.map_default (encoding_of_schema_element top) empty object_specs.additional_properties) object_specs.properties
59+
) empty object_specs.properties
60+
in
61+
begin match object_specs.additional_properties with
62+
| Some additional_properties ->
63+
let additional_encoding = encoding_of_schema_element top additional_properties in
64+
JE.custom (fun _ -> failwith "erase construct") (function
65+
| `Assoc fields ->
66+
let is_properties_field (name, _) = List.exists (fun (name', _, _, _) -> name = name') object_specs.properties in
67+
let (properties_fields, additional_fields) = List.partition is_properties_field fields in
68+
JE.destruct properties_encoding (`Assoc properties_fields);
69+
List.iter (fun (name, value) ->
70+
try
71+
JE.destruct additional_encoding value
72+
with Cannot_destruct (path, err) ->
73+
raise (Cannot_destruct (`Field name :: path, err))
74+
) additional_fields
75+
| j ->
76+
raise (unexpected j "object")
77+
) ~schema:(Json_schema.create schema_element)
78+
| None ->
79+
properties_encoding
80+
end
4581
| _ -> failwith (Format.asprintf "encoding_of_schema_element: %a" Json_schema.pp (Json_schema.create schema_element))
4682

4783
let encoding_of_schema (schema: Json_schema.schema): unit Json_encoding.encoding =
@@ -50,23 +86,30 @@ let encoding_of_schema (schema: Json_schema.schema): unit Json_encoding.encoding
5086

5187
open Json_schema
5288

53-
let rec element_defaults (element: element): Yojson.Safe.t =
89+
let rec element_defaults ?additional_field (element: element): Yojson.Safe.t =
5490
match element.default with
5591
| Some default ->
5692
Json_repr.any_to_repr (module Json_repr.Yojson) default
5793
| None ->
5894
begin match element.kind with
5995
| Object object_specs ->
60-
`Assoc (List.map (fun (name, field_element, _, _) ->
61-
(name, element_defaults field_element)
96+
let additional = match additional_field, object_specs.additional_properties with
97+
| Some additional_field, Some additional_properties ->
98+
(* create additional field with the additionalProperties default value for lookup in GobConfig *)
99+
[(additional_field, element_defaults ~additional_field additional_properties)]
100+
| _, _ ->
101+
[]
102+
in
103+
`Assoc (additional @ List.map (fun (name, field_element, _, _) ->
104+
(name, element_defaults ?additional_field field_element)
62105
) object_specs.properties)
63106
| _ ->
64107
Format.printf "%a\n" Json_schema.pp (create element);
65108
failwith "element_defaults"
66109
end
67110

68-
let schema_defaults (schema: schema): Yojson.Safe.t =
69-
element_defaults (root schema)
111+
let schema_defaults ?additional_field (schema: schema): Yojson.Safe.t =
112+
element_defaults ?additional_field (root schema)
70113

71114
let create_schema element =
72115
create @@ { element with id = Some "" } (* add id to make create defs check happy for phases Id_ref, doesn't get outputted apparently *)

‎src/util/options.ml‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -28,7 +28,8 @@ let schema =
2828

2929
let require_all = JsonSchema.schema_require_all schema
3030

31-
let defaults = JsonSchema.schema_defaults schema
31+
let defaults_additional_field = "__additional__" (* this shouldn't conflict with any actual field *)
32+
let defaults = JsonSchema.schema_defaults ~additional_field:defaults_additional_field schema
3233

3334
let () =
3435
(* Yojson.Safe.pretty_to_channel (Stdlib.open_out "options.require-all.schema.json") (JsonSchema.schema_to_yojson require_all); *)

‎src/util/options.schema.json‎

Lines changed: 14 additions & 144 deletions
Original file line numberDiff line numberDiff line change
@@ -1069,156 +1069,26 @@
10691069
"goblint_context": {
10701070
"title": "annotation.goblint_context",
10711071
"type": "object",
1072-
"properties": {
1073-
"base": {
1074-
"title": "annotation.goblint_context.base",
1075-
"type": "object",
1076-
"properties": {
1077-
"no-non-ptr": {
1078-
"title": "annotation.goblint_context.base.no-non-ptr",
1079-
"description": "",
1080-
"type": "array",
1081-
"items": { "type": "string" },
1082-
"default": []
1083-
},
1084-
"non-ptr": {
1085-
"title": "annotation.goblint_context.base.non-ptr",
1086-
"description": "",
1087-
"type": "array",
1088-
"items": { "type": "string" },
1089-
"default": []
1090-
},
1091-
"no-int": {
1092-
"title": "annotation.goblint_context.base.no-int",
1093-
"description": "",
1094-
"type": "array",
1095-
"items": { "type": "string" },
1096-
"default": []
1097-
},
1098-
"int": {
1099-
"title": "annotation.goblint_context.base.int",
1100-
"description": "",
1101-
"type": "array",
1102-
"items": { "type": "string" },
1103-
"default": []
1104-
},
1105-
"no-interval": {
1106-
"title": "annotation.goblint_context.base.no-interval",
1107-
"description": "",
1108-
"type": "array",
1109-
"items": { "type": "string" },
1110-
"default": []
1111-
},
1112-
"interval": {
1113-
"title": "annotation.goblint_context.base.interval",
1114-
"description": "",
1115-
"type": "array",
1116-
"items": { "type": "string" },
1117-
"default": []
1118-
}
1119-
},
1120-
"additionalProperties": false
1121-
},
1122-
"apron": {
1123-
"title": "annotation.goblint_context.apron",
1124-
"type": "object",
1125-
"properties": {
1126-
"no-context": {
1127-
"title": "annotation.goblint_context.apron.no-context",
1128-
"description": "",
1129-
"type": "array",
1130-
"items": { "type": "string" },
1131-
"default": []
1132-
},
1133-
"context": {
1134-
"title": "annotation.goblint_context.apron.context",
1135-
"description": "",
1136-
"type": "array",
1137-
"items": { "type": "string" },
1138-
"default": []
1139-
}
1140-
},
1141-
"additionalProperties": false
1142-
},
1143-
"no-widen": {
1144-
"title": "annotation.goblint_context.no-widen",
1145-
"description": "",
1146-
"type": "array",
1147-
"items": { "type": "string" },
1148-
"default": []
1072+
"additionalProperties": {
1073+
"type": "array",
1074+
"items": {
1075+
"type": "string",
1076+
"enum": ["base.no-non-ptr", "base.non-ptr", "base.no-int", "base.int", "base.no-interval", "base.interval", "apron.no-context", "apron.context", "no-widen", "widen"]
11491077
},
1150-
"widen": {
1151-
"title": "annotation.goblint_context.widen",
1152-
"description": "",
1153-
"type": "array",
1154-
"items": { "type": "string" },
1155-
"default": []
1156-
}
1157-
},
1158-
"additionalProperties": false
1078+
"default": []
1079+
}
11591080
},
11601081
"goblint_precision": {
11611082
"title": "annotation.goblint_precision",
11621083
"type": "object",
1163-
"properties": {
1164-
"no-def_exc": {
1165-
"title": "annotation.goblint_precision.no-def_exc",
1166-
"description": "",
1167-
"type": "array",
1168-
"items": { "type": "string" },
1169-
"default": []
1170-
},
1171-
"def_exc": {
1172-
"title": "annotation.goblint_precision.def_exc",
1173-
"description": "",
1174-
"type": "array",
1175-
"items": { "type": "string" },
1176-
"default": []
1177-
},
1178-
"no-interval": {
1179-
"title": "annotation.goblint_precision.no-interval",
1180-
"description": "",
1181-
"type": "array",
1182-
"items": { "type": "string" },
1183-
"default": []
1184-
},
1185-
"interval": {
1186-
"title": "annotation.goblint_precision.interval",
1187-
"description": "",
1188-
"type": "array",
1189-
"items": { "type": "string" },
1190-
"default": []
1191-
},
1192-
"no-enums": {
1193-
"title": "annotation.goblint_precision.no-enums",
1194-
"description": "",
1195-
"type": "array",
1196-
"items": { "type": "string" },
1197-
"default": []
1198-
},
1199-
"enums": {
1200-
"title": "annotation.goblint_precision.enums",
1201-
"description": "",
1202-
"type": "array",
1203-
"items": { "type": "string" },
1204-
"default": []
1205-
},
1206-
"no-congruence": {
1207-
"title": "annotation.goblint_precision.no-congruence",
1208-
"description": "",
1209-
"type": "array",
1210-
"items": { "type": "string" },
1211-
"default": []
1084+
"additionalProperties": {
1085+
"type": "array",
1086+
"items": {
1087+
"type": "string",
1088+
"enum": ["no-def_exc", "def_exc", "no-interval", "interval", "no-enums", "enums", "no-congruence", "congruence"]
12121089
},
1213-
"congruence": {
1214-
"title": "annotation.goblint_precision.congruence",
1215-
"description": "",
1216-
"type": "array",
1217-
"items": { "type": "string" },
1218-
"default": []
1219-
}
1220-
},
1221-
"additionalProperties": false
1090+
"default": []
1091+
}
12221092
}
12231093
},
12241094
"additionalProperties": false

‎tests/incremental/01-force-reanalyze/00-int.patch‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,7 @@
2525
"enabled" : true
2626
+ },
2727
+ "goblint_precision": {
28-
+ "interval" : ["f"]
28+
+ "f" : ["interval"]
2929
}
3030
},
3131
"ana" : {

‎tests/regression/02-base/67-no-int-context-option.c‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
// PARAM: --enable ana.int.interval --disable ana.context.widen --enable ana.base.context.int --set annotation.goblint_context.base.no-int[+] f
1+
// PARAM: --enable ana.int.interval --disable ana.context.widen --enable ana.base.context.int --set annotation.goblint_context.f[+] base.no-int
22
#include <assert.h>
33

44
int f(int x) {

‎tests/regression/02-base/68-int-context-option.c‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
// PARAM: --enable ana.int.interval --disable ana.context.widen --disable ana.base.context.int --set annotation.goblint_context.base.int[+] f
1+
// PARAM: --enable ana.int.interval --disable ana.context.widen --disable ana.base.context.int --set annotation.goblint_context.f[+] base.int
22
#include <assert.h>
33

44
int f(int x) {

‎tests/regression/42-annotated-precision/37-def_exc-via-option.c‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
// PARAM: --enable annotation.int.enabled --set ana.int.refinement fixpoint --set annotation.goblint_precision.def_exc[+] f --set annotation.goblint_precision.interval[+] f --set annotation.goblint_precision.def_exc[+] main
1+
// PARAM: --enable annotation.int.enabled --set ana.int.refinement fixpoint --set annotation.goblint_precision.f[+] def_exc --set annotation.goblint_precision.f[+] interval --set annotation.goblint_precision.main[+] def_exc
22
#include<assert.h>
33

44
int f(int in) {

0 commit comments

Comments
 (0)