Skip to content

Commit de2f979

Browse files
author
thk123
committed
Made ai_simplify perform a partial simplifcation
If the ai_simplify is not able to resolve the expression to a constant, it tries to simplify recursively any child operations. For example, given a int i that is know to be 1, and an unknown (top) array a, it would convert a[i] to a[1].
1 parent 8601e81 commit de2f979

File tree

5 files changed

+69
-2
lines changed

5 files changed

+69
-2
lines changed
+31
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,31 @@
1+
2+
default: tests.log
3+
4+
test:
5+
@if ! ../test.pl -c ../chain.sh ; then \
6+
../failed-tests-printer.pl ; \
7+
exit 1; \
8+
fi
9+
10+
tests.log:
11+
@if ! ../test.pl -c ../chain.sh ; then \
12+
../failed-tests-printer.pl ; \
13+
exit 1; \
14+
fi
15+
16+
show:
17+
@for dir in *; do \
18+
if [ -d "$$dir" ]; then \
19+
vim -o "$$dir/*.c" "$$dir/*.out"; \
20+
fi; \
21+
done;
22+
23+
clean:
24+
@for dir in *; do \
25+
rm -f tests.log; \
26+
if [ -d "$$dir" ]; then \
27+
cd "$$dir"; \
28+
rm -f *.out *.gb; \
29+
cd ..; \
30+
fi \
31+
done
+14
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
#!/bin/bash
2+
3+
src_dir=../../../src
4+
5+
goto_analyzer=$src_dir/goto-analyzer/goto-analyzer
6+
7+
options=$1
8+
file_name=${2%.c}
9+
10+
echo options: $options
11+
echo file name : $file_name
12+
13+
$goto_analyzer $file_name.c $options --simplify $file_name_simp.out
14+
$goto_analyzer $file_name_simp.out --show-goto-functions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
extern int arr[];
2+
3+
void main()
4+
{
5+
int index=0;
6+
int j=arr[index];
7+
}
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
CORE
2+
main.c
3+
"--variable --arrays"
4+
5+
arr\[0l\]

src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp

+12-2
Original file line numberDiff line numberDiff line change
@@ -275,8 +275,18 @@ bool variable_sensitivity_domaint::ai_simplify(
275275
sharing_ptrt<abstract_objectt> res=abstract_state.eval(condition, ns);
276276
exprt c=res->to_constant();
277277

278-
if(c.id()==ID_nil) // TODO : simplification within an expression
279-
return true;
278+
if(c.id()==ID_nil)
279+
{
280+
bool no_simplification=true;
281+
282+
// Try to simplify recursively any child operations
283+
for(exprt &op : condition.operands())
284+
{
285+
no_simplification&=ai_simplify(op, ns);
286+
}
287+
288+
return no_simplification;
289+
}
280290
else
281291
{
282292
bool condition_changed=(condition!=c);

0 commit comments

Comments
 (0)