Skip to content

Commit

Permalink
eclair: move function and macro properties outside ECLAIR
Browse files Browse the repository at this point in the history
Function and macro properties contained in ECLAIR/call_properties.ecl are of
general interest: this patch moves these annotations in a generaric JSON file
in docs. In this way, they can be exploited for other purposes (i.e. documentation,
other tools).

Add rst file containing explanation on how to update function_macro_properties.json.
Add script to convert the JSON file in ECL configurations.
Remove ECLAIR/call_properties.ecl: the file is now automatically generated from
the JSON file.

Signed-off-by: Maria Celeste Cesario  <maria.celeste.cesario@bugseng.com>
Signed-off-by: Simone Ballarin  <simone.ballarin@bugseng.com>
Acked-by: Stefano Stabellini <sstabellini@kernel.org>
  • Loading branch information
Maria Celeste Cesario authored and jbeulich committed Feb 7, 2024
1 parent 38ae473 commit f4519ee
Show file tree
Hide file tree
Showing 6 changed files with 939 additions and 128 deletions.
1 change: 1 addition & 0 deletions automation/eclair_analysis/ECLAIR/analysis.ecl
Original file line number Diff line number Diff line change
Expand Up @@ -30,6 +30,7 @@ if(not(scheduled_analysis),
-eval_file=deviations.ecl
-eval_file=call_properties.ecl
-eval_file=tagging.ecl
-eval_file=properties.ecl
-eval_file=concat(set,".ecl")

-doc="Hide reports in external code."
Expand Down
128 changes: 0 additions & 128 deletions automation/eclair_analysis/ECLAIR/call_properties.ecl

This file was deleted.

2 changes: 2 additions & 0 deletions automation/eclair_analysis/prepare.sh
Original file line number Diff line number Diff line change
Expand Up @@ -43,4 +43,6 @@ fi
make -f "${script_dir}/Makefile.prepare" prepare
# Translate the /* SAF-n-safe */ comments into ECLAIR CBTs
scripts/xen-analysis.py --run-eclair --no-build --no-clean
# Translate function-properties.json into ECLAIR properties
python3 ${script_dir}/propertyparser.py
)
37 changes: 37 additions & 0 deletions automation/eclair_analysis/propertyparser.py
Original file line number Diff line number Diff line change
@@ -0,0 +1,37 @@
import json
import os

script_dir = os.path.dirname(__file__)
properties_path = os.path.join(script_dir, "../../docs/function_macro_properties.json")
output_path = os.path.join(script_dir, "ECLAIR/call_properties.ecl")

with open(properties_path) as fp:
properties = json.load(fp)['content']

ecl = open(output_path, 'w')

for record in properties:

string = "-call_properties+={\""
if record['type'] == "function":
string += f"{record['value']}\", {{".replace("\\", "\\\\")
else:
string += f"{record['type']}({record['value']})\", {{".replace("\\", "\\\\")

i=0
for prop in record['properties'].items():
if prop[0] == 'attribute':
string += prop[1]
i+=1
else:
string += f"\"{prop[0]}({prop[1]})\""
i+=1

if i<len(record['properties']):
string += ", "
else:
string +="}}\n"

ecl.write(string)

ecl.close()

0 comments on commit f4519ee

Please sign in to comment.