1
1
#include " hal_core/netlist/boolean_function/symbolic_execution.h"
2
-
3
2
#include " hal_core/utilities/log.h"
4
3
5
4
namespace hal
@@ -235,6 +234,141 @@ namespace hal
235
234
return BooleanFunction::Const (simplified);
236
235
}
237
236
237
+ /* *
238
+ * Helper function to simplify a constant SHL operation.
239
+ *
240
+ * @param[in] p0 - Boolean function parameter 0.
241
+ * @param[in] p1 - Boolean function parameter 1.
242
+ * @returns Boolean function with a simplified constant value.
243
+ */
244
+ BooleanFunction Shl (const std::vector<BooleanFunction::Value>& p0, const u16 p1)
245
+ {
246
+ if (p1 >= p0.size ())
247
+ {
248
+ // Shift amount is too large, result is all zeros
249
+ return BooleanFunction::Const (std::vector<BooleanFunction::Value>(p0.size (), BooleanFunction::Value::ZERO));
250
+ }
251
+
252
+ std::vector<BooleanFunction::Value> result (p0.size (), BooleanFunction::Value::ZERO);
253
+
254
+ // Copy bits from original position to shifted position
255
+ for (auto i = p1; i < p0.size (); i++)
256
+ {
257
+ result[i] = p0[i - p1];
258
+ }
259
+
260
+ return BooleanFunction::Const (result);
261
+ }
262
+
263
+ /* *
264
+ * Helper function to simplify a constant LSHR operation.
265
+ *
266
+ * @param[in] p0 - Boolean function parameter 0.
267
+ * @param[in] p1 - Boolean function parameter 1.
268
+ * @returns Boolean function with a simplified constant value.
269
+ */
270
+ BooleanFunction Lshr (const std::vector<BooleanFunction::Value>& p0, const u16 p1)
271
+ {
272
+ if (p1 >= p0.size ())
273
+ {
274
+ // Shift amount is too large, result is all zeros
275
+ return BooleanFunction::Const (std::vector<BooleanFunction::Value>(p0.size (), BooleanFunction::Value::ZERO));
276
+ }
277
+
278
+ std::vector<BooleanFunction::Value> result (p0.size (), BooleanFunction::Value::ZERO);
279
+
280
+ // Copy bits from original position to shifted position
281
+ for (auto i = 0u ; i < p0.size () - p1; i++)
282
+ {
283
+ result[i] = p0[i + p1];
284
+ }
285
+
286
+ return BooleanFunction::Const (result);
287
+ }
288
+
289
+ /* *
290
+ * Helper function to simplify a constant ASHR operation.
291
+ *
292
+ * @param[in] p0 - Boolean function parameter 0.
293
+ * @param[in] p1 - Boolean function parameter 1.
294
+ * @returns Boolean function with a simplified constant value.
295
+ */
296
+ BooleanFunction Ashr (const std::vector<BooleanFunction::Value>& p0, const u16 p1)
297
+ {
298
+ auto sign_bit = p0.back (); // MSB is the sign bit
299
+
300
+ if (p1 >= p0.size ())
301
+ {
302
+ // Shift amount is too large, result is all sign bits
303
+ return BooleanFunction::Const (std::vector<BooleanFunction::Value>(p0.size (), sign_bit));
304
+ }
305
+
306
+ std::vector<BooleanFunction::Value> result (p0.size (), sign_bit);
307
+
308
+ // Copy bits from original position to shifted position
309
+ for (auto i = 0u ; i < p0.size () - p1; i++)
310
+ {
311
+ result[i] = p0[i + p1];
312
+ }
313
+
314
+ return BooleanFunction::Const (result);
315
+ }
316
+
317
+ /* *
318
+ * Helper function to simplify a constant ROL operation.
319
+ *
320
+ * @param[in] p0 - Boolean function parameter 0.
321
+ * @param[in] p1 - Boolean function parameter 1.
322
+ * @returns Boolean function with a simplified constant value.
323
+ */
324
+ BooleanFunction Rol (const std::vector<BooleanFunction::Value>& p0, const u16 p1)
325
+ {
326
+ auto rotate_amount = p1 % p0.size (); // Modulo for rotation
327
+
328
+ if (rotate_amount == 0 )
329
+ {
330
+ return BooleanFunction::Const (p0); // No rotation needed
331
+ }
332
+
333
+ std::vector<BooleanFunction::Value> result (p0.size ());
334
+
335
+ // Perform the rotation
336
+ for (auto i = 0u ; i < p0.size (); i++)
337
+ {
338
+ auto new_pos = (i + rotate_amount) % p0.size ();
339
+ result[new_pos] = p0[i];
340
+ }
341
+
342
+ return BooleanFunction::Const (result);
343
+ }
344
+
345
+ /* *
346
+ * Helper function to simplify a constant ROR operation.
347
+ *
348
+ * @param[in] p0 - Boolean function parameter 0.
349
+ * @param[in] p1 - Boolean function parameter 1.
350
+ * @returns Boolean function with a simplified constant value.
351
+ */
352
+ BooleanFunction Ror (const std::vector<BooleanFunction::Value>& p0, const u16 p1)
353
+ {
354
+ auto rotate_amount = p1 % p0.size (); // Modulo for rotation
355
+
356
+ if (rotate_amount == 0 )
357
+ {
358
+ return BooleanFunction::Const (p0); // No rotation needed
359
+ }
360
+
361
+ std::vector<BooleanFunction::Value> result (p0.size ());
362
+
363
+ // Perform the rotation
364
+ for (auto i = 0u ; i < p0.size (); i++)
365
+ {
366
+ auto new_pos = (i + p0.size () - rotate_amount) % p0.size ();
367
+ result[new_pos] = p0[i];
368
+ }
369
+
370
+ return BooleanFunction::Const (result);
371
+ }
238
372
/* *
239
373
* Helper function to simplify a constant SLE operation.
240
374
*
@@ -1288,9 +1422,19 @@ namespace hal
1288
1422
}
1289
1423
1290
1424
std::vector<std::vector<BooleanFunction::Value>> values;
1425
+ std::vector<u16> indices;
1426
+
1291
1427
for (const auto & parameter : p)
1292
1428
{
1293
- values.emplace_back (parameter.get_top_level_node ().constant );
1429
+ if (parameter.is_index ())
1430
+ {
1431
+ indices.push_back (parameter.get_index_value ().get ());
1432
+ }
1433
+ else
1434
+ {
1435
+ const auto v = parameter.get_top_level_node ().constant ;
1436
+ values.emplace_back (v);
1437
+ }
1294
1438
}
1295
1439
1296
1440
switch (node.type )
@@ -1311,15 +1455,32 @@ namespace hal
1311
1455
case BooleanFunction::NodeType::Mul:
1312
1456
return OK (ConstantPropagation::Mul (values[0 ], values[1 ]));
1313
1457
1314
- case BooleanFunction::NodeType::Slice: {
1315
- auto start = p[1 ].get_index_value ().get ();
1316
- auto end = p[2 ].get_index_value ().get ();
1317
- return OK (BooleanFunction::Const (std::vector<BooleanFunction::Value>(values[0 ].begin () + start, values[0 ].begin () + end + 1 )));
1458
+ case BooleanFunction::NodeType::Sdiv: {
1459
+ // TODO implement
1460
+ return ERR (" could not propagate constants: not implemented for given node type" );
1461
+ }
1462
+ case BooleanFunction::NodeType::Udiv: {
1463
+ // TODO implement
1464
+ return ERR (" could not propagate constants: not implemented for given node type" );
1465
+ }
1466
+ case BooleanFunction::NodeType::Srem: {
1467
+ // TODO implement
1468
+ return ERR (" could not propagate constants: not implemented for given node type" );
1318
1469
}
1470
+ case BooleanFunction::NodeType::Urem: {
1471
+ // TODO implement
1472
+ return ERR (" could not propagate constants: not implemented for given node type" );
1473
+ }
1474
+
1319
1475
case BooleanFunction::NodeType::Concat: {
1320
1476
values[1 ].insert (values[1 ].end (), values[0 ].begin (), values[0 ].end ());
1321
1477
return OK (BooleanFunction::Const (values[1 ]));
1322
1478
}
1479
+ case BooleanFunction::NodeType::Slice: {
1480
+ auto start = p[1 ].get_index_value ().get ();
1481
+ auto end = p[2 ].get_index_value ().get ();
1482
+ return OK (BooleanFunction::Const (std::vector<BooleanFunction::Value>(values[0 ].begin () + start, values[0 ].begin () + end + 1 )));
1483
+ }
1323
1484
case BooleanFunction::NodeType::Zext: {
1324
1485
values[0 ].resize (node.size , BooleanFunction::Value::ZERO);
1325
1486
return OK (BooleanFunction::Const (values[0 ]));
@@ -1329,6 +1490,17 @@ namespace hal
1329
1490
return OK (BooleanFunction::Const (values[0 ]));
1330
1491
}
1331
1492
1493
+ case BooleanFunction::NodeType::Shl:
1494
+ return OK (ConstantPropagation::Shl (values[0 ], indices[0 ]));
1495
+ case BooleanFunction::NodeType::Lshr:
1496
+ return OK (ConstantPropagation::Lshr (values[0 ], indices[0 ]));
1497
+ case BooleanFunction::NodeType::Ashr:
1498
+ return OK (ConstantPropagation::Ashr (values[0 ], indices[0 ]));
1499
+ case BooleanFunction::NodeType::Rol:
1500
+ return OK (ConstantPropagation::Rol (values[0 ], indices[0 ]));
1501
+ case BooleanFunction::NodeType::Ror:
1502
+ return OK (ConstantPropagation::Ror (values[0 ], indices[0 ]));
1503
+
1332
1504
case BooleanFunction::NodeType::Eq:
1333
1505
return OK ((values[0 ] == values[1 ]) ? BooleanFunction::Const (1 , 1 ) : BooleanFunction::Const (0 , 1 ));
1334
1506
case BooleanFunction::NodeType::Sle:
@@ -1342,14 +1514,6 @@ namespace hal
1342
1514
case BooleanFunction::NodeType::Ite:
1343
1515
return OK (ConstantPropagation::Ite (values[0 ], values[1 ], values[2 ]));
1344
1516
1345
- case BooleanFunction::NodeType::Sdiv:
1346
- // TODO implement
1347
- case BooleanFunction::NodeType::Udiv:
1348
- // TODO implement
1349
- case BooleanFunction::NodeType::Srem:
1350
- // TODO implement
1351
- case BooleanFunction::NodeType::Urem:
1352
- // TODO implement
1353
1517
default :
1354
1518
return ERR (" could not propagate constants: not implemented for given node type" );
1355
1519
}
0 commit comments