Skip to content

Commit 96156fe

Browse files
author
pkesseli
committed
Added benchmark #33, fixed list parameter order in CEGIS jsa.h
1 parent 2304058 commit 96156fe

File tree

6 files changed

+136
-6
lines changed

6 files changed

+136
-6
lines changed

‎regression/cegis/cegis_jsa_benchmark_18/main.c

-2
Original file line numberDiff line numberDiff line change
@@ -28,10 +28,8 @@ int main(void)
2828
__CPROVER_jsa_hasNext(&heap, __CPROVER_jsa_iterator_it);)
2929
{
3030
const __CPROVER_jsa_data_t integer=__CPROVER_jsa_next(&heap, __CPROVER_jsa_iterator_it);
31-
//if ((integer - min) > 0)
3231
if (integer > min)
3332
{
34-
//__CPROVER_jsa_add(&heap, __CPROVER_jsa_list_newList, integer - min);
3533
__CPROVER_jsa_add(&heap, __CPROVER_jsa_list_newList, integer);
3634
}
3735
}

‎regression/cegis/cegis_jsa_benchmark_31/ArrayUtils.java

+80
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,80 @@
1+
package arrays;
2+
3+
import java.util.ArrayList;
4+
import java.util.Arrays;
5+
import java.util.List;
6+
7+
8+
9+
public class ArrayUtils {
10+
11+
public Integer[] merge(Integer[] array1, Integer[] array2){
12+
13+
List<Integer> returnedList = new ArrayList<Integer>();
14+
List<Integer> concatList = array1 != null ? new ArrayList<Integer>(Arrays.asList(array1)) :
15+
(array2 != null ? new ArrayList<Integer>(Arrays.asList(array2)) : new ArrayList<Integer>()) ;
16+
if(array2 != null && array2 != null)
17+
concatList.addAll(Arrays.asList(array2));
18+
19+
for(Integer element2: concatList){
20+
21+
if(returnedList.indexOf(element2) == -1){
22+
returnedList.add(element2);
23+
}
24+
25+
}
26+
return (Integer[]) returnedList.toArray(new Integer[returnedList.size()]);
27+
}
28+
29+
public Integer[] innerJoin(Integer[] array1, Integer[] array2){
30+
31+
List<Integer> returnedList = new ArrayList<Integer>();
32+
33+
for(Integer element1: array1){
34+
35+
for(Integer element2: array2){
36+
if(element2 == element1){
37+
returnedList.add(element1);
38+
break;
39+
}
40+
}
41+
}
42+
43+
return (Integer[]) returnedList.toArray(new Integer[returnedList.size()]);
44+
}
45+
46+
public Integer[] leftJoin(Integer[] array1, Integer[] array2){
47+
48+
List<Integer> returnedList = array1 != null ? new ArrayList<Integer>(Arrays.asList(array1)) :
49+
(array2 != null ? new ArrayList<Integer>(Arrays.asList(array2)) :
50+
new ArrayList<Integer>());
51+
if(array1 != null){
52+
for(Integer element2: array2){
53+
54+
if(returnedList.indexOf(element2) > -1){
55+
returnedList.add(element2);
56+
}
57+
}
58+
}
59+
60+
return (Integer[]) returnedList.toArray(new Integer[returnedList.size()]);
61+
}
62+
63+
public Integer[] outerJoin(Integer[] array1, Integer[] array2){
64+
65+
List<Integer> returnedList = new ArrayList<Integer>();
66+
List<Integer> concatList = array1 != null ? new ArrayList<Integer>(Arrays.asList(array1)) :
67+
(array2 != null ? new ArrayList<Integer>(Arrays.asList(array2)) : new ArrayList<Integer>()) ;
68+
if(array1 != null && array2 != null)
69+
concatList.addAll(Arrays.asList(array2));
70+
71+
for(Integer element1: concatList){
72+
if(concatList.indexOf(element1) == concatList.lastIndexOf(element1)){
73+
returnedList.add(element1);
74+
}
75+
}
76+
77+
return (Integer[]) returnedList.toArray(new Integer[returnedList.size()]);
78+
}
79+
80+
}

‎regression/cegis/cegis_jsa_benchmark_31/main.c

+38
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,38 @@
1+
#ifdef __CPROVER
2+
#define __CPROVER_JSA_MAX_CONCRETE_NODES 2u
3+
#define __CPROVER_JSA_MAX_NODES_PER_LIST 1u
4+
#define __CPROVER_JSA_MAX_ABSTRACT_NODES 0u
5+
#define __CPROVER_JSA_MAX_ITERATORS 1u
6+
#define __CPROVER_JSA_MAX_LISTS 2u
7+
8+
#define JSA_SYNTHESIS_H_
9+
#define __CPROVER_JSA_DEFINE_TRANSFORMERS
10+
#define __CPROVER_JSA_MAX_QUERY_SIZE 2u
11+
#define __CPROVER_JSA_MAX_PRED_SIZE 2u
12+
#define __CPROVER_JSA_NUM_PRED_OPS 5u
13+
#define __CPROVER_JSA_NUM_PRED_RESULT_OPS 2u
14+
#endif
15+
16+
#include "../../../src/ansi-c/library/jsa.h"
17+
18+
int main(void)
19+
{
20+
__CPROVER_jsa_abstract_heapt heap;
21+
__CPROVER_jsa_assume_valid_heap(&heap);
22+
const __CPROVER_jsa_list_id_t __CPROVER_jsa_list_input=0;
23+
__CPROVER_jsa_assume_valid_list(&heap, __CPROVER_jsa_list_input);
24+
const __CPROVER_jsa_list_id_t __CPROVER_jsa_list_returnedList=1;
25+
__CPROVER_jsa_assume_new_list(&heap, __CPROVER_jsa_list_returnedList);
26+
const __CPROVER_jsa_data_t element1;
27+
for (const __CPROVER_jsa_iterator_id_t __CPROVER_jsa_iterator_it=__CPROVER_jsa_iterator(&heap, __CPROVER_jsa_list_input);
28+
__CPROVER_jsa_hasNext(&heap, __CPROVER_jsa_iterator_it);)
29+
{
30+
const __CPROVER_jsa_data_t element2=__CPROVER_jsa_next(&heap, __CPROVER_jsa_iterator_it);
31+
if (element2 == element1)
32+
{
33+
__CPROVER_jsa_add(&heap, __CPROVER_jsa_list_returnedList, element2);
34+
}
35+
}
36+
37+
return 0;
38+
}

‎regression/cegis/cegis_jsa_benchmark_31/source.url

+1
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
https://raw.githubusercontent.com/Vladimir-Moskov/GitJavaProjects/f12fc8219bb5b7ad53c4af753d32594cab20138e/javaJunior/src/arrays/ArrayUtils.java

‎regression/cegis/cegis_jsa_benchmark_31/test.desc

+9
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
main.c
3+
--gcc --jsa -D __CPROVER --cegis-statistics --cegis-genetic
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
7+
^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
8+
--
9+
^warning: ignoring

‎src/ansi-c/library/jsa.h

+8-4
Original file line numberDiff line numberDiff line change
@@ -933,11 +933,15 @@ __CPROVER_jsa_inline void __CPROVER_jsa_stream_op(
933933
__CPROVER_jsa_abstract_heapt * const heap,
934934
const __CPROVER_jsa_list_id_t list,
935935
const __CPROVER_jsa_iterator_id_t it,
936-
const __CPROVER_jsa_list_id_t copy,
936+
const __CPROVER_jsa_list_id_t source,
937937
const __CPROVER_jsa_pred_id_t pred_id,
938938
const __CPROVER_jsa__internal_index_t id)
939939
{
940-
__CPROVER_jsa_node_id_t node=__CPROVER_jsa__internal_get_head_node(heap, list);
940+
__CPROVER_jsa_node_id_t node;
941+
if (__CPROVER_jsa_null == source)
942+
node = __CPROVER_jsa__internal_get_head_node(heap, list);
943+
else
944+
node = __CPROVER_jsa__internal_get_head_node(heap, source);
941945
const __CPROVER_jsa_node_id_t end=heap->iterators[it].node_id;
942946
for (__CPROVER_jsa__internal_index_t i=0; i < __CPROVER_JSA_MAX_NODES_PER_LIST; ++i)
943947
{
@@ -958,10 +962,10 @@ __CPROVER_jsa_inline void __CPROVER_jsa_stream_op(
958962
break;
959963
case COPY_IF:
960964
if (pred_result != 0)
961-
__CPROVER_jsa_add(heap, copy, value);
965+
__CPROVER_jsa_add(heap, list, value);
962966
break;
963967
case MAP:
964-
__CPROVER_jsa_add(heap, copy, pred_result);
968+
__CPROVER_jsa_add(heap, list, pred_result);
965969
break;
966970
case MAP_IN_PLACE:
967971
heap->concrete_nodes[node].value=pred_result;

0 commit comments

Comments
 (0)